Gradual typing for Clojure | Hacker News Reader

Gradual typing for Clojure

frenchy64.github.io

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.

"http://www.smashcompany.com/technology/how-ignorant-am-i-and...

Might want to fix that link by removing the rightmost quote. Thanks!

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.

Great point.

`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.

http://www.cs.colorado.edu/~siek/pubs/pubs/2006/siek06:_grad...

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.

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.

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).

Reply on news.ycombinator.com