I gave $150 and I hope every other Clojure developer does the same. I think this project is very important. Having a clean bridge from dynamic programing to typed programming gives us an important way to document our own learning process.
In my blog post "How ignorant am I, and how do I formally specify that in my code?" I tried to communicate why I think this is important. I am not sure I found the correct words, but the idea is that when I start on a problem, especially a problem I've never dealt with before, I don't want to specify a contract because I consider myself too ignorant to specify a contract. The flip side of that is when you see a contract in my code, you know that you are looking at a bit of code where I feel I have overcome ignorance and learned enough to specify something strict.
Interesting. I love the notion of specifying (implicitly or explicitly) your level of confidence in code or model.
That said, I find my experience differs around the following:
"[W]hen I start on a problem, especially a problem I've never dealt with before, I don't want to specify a contract because I consider myself too ignorant to specify a contract."
I find that's precisely when I find types the most valuable. I can start to sketch out the properties that I think should hold, and the type checker helps me think ahead and catch inconsistencies before I've coded all the way to them.
It also helps me write not-quite-right code at the outset with confidence, knowing that as I discover that I'm wrong about things I will have assistance in finding where I am wrong about things, and hopefully more quickly get to sufficiently right and sufficiently complete code.
I recognize that much of this is subjective, may well not apply to everyone, and might even be wrong (it's a hard thing to measure)... but I thought I'd share my POV.
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.
In my blog post "How ignorant am I, and how do I formally specify that in my code?" I tried to communicate why I think this is important. I am not sure I found the correct words, but the idea is that when I start on a problem, especially a problem I've never dealt with before, I don't want to specify a contract because I consider myself too ignorant to specify a contract. The flip side of that is when you see a contract in my code, you know that you are looking at a bit of code where I feel I have overcome ignorance and learned enough to specify something strict.
"http://www.smashcompany.com/technology/how-ignorant-am-i-and...