Weeknotes 33, Aug 2026 [2026-W33]

August 10, 2026

Exact first-order checks for gradual typing?

My brief understanding of gradual typing

One phrasing of the slogan of gradual typing is that “gradual typing is about ill-typed programs.” (I heard this from Prof. David van Horn during NJPLS 2026.) But what does that mean? When do we need ill-typed programs?

The famous slogan of type systems is that “well-typed programs do not go wrong.” Obviously, we do not want wrong programs even though they are ill-typed. So, our hope is that the program may go right under some circumstances, just that we cannot justify that to the type system.

From this view, gradual typing means loosening the restrictions from the type system. For instance, we may write x: ? to indicate that x can be seen as anything; in a type system with subtyping, this is the same as down-casting the type of x to the bottom type, so it can be up-cast to any other type.

Besides checking that the program may go right during loosened type checking, some versions of gradual typing also attempt to do better: in circumstances where the program does go wrong, try to make it go wrong in a controlled way. For example, instead of getting stuck, reaching some explicit error state that blames the reason sounds better. Such controlled wrongness is enforced by runtime checks.

Runtime checks and safe erasure

Now, one question is: what exactly should such runtime checks enforce? The answer of that question depends on what kinds of wrongness do we want to control.

Recall that the goal of the static type system is to rule out certain kinds of stuck. Thus, the runtime checks should focus on the same kinds of stuck: when a value passes the runtime check, using it in certain contexts will reduce instead of stuck.

It is very intuitive to come up with a inverse criterion: when using a value in certain contexts will not stuck, it should pass the runtime check. The criterion of robust dynamic embedding captures this: if a dynamic term has the semantics of a certain static type, then only the context surrounding it but not the term itself should be blamed if using the term as that type produces an error.

As stated above, the loosened static obligations are reassured by the runtime checks. Therefore, from this view, it would be absurd if the static obligations themselves are detached from runtime checks. The best view of static types then should be based on the runtime checks.

Safe erasure

Specifically, one interesting case is when we are working with a language that already performs runtime type checks. Not just runtime checks, but runtime type checks. As an instance, Python raises TypeError when the type of things do not match.

For those languages, a natural question then is that can we reuse these already-present checks for gradual typing? This idea is called Safe Erasure Gradual Typing: although the elaboration is merely erasing type annotations, a well-typed term still either 1) diverges, 2) reduces to a so-typed value, or 3) triggers an error at a runtime check already present in the dynamic language.

But what does safe erasure mean, after all? From the intuition, we can understand safe erasure as: the guarantees provided by the types are still sound because of existing runtime checks.

For a function, the inferred function parameters must be over-approximations of their uses in the function body, because otherwise the type would include less values than what would be accepted, which in turn implies more checks than actual, so it would be unsafe to erase.

On the other hand, the inferred function return types are also over-approximations of what would actually be returned, otherwise it would be also unsafe to erase that type because there are no real checks for return types.

What about annotated types? One caveat is that types are not strict anymore. By not being strict I mean that, for example, the return value of a function with type A -> B might not be B. Only strong functions have such property; ordinary functions, when passed a value with the unknown type, only returns an unknown.

This landscape deliberately leaves the other direction open, i.e. under-approximation of function parameter type and under-approximation or function return type.

If we try to view static types as abstractions of runtime checks, one immediate problem is how to treat higher-order types like function types. A function type cannot be an abstraction of runtime checks, because there are no general way to check if a function has a certain function type (in the usual understanding, returning something in the range type if provided something in the domain type) without calling it.

On the contrary, there are other type constructors that I call first-order, and they should have the property that a type containing only first-order type constructors is an exact abstraction of a set of runtime checks.

Safe Erasure Gradual Typing proposes strong functions to deal with function types. A strong function, when called with an arbitrary dynamic argument, can only return a value within its codomain, diverge, or fail through an existing runtime check.

Contexts

Weeknotes [weeknotes]

April 10, 2026

Weeknotes 33, Aug 2026 [2026-W33]

Exact first-order checks for gradual typing?

My brief understanding of gradual typing

Runtime checks and safe erasure

Now, one question is: what exactly should such runtime checks enforce? The answer of that question depends on what kinds of wrongness do we want to control.

Safe erasure

But what does safe erasure mean, after all? From the intuition, we can understand safe erasure as: the guarantees provided by the types are still sound because of existing runtime checks.

