Gradual typing for Clojure(frenchy64.github.io)

102 pointsby michaelsbradley11 yıl önce11 comments

frenchy64.github.io

http://frenchy64.github.io/2015/06/19/gradual-typing.html

2 comments

lkrubner11 yıl önce

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

dllthomas11 yıl önce

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.

calibraxis11 yıl önce

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

tel11 yıl önce

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.

ambrosebs11 yıl önce

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

millstone11 yıl önce

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

ambrosebs11 yıl önce

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

millstone11 yıl önce

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.

ambrosebs11 yıl önce

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.

tel11 yıl önce

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

dllthomas11 yıl önce

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.