<p>Statically-typed languages specify the types of variables and functions and reject programs they know won't work before they run. Dynamically-typed languages don't include these annotations or checks, and let any program run as far as it can. &quot;Gradually typed&quot; languages are somewhere in the middle.</p>
<p>I understand that the programmer can mix typed and untyped code together, but what does that imply for what the language does at run time? What sort of language do I end up with?</p>

<static-typing><dynamic-typing><gradual-typing>
What are the run-time implications of gradual typing?
<p>It's instructive to look at the gradually typed languages that have emerged over the past decade or so. In particular, they are often extensions to dynamically typed languages:</p>
<ul>
<li><a href="https://hacklang.org" rel="nofollow noreferrer">Hack</a> extends PHP</li>
<li><a href="https://www.modular.com/mojo" rel="nofollow noreferrer">Mojo</a> extends Python</li>
<li><a href="https://www.typescriptlang.org" rel="nofollow noreferrer">TypeScript</a> extends JavaScript</li>
<li><a href="https://julialang.org" rel="nofollow noreferrer">Julia</a> is influenced by MATLAB</li>
</ul>
<p>Far less common is a statically typed language that has been augmented with the ability to determine types at runtime. The takeaway is that gradual typing allows user to become more precise/structured/rigorous with their code as they get more experience developing their applications.</p>

CC BY-SA 4.0
2023-05-19T01:09:15.997Z
2023-05-19T01:09:15.997Z
chrisaycock
<p>There are a few different approaches to gradual typing, and some have more impact on the language than others. One major cluster is <em>sound</em> gradual typing, which wants to ensure that the static type annotations are correct even when values from dynamically-typed code enters them. This requires dynamic checks and run-time errors.</p>
<p>Another major cluster only enforces types statically where present, and doesn't do anything with them at run time. These are especially common when adding static types onto an existing dynamically-typed language, as in TypeScript. Some people consider the term &quot;gradual typing&quot; to mean only <em>sound</em> gradual typing, and only refer to the others as &quot;optional typing&quot;; this can be a bit of a fight that I want to sidestep here.</p>
<p>If you're looking at one of the variants with no dynamic checking then the run-time effects are <em>almost</em> nil, but for strictly being &quot;gradual&quot; there are a couple of language-level impacts that do affect run-time behaviour, addressed below. The next section addresses only the sound systems with run-time checking, and we'll return to the language-design elements at the end.</p>
<h1>Dynamic enforcement?</h1>
<p>There are several different strategies for run-time checks, trading off different implementation and behavioural traits. Three of particular note were identified by Vitousek et al. in <em>Design and Evaluation of Gradual Typing for Python</em>:</p>
<ul>
<li>The <em>guarded</em> semantics puts a <strong>proxy wrapper around a value</strong> when it passes from dynamically-typed code to statically-typed code. The statically-typed code only accesses the wrapper object, and the wrapper performs the type checking. Typed Racket follows this approach, but uses <em>chaperones</em> that avoid making the proxy detectable to code. Other references to the same object are not wrapped up, and it's unwrapped when handed back to untyped code.</li>
<li>The <em>transient</em> semantics checks that the value's type is <strong>consistent with the static type when it passes through a type annotation</strong>, but doesn't hold on to that information for later. Further interactions that invalidate the type may go undetected, and there may be more checks than needed.</li>
<li>The <em>monotonic</em> semantics <strong>permanently modifies the object itself</strong> to know what type it's expected to have. These modifications persist through the whole program and all references to that object, including ones that never went into static code, and including after the original static reference is obsolete.</li>
</ul>
<p>Many variations on these are possible, and others. The ideal is to ensure that purely static code never has type errors, and run-time errors can be blamed on a piece of dynamically-typed code.</p>
<h2>Performance</h2>
<p>Making these run-time checks can be expensive, to the point of one system being described as &quot;only 8,000 times slower&quot;, but these costs can be mitigated. The different enforcement strategies have different trade-offs, and so does the number of different type boundaries: the more places you have to check things, the more work there is, so allowing only whole modules to be typed or untyped can be easier than allowing toggling individual annotations.</p>
<p>The transient semantics is generally regarded as having the worst performance, with many redundant checks, though <a href="https://drops.dagstuhl.de/opus/volltexte/2019/10797/pdf/LIPIcs-ECOOP-2019-5.pdf" rel="nofollow noreferrer">Roberts et al.</a> showed that a high-performance optimising virtual machine could eliminate almost all of the cost of transient checks, and <a href="https://dl.acm.org/doi/10.1145/3133879" rel="nofollow noreferrer">Richards et al.</a> showed the same for the monotonic semantics. Optimisations of the chaperones in Typed Racket have produced very low overheads. All of these optimisations have real engineering costs and you should expect some level of slowdown, but it may well be manageable for the application domain of the language.</p>
<p>These optimisations can generally be implemented later on, but things like advanced chaperones are very invasive, so you'd probably want to commit to that approach early.</p>
<h1>Language effects at run time</h1>
<p>One defining point in <a href="https://drops.dagstuhl.de/opus/volltexte/2015/5031/pdf/21.pdf" rel="nofollow noreferrer">Siek et al.'s <em>Refined Criteria for Gradual Typing</em></a> is the <em>Gradual Guarantee</em>: given a runnable gradually-typed program with at least one type annotation, <strong>removing a type annotation doesn't change the behaviour of the program</strong>.
The Gradual Guarantee imposes some unexpected restrictions on what other features the language can have that do have some run-time effects, <em>even if</em> the types aren't dynamically enforced.</p>
<p>In particular, <strong>the language can't have any features that cause the behaviour to change based on type annotations</strong>. That includes things like <code>instanceof</code> or typecase pattern-matching with higher-order types: <code>x instanceof List</code> is probably ok, but <code>x instanceof List&lt;String&gt;</code> isn't, because removing the <code>String</code> annotation would cause a different branch to be taken. In a structural type system, <em>every</em> type test is higher-order, so you can't have those features at all.</p>
<p>It also rules out some uses of constructs like Haskell's <code>newtype</code>, where the annotated type is used to provide different behaviour or class instances.</p>
<p>On the other hand, nothing says you actually <em>have</em> to be gradually-typed under these complete criteria, so a language could include those features anyway; using the label is only a broad branding exercise anyway.</p>

