11
$\begingroup$

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?

$\endgroup$

2 Answers 2

10
$\begingroup$

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. showed that a high-performance optimising virtual machine could eliminate almost all of the cost of transient checks, and Richards et al. 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 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<String> 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.

$\endgroup$
6
  • $\begingroup$ "x instanceof List is probably ok, but `x instanceof List isn't." -- Formatting error? Those look like the same thing. $\endgroup$
    – Bbrk24
    May 19, 2023 at 0:51
  • $\begingroup$ @Bbrk24 Yep, thanks. Missing backtick ate the <String> part. $\endgroup$
    – Michael Homer
    May 19, 2023 at 0:53
  • $\begingroup$ "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? $\endgroup$
    – kaya3
    May 19, 2023 at 2:43
  • 1
    $\begingroup$ @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). $\endgroup$
    – Michael Homer
    May 19, 2023 at 3:01
  • 1
    $\begingroup$ @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. $\endgroup$
    – Michael Homer
    May 19, 2023 at 3:21
3
$\begingroup$

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:

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .