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.
`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.
Typed Clojure is currently static analysis only and offers no automatic speed improvements. It has the nice property that code will compile and run no matter what the type checker thinks.
To type check Clojure idioms we use techniques that resemble light-weight dependent types. No particular attempt is made to go beyond the minimum required for checking certain idioms.
We can express lengths of sequences for example, but they only support explicit lengths: you can't put a type variable in the length position.
The dotted type-variable on the right hand side of ... is what ensures both sets of dots get instantiated with the same sequence of types.
Both sides of b ... b are actually completely different. The left is a type (called a "pre-type") and the right is a dotted type variable currently in scope.
The trick is that the dotted type-variable is also scoped as a normal free variable in the pre-type.
It might help thinking of "b ... b" as expanding to "b1 b2 b3 b4 b5", where each is a fresh type variable.
Then, consider "(NonEmptySeqable b) ... b" as expanding to "(NonEmptySeqable b1) (NonEmptySeqable b2) (NonEmptySeqable b3) (NonEmptySeqable b4) (NonEmptySeqable b5)".
The b's "match up" pairwise, but they're quite different than what you might expect.
Yup, makes sense (well, paragraph three onward -- I don't know enough yet to understand stuff like "dotted type-variable", but I think the general way this is working is clear :).
So would this definition be equivalent and work?
(ann clojure.core/map
(All [c b ...]
(Fn [[b ... b -> c]
(NonEmptySeqable b) ... b
-> (NonEmptyLazySeq c)]
[[b ... b -> c]
(U nil (Seqable b)) ... b
-> (LazySeq c)])))
| The b's "match up" pairwise, but they're quite different than what you might expect.
Makes sense, but slightly confusing at first, 'cuz the b before the ... is a different thing than the b after.
Thanks for the response, and typed clojure. I think this is going to be the thing that finally gets me to start playing with clojure. :)
The information on what needs annotating isn't quite complete: loops and some other macros need annotations.
I'm probably responsible for the thinking that annotations are only needed for "top levels and function parameters". I usually forget about the other ones, but I think those two are the most significant.
Rich hasn't been directly involved, aside from providing encouragement.
Almost all the design/implementation work was done via Typed Racket anyway. I stole a lot of it and spent most of the time on Clojure-specific problems.
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.