One of the key aspects of gradual typing is that the same code can execute in two different contexts with different kinds of contracts. For example take the following code:
(ns my-typed
{:lang :core.typed})
(ann my-plus [Num Num -> Num])
(defn my-plus [a b] (+ a b))
(my-plus 2 4)(ns my-untyped
(:require [my-typed :as typ]))
(typ/my-plus 1 2)Here we are defining a typed function my-plus in our typed namespace my-typed, then both use it the same typed context and in an untyped context my-untyped. The question to ask is: where do we need to enforce invariants at runtime?
Well, our first call to my-plus is verified at compile-time via type checking, because it occurs in the typed namespace my-typed. This does not require contracts. However, the my-untyped usage is unchecked by the type checker, so we need to protect my-plus from being passed anything other than two Num arguments.
The way we achieve this is to create two vars for every typed var: one that is named the same as the original var and is fully checked at runtime, and another that has a hidden name and has no contracts to which we rewrite to in typed contexts.
Here is what the previous code looks like after type checking:
(ns my-typed
{:lang :core.typed})
(ann my-plus [Num Num -> Num])
(defn my-plus___typed [a b]
(+ a b))
(def my-plus
(t/cast [Num Num -> Num] my-plus___typed))
(my-plus__typed 2 4)(ns my-untyped
(:require [my-typed :as typ]))
(typ/my-plus 1 2)Notice my-plus does extra checking at runtime and my-plus___typed is fully statically checked. This way typed code interacting with typed code can be rewritten to avoid unnecessary contract checks because we actually control compilation at that point, and all other code pays the runtime verification penalty by default. This is the basic approach of Typed Racket.
This should work, but there are tradeoffs here. Notice my-plus now not only pays for extra contract checks but also an extra var dereference every call. Can't we just duplicate the implementation of my-plus___typed in my-plus to avoid this? I think so, but the tradeoff here is in future alter-var-root and def of my-plus.
For example, say we add tracing to my-plus with tools.trace.
(ns my-typed
{:lang :core.typed}
(:require [clojure.tools.trace :as trace]))
...
(trace/trace-vars my-plus)We can't rewrite this in a typed context because trace-vars is a macro, so this isn't quite what we want. We might want my-plus and my-plus___typed to automatically keep in sync with var validators, functions triggered after a alter-var-root and def. Concretely, if (alter-var-root #'my-plus f) then this synchronisation measures might trigger (alter-var-root #'my-plus___typed f).
An open question is where these validators should be added: should my-plus trigger my-plus__typed, vice-versa, or even both (how do we stop infinite mutual alter-var-roots?).
This is a classic problem in gradual typing that applies to all other constructs definable in both typed and untyped lands. This, however, does not just apply to vars in Clojure: other interesting interactions occur with multimethods, datatypes and records.
What are the different combinations of typed and untyped lands that we can define and use these Clojure constructs? (I think multimethods might have the most potentially interesting story, we will explore that another time).