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.
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).
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.
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.
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.
There would be annotations in the same places as Typed Clojure, except :no-check would be replaced by type soundness-preserving runtime assertions. There would be no need for :no-check anyway; Typed Racket's base annotations are complete AFAIK.
I will tiptoe carefully around the issue you're bringing up and point out that the styles of type checking provided by Dialyzer and Typed Clojure are pretty different.
http://www.cs.colorado.edu/~siek/pubs/pubs/2006/siek06:_grad...