This landscape deliberately leaves the other direction open, i.e. under-approximation of function parameter type and under-approximation or function return type.

Weeknotes 24, Jun 2026 [2026-W24]

Semantic subtyping for functions

Dealing with functions in a semantic subtyping setting is awkward: it is generally not viable to use type-case to test with function types. For example, you cannot say “test if $𝑥$ is type $𝑡_{1} \to 𝑡_{2}$ .”

The reason is that, functions don’t have “principal” or “minimal” types in general. That is, for a function value $𝑓$ , it is not guaranteed that there is a type $𝑡_{𝑓}$ such that for any type $𝑡$ , either $𝑡_{𝑓} < : 𝑡$ or $𝑡_{𝑓} < : \neg 𝑡$ . For instance, consider the identity function. Its principal type $𝑡_{id}$ should be $⋂_{𝑡} (𝑡 \to 𝑡)$ for all type $𝑡$ , but that is not expressible in an ordinary type system.

In general, to test whether $𝑓$ has type $𝑡_{1} \to 𝑡_{2}$ is to ask if for every value $𝑥$ in $𝑡_{1}$ , $𝑓 (𝑥)$ is in $𝑡_{2}$ . If there is a principal type $𝑡_{𝑓}$ , then we should be able to get, informally, the restriction of $𝑡_{𝑓}$ to $𝑡_{1}$ . That requires the domain of $𝑡_{𝑓}$ to be able to be split into minimal types, along with also split range. Still consider the identity function: since there are no infinite intersection type, we can only type it as $⊤ \to ⊤$ , and we have no idea what the corresponding range should be for the split domains.

One might ask how do we typecheck a function then. Turns out we are totally fine in typechecking stage, but this is about how to check the type of a function dynamically at runtime, and if we want to call the typechecker at runtime, we will have to introduce a lot of other problems. Maybe using abstract interpretation to execute the function on the abstract domain could help?

Weeknotes 23, Jun 2026 [2026-W23]

Can we use type-cases instead of casts?

Recently I was thinking whether we could simply use type-cases instead of casts for the runtime checks of gradual set-theoretic types. It seems to me that type casts in such a setting are almost just a limited form of type-cases.

When studying gradual typing, we usually have a source language in which typechecking are implicitly loosened by the presence of gradual types, and terms of the source language is translated into a cast language where runtime typechecks are made explicit.

But, in the set-theoretic setting we already have the type-case expression, and its very usage is to check the type of a value at runtime. So, why do we need another set of mechanism, namely casts, instead of using the more “native” type-cases?

However, there are also some differences between them.

First, a cast has a source type and a target type, where a type-case has only a test type which roughly corresponds to the target type, and the source type is implicitly the type of the testee.

Second, they currently work differently for functions. Casts for functions are usually translated to a wrapper which inserts corresponding casts both for the argument and the return value, while type-cases usually only supports testing if something is a function without caring details on the argument and return type.

The last problem is, type-cases being more powerful and generic also means they are more complex. This in turn means replacing casts using type-cases may not make things more simple.

Weeknotes 21, May 2026 [2026-W21]

NJPLS was fun!

I attended this year’s first NJPLS this week, thanks to the generous travel support by my advisor. It was a great experience, although I was a bit upset that my talk proposal didn’t make it. (Nevertheless, after listened to all the talks, I think they are indeed more interesting than mine.)

Talks I enjoyed most were Principal Gradual Type Inference by Prof. David Van Horn and Morphosyntactic Programming: Case, Mood, and Type-Directed Disambiguation for Turkish-Like Syntax by Dr. Joomy Korkut.

Discussion about gradual typing

I discussed with Prof. Van Horn about gradual typing after his talk. One of his interesting slogans in the talk was “gradual typing is about ill-typed programs.” After the discussion, we thought that this claim could be somehow extended. Some programs are definitively ill-typed; for example, using something here as an integer and elsewhere as a boolean is definitively inconsistent, as well as using something here as a pair and elsewhere as a function. We may say such inconsistency violates with the value’s type constructor. Meanwhile, using a function here as an Int -> Int and elsewhere as an Bool -> Bool might be okay at runtime, even the type system may lack the expressivity to type such a function. So, there are two kinds of ill-typedness in terms of gradual types: one is when you mess up with the value’s essence, and another is when you are merely trying to bypass the inability of the type system. We also discussed some other topics.

Non-English programming languages

Dr. Joomy Korkut presented their design of a programming language with a Turkish-Like Syntax, which allows you to use Turkish morphology on identifiers and keywords to express special semantics. I liked this idea a lot.

I do not aim to attack English-based programming languages. They are programming languages after all, and technically one could just regard the keywords as mere symbols (just like those from logic and mathematics). And most programming languages allow Unicode identifiers.

The interesting (to me) idea here is to utilize linguistic features of natural languages, contrary to the “symbolism” view of programming language syntax.

This is also related to some of my thoughts on a programming language in Chinese. Although, like said above, it is easy to imagine one modifying only the lexer of a compiler/interpreter to make it use Chinese keywords and punctuation, that is not what I mean. I was thinking something more accommodated to the distinct properties of Chinese. However, different from Turkish whose morphology could be utilized, Chinese is on the other end: there is no morphology at all, and all meanings are expressed merely by combination of words instead of applying morphology to words. So morphology is not something here. Another distinct property of Chinese is that its texts does not use spaces between words and sentences at all, only line breaks between paragraphs. But this makes it sounds farther away from what a programming language may like. So, I think it still require some considerations on how to program “in Chinese”.

Weeknotes 19, May 2026 [2026-W19]

Post什么是“缠绕沈子纲之铁链” [000W]

如果在一些在线英汉汉英词典（如欧路词典）上查询 dangles（注意并非 dangle）这个词，会得到一个奇怪的义项：“n. 缠绕沈子纲之铁链”。这个义项令人十分迷惑：谁是沈子纲（这听上去很像一个人名），或者说，什么是沈子纲？为什么要用铁链缠绕沈子纲？为什么 dangles 会被联系到这个义项？

这激起了我的好奇心。此时，如果是熟悉渔业专业英语的人，已经能大致知道背后的来龙去脉甚至可能并不觉得奇怪。遗憾的是，我并不熟悉渔业专业英语。

于是我在网络上查询“缠绕沈子纲之铁链”。搜索结果几乎全部是无关结果，主要来自“缠绕”和“铁链”这两个关键词，然而结果中也有其他若干英汉汉英词典或翻译网站，无一例外在它们的“网络释义”中将 dangles 这个词解释为“缠绕沈子纲之铁链”。幸运的是，必应词典提供了这个“网络释义”义项的来源：“食品论坛” BBS 的“水产”板块中，有用户提问“谁能提供关于水产的英语词汇”，而回复中有一位神秘人贴出了大量独家汉英词汇对照。在页面上搜索 dangles，果然该神秘人将其解释为“缠绕沈子纲之铁链”。到了这一步，这个义项的来源已经解明。剩下的问题是：什么是“沈子纲”？什么又是“缠绕沈子纲之铁链”？为什么要用铁链缠绕沈子纲？

此时，如果是更聪明的人，已经能快速知道“沈子纲”对应的是什么。遗憾的是，我并没有这么聪明。

于是我在网络上查询“沈子纲”。可以看出这个词汇的确很像个人名，因为搜索结果几乎都与各种人物有关。不过，其中出现了一个英文词汇 footrope 的百度百科页面，其解释为：“footrope，英语单词，主要用作为名词，用作名词译为‘沈子纲’。”

此时，如果是熟悉渔业专业英语的人，已经能几乎完全明白背后的来龙去脉。遗憾的是，我并不熟悉渔业专业英语。

我恍然大悟，回到食品论坛的那个页面搜索“沈子纲”，果然该神秘人同样列出了这对词汇。将两个英文词语在渔业领域的意思交叉对比，可以得知 footrope 指的是渔网底部带有配重以使得网具下沉并张开成特定形状的绳索，而 dangles，如神秘人所言，是缠绕 footrope 之铁链，起到配重与惊起海中的底栖生物以便于打捞的双重作用。

问题是，这个东西为什么会被神秘人称为“沈子纲”呢？如果这是通用的译名或译法，为什么会查询不到任何结果？

此时，如果是对汉字足够敏感的人，已经能从上下文中猜测到正确答案。遗憾的是，我对汉字同样不够敏感。

于是我继续查看“沈子纲”的搜索结果。令人意外的是，这个日文网页提到了“沈子綱”在日文中的存在。到了这一步，在日文汉字的提示下，我终于还是对汉字产生了一定的敏感：这个“沈子纲”，在中国大陆的语境下，是不是应该被写成“沉子纲”呢？