CC BY-SA 4.0
2023-05-19T00:42:56.627Z
2023-05-31T05:53:17.977Z
2023-05-31T05:53:17.977Z
Michael Homer
CC BY-SA 4.0
2023-05-19T00:51:59.683Z
"`x instanceof List` is probably ok, but `x instanceof List isn't." -- Formatting error? Those look like the same thing.
Bbrk24
CC BY-SA 4.0
2023-05-19T00:53:25.227Z
@Bbrk24 Yep, thanks. Missing backtick ate the `<String>` part.
Michael Homer
CC BY-SA 4.0
2023-05-19T02:43:33.173Z
*"in a sound gradual system some sort of run-time checking happens when typed code interacts with untyped code and reports any type mismatches."* This is interesting; I'm familiar with gradual typing only via Typescript and Python, where there is explicitly no such run-time checking. Of course, Typescript's type system is famously not sound, and I'm not sure about Python but I would guess none of the third-party static checkers for it are fully sound. Are there any good examples of gradually typed languages which do have sound type systems and require these runtime checks?
kaya3
CC BY-SA 4.0
2023-05-19T03:01:23.860Z
@kaya3 The unchecked systems are what Siek has referred to as "level 1 gradual typing" and are frequently just excluded from graduality at all at this point — these are the ones that can be called *optional typing* instead to distinguish them, but both terms are still in use in practice; the checked version can also be specified as "*sound* gradual typing".  I am trying to sidestep that fight. Typed Racket was the first significant sound gradual system, and there have been sound implementations of gradual typing for Python (Reticulated Python in Vitousek et al. originated monotonic semantics).
Michael Homer
CC BY-SA 4.0
2023-05-19T03:19:47.447Z
Thanks ─ I didn't mean to invoke a fight, was just trying to relate the information in your answer to what I previously knew. I have seen the term "optional typing" before in reference to Typescript, but I didn't know about this distinction.
kaya3
CC BY-SA 4.0
2023-05-19T03:21:17.840Z
@kaya3 I didn't think you were! I probably should put more mention of those approaches in the answer, though  it's gotten pretty lengthy as it is.
Michael Homer
# What are the run-time implications of gradual typing?
Posted by: username_0 on 2023-05-19
Statically-typed languages specify the types of variables and functions and reject programs they know won't work before they run. Dynamically-typed languages don't include these annotations or checks, and let any program run as far as it can. "Gradually typed" languages are somewhere in the middle.

I understand that the programmer can mix typed and untyped code together, but what does that imply for what the language does at run time? What sort of language do I end up with?
**Tags:** static-typing dynamic-typing gradual-typing
---
## 2 answers
### Answer by username_0 on 2023-05-19. Score: 10
There are a few different approaches to gradual typing, and some have more impact on the language than others. One major cluster is *sound* gradual typing, which wants to ensure that the static type annotations are correct even when values from dynamically-typed code enters them. This requires dynamic checks and run-time errors.

Another major cluster only enforces types statically where present, and doesn't do anything with them at run time. These are especially common when adding static types onto an existing dynamically-typed language, as in TypeScript. Some people consider the term "gradual typing" to mean only *sound* gradual typing, and only refer to the others as "optional typing"; this can be a bit of a fight that I want to sidestep here.

If you're looking at one of the variants with no dynamic checking then the run-time effects are *almost* nil, but for strictly being "gradual" there are a couple of language-level impacts that do affect run-time behaviour, addressed below. The next section addresses only the sound systems with run-time checking, and we'll return to the language-design elements at the end.

# Dynamic enforcement?

There are several different strategies for run-time checks, trading off different implementation and behavioural traits. Three of particular note were identified by Vitousek et al. in *Design and Evaluation of Gradual Typing for Python*:

