§ The Gradual Guarantees
- Says that static and dynamic type systems match up, and thus interpolating makes sense.
- The ur-example is
(\y y) ((\x x) 42)). - This program dynamically executes and produces
42.
§ statically correct programm
- The correctly type annotated program
(\(y : Int) y) ((\(x : Int) x) 42)will pass the type checker, and run to produce the same value 42.
def f(x : Int): return x
def g(y): return y
a = 42
b = f(a)
b' = upcast b Int # Inferred b' : Int
c = g(b')
§ statically incorrect programm
- Consider the program
(\y y) ((\(x : Bool) x) 42). This elaborates into:
# Inferred f : Bool -> Any
def f(x : Bool): return x
# Inferred g: Any -> Any
def g(y): return y
a = 42 # Inferred a : Int
b = f(a) # Type error, f : Bool -> Any mismatch argument a : Int
c = g(b) # See that this is type-correct, (b : Any), (g : Any -> Any)
§ dynamically incorrect programm
- Consider the program
(\(y : Bool) y) ((\x x) 42). This elaborates into:
# Inferred f : Any -> Any
def f(x): return x
# Inferred g: Bool -> Any
def g(y : Bool): return y
a = 42 # Inferred a : Int
b = f(a) # Inferred b : Any
b' = upcast b Bool # dynamic error at upcast, since at runtime, (b := 42)
c = g(b)
§ What have we learnt?
- If we add all the types, we get a type checker that passes which accepts correct programs (fully anootated).
- Some ways of adding type information will throw static type errors
- Some ways of adding types will give us a runtime error from upcasts .
- Since the upcasts are inserted "in between" calls to the statically typed functions, we never get an error inside a statically typed function.
- In particular, we can state that the error arises from the call to the dynamic functions.
§ Gradual guarantees
- if a program is well typed, removing types keeps the program well typed.
- If a well typed program evaluates to a value, then removing types from this program also evaluates to the same value.
- adding type annotations can add either static errors, or dynamic errors from untyped code . Typed code that passes static type checking cannot create new errors dynamically.
§ Why are the gradual guarantees useful?
- If the gradual guarantees are true, then we know that we can "trust" the static types: if a value
x has type Nat, then at runtime, it will only be of type Nat (if passed an incorrect value, the cast before the assignment will make sure that no non- Nat value flows into x). This means that we can, for e.g., write a compiler that makes the statically typed portion of the program way faster! - Contrast this to the case where we run the program
(\(y : Bool) y) ((\x. x) 42) and produce the result 42. A compiler count not produce faster code, because y at runtime has value 42 which is an integer, not a boolean! - In the neat article by Jeremy Siek on Is typescript gradually typed , he describes the academic version with gradual guarantees as "level 2", and the python/typescripe like behaviour as "level 1". To quote:
level 1 gradual typing does not provide run-time support for catching broken invariants, such as deriv's expectation that its arguments have type string. Thus, a TypeScript programmer that really wants to enforce such an invariant would need to add code to check the type of the argument, a common practice today in JavaScript.
Level 2 gradual typing ensures that the value stored in a variable is consistent with the variable's static type and it provides the run-time checking to catch when this invariant is about to be broken. Thus, level 2 gradual typing removes the need for hand-written type tests. Also, level 2 gradual typing opens up the possibility of compiling statically-typed regions of a program in a more efficient, type-specific manner. (This is an active area of my current research.) The disadvantages of level 2 gradual typing are the run-time overhead from cast checking and the increased implementation complexity.
Level 3 gradual typing improves on level 2 by adding blame tracking, thereby improving the diagnostic errors reported when a cast fails. The extra cost of blame tracking is not very significant, so I would always suggest level 3 over level 2.
§ References