于是我搜索“沉子纲”，得到大量与渔业有关的搜索结果，简单阅读之后确认和之前的 footrope 这个英文词汇指的是同一个东西。结合这一点搜索，可以得知 dangles 所对应的东西并没有一个通用的专名或译法，但或许可称为“垂链”“吊链”“悬垂索具”等等，或者，如一开始的神秘义项所云，是“缠绕沉子纲之铁链”。只是不知为何，食品论坛的神秘人可能受到日语影响，将“沉子纲”写成了“沈子纲”。

Weeknotes 17, Apr 2026 [2026-W17]

This week I have been thinking about the problem of choosing a “best” or “principal” type when performing gradual type inference.

Principal type for gradual type inference

The type inference problem can be described as, given a context $Γ$ and an expression $𝑒$ , find a type $𝑇$ such that $Γ ⊢ 𝑒 : 𝑇$ .

The problem is that, there could be multiple types $𝑇$ that is valid in some sense. For example, a function $𝜆 𝑥 . 𝑥$ satisfies both the type $𝖨𝗇𝗍 \to 𝖨𝗇𝗍$ and $𝖡𝗈𝗈𝗅 \to 𝖡𝗈𝗈𝗅$ intuitively.

In such cases, we want to infer a principal type (I’m using the term “principal” in a loose and informal sense). For example, for the identity function above, we might want to infer something like $\forall 𝛼 . 𝛼 \to 𝛼$ which could be instantiated to the two concrete types.

Here is another example:

class Animal():
  field name :: String

class Cat():
  extends Animal
  field fishes

class Dog():
  extends Animal
  field bones

Given the code above, a function fun (x): x.name might have type Cat -> String, Dog -> String, or even Animal -> Object. but a more suitable type would be Animal -> String. So, for different type systems, how we define the property of being “principal” can vary. For a system with parametric polymorphism, it might mean being able to be instantiated to any other possible type; for a system with subtyping, it might mean being the supertype of any other possible type without going too far to the top type like Object unless necessary. In one word, the type we want is principal with regard to a certain relation.

Now let’s consider the type inference for a gradual type system. Still, there could be multiple types that are valid in some sense, and we want to pick a principal one. The problem now is:

What does “valid” mean?
What does “principal” mean?

Validity can have many interpretations. It could mean static typability, that is, plugging in a valid type yields a gradually well-typed program. For a unification-based type inference system, that means satisfying all the constraints. It may also concern runtime semantics, such as requiring that after plugging in the inferred type, all executions or at least some executions are safe (no cast error, do not diverge, etc.). For our analysis now, let’s choose the typing-based interpretation, that is, it should at least mean not raising a static type error when plugged in.

What about being principal? Intuitively, just like in systems with subtyping we pick the type satisfying certain properties with regard to the subtyping relation, in a gradual type system we should pick the type with certain properties with regard to the precision or materialization relation. Also like subtyping, the precision or materialization relation induces a upper semilattice on the gradual types. So, the problem becomes: given a set $𝑇$ of members of the semilattice $⟨ 𝑆, \leq ⟩$ where all $𝑡 \in 𝑇$ satisfies the validity condition $𝑉 (𝑡)$ , pick a $𝑡 \in 𝑇$ satisfying certain properties. Here the relation $𝑎 \leq 𝑏$ means $𝑎$ is more precise than $𝑏$ , or $𝑎$ materializes $𝑏$ . Note that with that relation and our typability interpretation of validity, $𝑉 (𝑡)$ has the monotone property: if $𝑉 (𝑡_{1})$ and $𝑡_{1} \leq 𝑡_{2}$ , then also $𝑉 (𝑡_{2})$ .

As a hint, we could try to extract some rules from previous literature (notice that the direction of the order relation $⊑$ in the literature is the reverse of our $\leq$ ):

Rules for gradual type inference [000V]

In section 3 of Gradual Typing with Unification-based Inference, the authors discuss some examples where the naive “well-typed after substitution” approach fails. That implies some rules that gradual type inference should follow.

In the following example codes, α is a type variable not in the parametric polymorphism sense, but in the unification-based type inference sense, that is, a variable to be substituted with a gradual type after type inference.

Static conservativity

let f(g: α) = g 1
f 1

The above program would not pass static typecheck, since there is no possible substitution for α. Thus, even if substituting α with ? make the program pass gradual typecheck, such a substitution should not be chosen.

The rule here is that a program can be gradually well-typed if and only if it can be statically well-typed.

Constraint-informativeness preservation

