The ability to type the variadic map in particular seemed awesome, though I agree the syntax was weird:
[[a b ... b -> c] (NonEmptySeqable a) (NonEmptySeqable b) ... b -> (NonEmptyLazySeq c)]
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.
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)])))
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. :)
I ask because if my untyped program is wrong, I debug it until it is right and at that point there seems to be no difference anymore between typed and untyped clojure.
TLDR:
- Does it improve speed (in comparison to "type hinted" clojure?)
- Are there other advantages of Typed Clojure other than compile time errors that I am unaware of?
Typed Clojure and Typed Racket are very closely related in theory and implementation.
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.
I'm undoubtedly addicted to the full static assertions that Haskell's type system provides, but some elements of Typed Clojure are expressive enough to remind me of Agda or Idris.