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 attached as well which attempts to prevent a consume of such an `Any` from using the type `t` incorrectly.
`Any` is also often called `Dyn` or `Dynamic` in normal typed languages, which is slightly different to `Any` here (core.typed's `Any` is the supertype to all types, `Dyn` is usually both the super and subtype to all types).
I don't think this is the same. `Dynamic` is an object along with its reified type. Now consider a dynamically typed function that returns either a String or an Int, according to a Bool parameter. This function ought to be statically type-able as Bool->String OR Bool->Int. It does not have a single static type, so it cannot be represented as `Dynamic`.
I went back to Siek & Taha's original formulation and they have a nice examples section in 5.3 of some interesting higher-order cases with Dyn, that better demonstrates than my clumsy attempt.
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.
Right, I think when you have a Dyn, you import all untyped code as type Dyn or containing Dyn. Then the idea is, when you unwrap a Dyn function at runtime, to distribute the function checks to the domain and range of the function.
Say you had some untyped function `f` that is Dyn -> Dyn.
(defn f [a :- Dyn] :- Dyn
a)
Running
(inc (f 1))
would wrap 1 in Dyn, then a Dyn exits as a return value, so no further wrapping is needed. Now it's `inc`'s responsibility to ensure it's really being passed a number, so it unwraps the Dyn and finds an int inside.
So you're right - it only works with first-order values without this kind of machinery, which end up looking pretty much like what I talk about in the article.
Yeah, 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).
Dyn doesn't have to lose the fact that it once held (Int -> Int). If you have a function that is (Dyn -> Dyn), then it's true that you can't get (Int -> Int) out of that, but you don't actually have one of those so that shouldn't be surprising.
The interesting technology thus is the "injection" `t -> Any` which is universally valid but appears to have its own contract attached as well which attempts to prevent a consume of such an `Any` from using the type `t` incorrectly.