Gradual typing for Clojure
frenchy64.github.io
Gradual typing for Clojure
1–10 of 12 posts
Re: Gradual typing for Clojure
#2My 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.
Re: Gradual typing for Clojure
#3My 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…
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).
Re: Gradual typing for Clojure
#4My 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
#5My 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…
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`.
Re: Gradual typing for Clojure
#6I 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...
Re: Gradual typing for Clojure
#7I 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, bu…
Might want to fix that link by removing the rightmost quote. Thanks!
Re: Gradual typing for Clojure
#8My 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.
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.
Re: Gradual typing for Clojure
#9Earlier quoted context omitted.
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...
Re: Gradual typing for Clojure
#10My 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.
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.