let x: α = x + 1

Substituting α with ? would make the above program pass gradual typecheck, but a more appropriate choice is int.

The rule here is that when a more precise type is possible, a less precise one should not be chosen as the inferred type.

Minimal adequate solution

let f(x: ?) =
    let y: α = x in y

Substituting α with some more precise type such as int won’t trigger a type error during gradual typecheck, since they are consistent with ?. However, doing so blocks the possibility to, for example, apply the function to a boolean. The only appropriate substitution for α is ?.

The rule here is that when multiple types all make the program gradually well-typed, then the chosen type should be less precise than them and be consistent with them, that is, they are all materializations of the chosen type.

The first rule is more connected to the Refined Criteria for Gradual Typing: it simply says that if there are no static types in $𝑇$ , then we should raise a type error. It implies that $𝑇$ has some minimal element(s), i.e. elements that no other elements are smaller than them (different from the least element), and they are all static types since minimal elements that are not static types cannot be in $𝑇$ according to rule 1.

The second rule is more like filtering what is “valid”: from the constraints we know that there is a set $Σ \subseteq 𝑆$ such that for all $𝑡 \in 𝑇$ and for all $𝜎 \in Σ$ , $𝜎$ is less precise than $𝑡$ . For our specific inference problem to be meaningful, a reasonable requirement is that there exist a lower bound of all $𝜎 \in Σ$ with regard to $\leq$ ; otherwise we won’t have a reasonable element to choose as the principal one. That implies that a greatest lower bound $𝜎_{𝗀𝗅𝖻}$ of $Σ$ exists, and it is an upper bound of what we might choose as the principal type. From the perspective of types, all the $𝜎$ s means some information we already know about the type to infer, and their greatest lower bound is the combination of these informations. For example, we may have $Σ = {? \to (𝖨𝗇𝗍 \to ?), ? \to (? \to 𝖨𝗇𝗍)}$ , and $𝜎_{𝗀𝗅𝖻} = ? \to (𝖨𝗇𝗍 \to 𝖨𝗇𝗍)$ .

The third rule makes more sense of “principal.” It implies that if the greatest lower bound of $𝑇$ does not exist or is not in $𝑇$ (i.e. $𝑇$ does not have a least element), then the principal element we choose should be greater than or equal to the least upper bound $\overset{̆}{𝑡}$ of the minimal elements of $𝑇$ . This $\overset{̆}{𝑡}$ sets a lower bound of what we might choose as the principal type. Notice that the minimal elements of $𝑇$ at least contains some static types (implied by rule 1), and any pair of static types are non-comparable, and any static type is also a minimal element in $⟨ 𝑆, \leq ⟩$ , so if the greatest lower bound of $𝑇$ exists and is in $𝑇$ , then that element must be the sole static type in $𝑇$ . If that is the case, intuitively this static type should just be the principal type we infer.

The third rule and second rule combined together gives us another requirement: $\overset{̆}{𝑡}$ should be less than or equal to $𝜎_{𝗀𝗅𝖻}$ . Otherwise we have no reasonable $𝑡$ to choose as the principal one. It is also clear that when the two are equal and they are in $𝑇$ , they are the principal element to choose.

Are $𝜎_{𝗀𝗅𝖻}$ and $\overset{̆}{𝑡}$ in $𝑇$ ? To answer this, we first ask: in what cases would a type be not in $𝑇$ ? Since our notion of “valid” means “not raising type error when plugged in”, then not in $𝑇$ , i.e. not valid, should mean it would raise a type error when plugged in, which in turn means that all the materialization of it (thus all static ones) would raise a type error. So, “valid” in turn means some of its materialization (thus some static ones) would fit. This interpretation immediately tells us that $𝜎_{𝗀𝗅𝖻} \in 𝑇$ and $\overset{̆}{𝑡} \in 𝑇$ .

