My understanding is that gradual typing, indeed all of the interesting cases considered here, can be well understood through the introduction of an `Any` type to the normal typed language. A contract is then a coercion `Any -> Maybe t` for some subtype of `Any`, `t`, which is being demanded. The interesting technology thus is the "injection" `t -> Any` which is universally valid but appears to have its own contract a…
I don't think the above scheme works, except for primitive cases. Say in your example the type t is Int->Int. The Halting Problem says we cannot determine if a given dynamically typed function matches this type: we must actually run the function and then look at the result. So we cannot do the type checking at the point of "unwrapping" the Maybe.
Re: Gradual typing for Clojure
#11Yeah, when wrapping `(Int -> Int) -> Any` you would need to package it up with a proof of its type if you want to unwrap it and check. A weaker promise might be merely to unpack `Any` into `Dyn -> Dyn` which states only that we have a function and nothing of its domain or range. Those would have to be unwrapped specifically later. A function `Dyn` to `Dyn` probably doesn't evaluate its argument's type anyway so it could fail at runtime regardless. The receiver of its output would then be required to unwrap the `Dyn` and check its type (if needed).