* The *guarded* semantics puts a **proxy wrapper around a value** when it passes from dynamically-typed code to statically-typed code. The statically-typed code only accesses the wrapper object, and the wrapper performs the type checking. Typed Racket follows this approach, but uses *chaperones* that avoid making the proxy detectable to code. Other references to the same object are not wrapped up, and it's unwrapped when handed back to untyped code.
* The *transient* semantics checks that the value's type is **consistent with the static type when it passes through a type annotation**, but doesn't hold on to that information for later. Further interactions that invalidate the type may go undetected, and there may be more checks than needed.
* The *monotonic* semantics **permanently modifies the object itself** to know what type it's expected to have. These modifications persist through the whole program and all references to that object, including ones that never went into static code, and including after the original static reference is obsolete.

Many variations on these are possible, and others. The ideal is to ensure that purely static code never has type errors, and run-time errors can be blamed on a piece of dynamically-typed code.

## Performance

Making these run-time checks can be expensive, to the point of one system being described as "only 8,000 times slower", but these costs can be mitigated. The different enforcement strategies have different trade-offs, and so does the number of different type boundaries: the more places you have to check things, the more work there is, so allowing only whole modules to be typed or untyped can be easier than allowing toggling individual annotations.

The transient semantics is generally regarded as having the worst performance, with many redundant checks, though [Roberts et al.](https://drops.dagstuhl.de/opus/volltexte/2019/10797/pdf/LIPIcs-ECOOP-2019-5.pdf) showed that a high-performance optimising virtual machine could eliminate almost all of the cost of transient checks, and [Richards et al.](https://dl.acm.org/doi/10.1145/3133879) showed the same for the monotonic semantics. Optimisations of the chaperones in Typed Racket have produced very low overheads. All of these optimisations have real engineering costs and you should expect some level of slowdown, but it may well be manageable for the application domain of the language.

These optimisations can generally be implemented later on, but things like advanced chaperones are very invasive, so you'd probably want to commit to that approach early.

# Language effects at run time

One defining point in [Siek et al.'s *Refined Criteria for Gradual Typing*](https://drops.dagstuhl.de/opus/volltexte/2015/5031/pdf/21.pdf) is the *Gradual Guarantee*: given a runnable gradually-typed program with at least one type annotation, **removing a type annotation doesn't change the behaviour of the program**.
The Gradual Guarantee imposes some unexpected restrictions on what other features the language can have that do have some run-time effects, *even if* the types aren't dynamically enforced.

In particular, **the language can't have any features that cause the behaviour to change based on type annotations**. That includes things like `instanceof` or typecase pattern-matching with higher-order types: `x instanceof List` is probably ok, but `x instanceof List` isn't, because removing the `String` annotation would cause a different branch to be taken. In a structural type system, *every* type test is higher-order, so you can't have those features at all.

It also rules out some uses of constructs like Haskell's `newtype`, where the annotated type is used to provide different behaviour or class instances.

On the other hand, nothing says you actually *have* to be gradually-typed under these complete criteria, so a language could include those features anyway; using the label is only a broad branding exercise anyway.
> **Comments:**
> **username_2** (2023-05-19): "`x instanceof List` is probably ok, but `x instanceof List isn't." -- Formatting error? Those look like the same thing.  
> **username_0** (2023-05-19): @Bbrk24 Yep, thanks. Missing backtick ate the `<String>` part.  
> **username_3** (2023-05-19): *"in a sound gradual system some sort of run-time checking happens when typed code interacts with untyped code and reports any type mismatches."* This is interesting; I'm familiar with gradual typing only via Typescript and Python, where there is explicitly no such run-time checking. Of course, Typescript's type system is famously not sound, and I'm not sure about Python but I would guess none of the third-party static checkers for it are fully sound. Are there any good examples of gradually typed languages which do have sound type systems and require these runtime checks?  
> **username_0** (2023-05-19): @kaya3 The unchecked systems are what Siek has referred to as "level 1 gradual typing" and are frequently just excluded from graduality at all at this point — these are the ones that can be called *optional typing* instead to distinguish them, but both terms are still in use in practice; the checked version can also be specified as "*sound* gradual typing".  I am trying to sidestep that fight. Typed Racket was the first significant sound gradual system, and there have been sound implementations of gradual typing for Python (Reticulated Python in Vitousek et al. originated monotonic semantics).  
> **username_3** (2023-05-19): Thanks ─ I didn't mean to invoke a fight, was just trying to relate the information in your answer to what I previously knew. I have seen the term "optional typing" before in reference to Typescript, but I didn't know about this distinction.  
> **username_0** (2023-05-19): @kaya3 I didn't think you were! I probably should put more mention of those approaches in the answer, though  it's gotten pretty lengthy as it is.  
---
### Answer by username_1 on 2023-05-19. Score: 3
It's instructive to look at the gradually typed languages that have emerged over the past decade or so. In particular, they are often extensions to dynamically typed languages:

* [Hack](https://hacklang.org) extends PHP
* [Mojo](https://www.modular.com/mojo) extends Python
* [TypeScript](https://www.typescriptlang.org) extends JavaScript
* [Julia](https://julialang.org) is influenced by MATLAB

Far less common is a statically typed language that has been augmented with the ability to determine types at runtime. The takeaway is that gradual typing allows user to become more precise/structured/rigorous with their code as they get more experience developing their applications.
---