Since $𝜎_{𝗀𝗅𝖻} \in 𝑇$ and $\overset{̆}{𝑡} \in 𝑇$ , let $𝑇^{'} \subseteq 𝑇$ be the set of all elements in $𝑇$ that is between them, $⟨ 𝑇, \leq ⟩$ form a lattice; more precisely, a sub-lattice of $⟨ 𝑆, \leq ⟩$ . The next question is: how should we choose the principal type out of it?

If $𝑇^{'}$ is a singleton, the answer is very simple. In what cases would $𝑇^{'}$ not be a singleton? That would be the cases where there are materialization of $𝜎_{𝗀𝗅𝖻}$ other than $\overset{̆}{𝑡}$ that would raise a type error when plugged in. What should we choose as the principal type in that case?

The answer is still not clear to me, but I doubt that it would be more like a design choice. If you want to be more tolerant and allow more things to be consistent, you choose $𝜎_{𝗀𝗅𝖻}$ ; if you want to be more precise, you choose $\overset{̆}{𝑡}$ .

From the view of abstract interpretation, every gradual type $𝜏$ can be concretized to a set of static types $𝛾 (𝜏)$ , and every set of static types ${𝑡, \dots}$ can be abstracted to a gradual type $𝛼 ({𝑡, \dots})$ . Obviously, $𝜎_{𝗀𝗅𝖻} = 𝛼 (⋃_{𝑡 \in 𝑇} 𝛾 (𝑡))$ , and $\overset{̆}{𝑡} = 𝛼 (⋂_{𝑡 \in 𝑇} 𝛾 (𝑡))$ .

Also note that this concept of being principal could be somehow orthogonal to other concepts of principal type, such as the subtyping or parametric polymorphism ones we mentioned above. If that is the case, the type inference algorithm need to consider all of them and maybe make some considerations if they are not compatible.

Weeknotes 15, Apr 2026 [2026-W15]

Start writing weeknotes

The benefits of journaling are already widely discussed, but for me, the motivation to do so comes from reading the weeknotes of Jon Sterling. Keeping a journal has several benefits that are particularly relevant to me:

I usually let my mind wander among various ideas but also forget these thoughts easily. Writing things down preserves these thoughts that may show their value later.
I’m a non-native English speaker, so writing regularly helps me sharpen my writing skills.

There are also other general benefits applicable to everyone, like it helps to organize thoughts, provides a sense of accomplishment (that creates a positive feedback loop), and allows one to “think in public” to get feedback from others. I find weeknotes more manageable than daily journals: I’m not ready to make that commitment, and I don’t have enough to say every 24 hours.

Weeknotes 21, May 2026 [2026-W21]

May 24, 2026

NJPLS was fun!

Discussion about gradual typing

Non-English programming languages

The interesting (to me) idea here is to utilize linguistic features of natural languages, contrary to the “symbolism” view of programming language syntax.

ArticleRobust Dynamic Embedding for Gradual Typing [JTTT25]

9
ICFP
Koen Jacobs, Matías Toro, Nicolas Tabareau, Éric Tanter
2025-08-05
10.1145/3747507

Gradual typing has long been advocated as a means to bridge the gap between static and dynamic typing disciplines, enabling a range of use cases such as the gradual migration of existing dynamically typed code to more statically typed code, as well as making advanced static typing disciplines more accessible. To assess whether a given gradual language can effectively support these use cases, several formal properties have been proposed, most notably the refined criteria set forth by Siek et al. One criterion asserts that the dynamic extreme of the spectrum should be expressible in the gradual language, formalized by the existence of an adequate embedding from the corresponding dynamic language. We observe that the existing dynamic embedding criterion does not capture the desirable property of being able to ascribe embedded code to a static type that it semantically satisfies, and ensure reliable interactions with other components within the gradual language. Specifically, we introduce the notion of robustness for gradual terms, meaning that when interacting with any gradual context, runtime failures that may occur ought to be caused by the context, not by the robust term itself. We then formulate the robust dynamic embedding criterion: if a dynamic component semantically satisfies a given static type, then its embedding subsequently ascribed to that static type should be a robust term. We demonstrate that robust dynamic embedding is not implied by any existing metatheoretical property from the literature, and is not upheld by various existing gradual languages. We show that robust dynamic embedding is achievable with a gradualized simply-typed language. All the results are formalized in the Rocq proof assistant. This novel criterion complements the set of criteria for gradual languages and opens several venues for further exploration, in particular for typing disciplines that enforce rich semantic properties.

OnlineGuard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir [CD24]

We define several techniques to extend gradual typing with semantic subtyping, specifically targeting dynamic languages. Focusing on the Elixir programming language, we provide the theoretical foundations for its type system. Our approach demonstrates how to achieve type soundness for gradual typing in existing dynamic languages without modifying their compilation, while still maintaining high precision. This is accomplished through the static detection of “strong functions”, which leverage runtime checks inserted by the programmer or performed by the virtual machine, and through a fine-grained type analysis of pattern-matching expressions with guards.