This is really interesting/cool looking stuff. Clojure has piqued my interest for a while, but the longer I've been programming, the less I want to have to deal w/ dynamically-typed languages.

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

I guess the '... b' is really just saying "continue the sequence until the end"? Like you could imagine a syntax where instead of ...b it was just "...", as in "[[a b ... -> c] (NonEmptySeqable a) (NonEmptySeqable b) ... -> (NonEmptyLazySeq c)".

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

Clojure's map takes at least 2 arguments, so that's why we have an extra "a".

I also commented on the blog post explaining the terms I used.

Ah, that makes sense.

This is a great tutorial -- one of the best for Typed Clojure I've come across. The parallels to Haskell finally made some of the Clojure implementation of typing sink in for me.

Agreed. After reading this, I finally feel like I'm beginning to grok Typed Clojure. Will probably recommend this article to newcomers to the library, especially if they have a Haskell/ML background. Hoping to take my new understanding and write a simple typed raytracer modeled after Htrace (http://nobugs.org/developer/htrace/) when I've got a spare moment. Or maybe someone could beat me to the punch. :P

I'm am always so excited by Typed Clojure. It's very interesting to see what you can do with an optional, add-on-type type system that is allowed to be flexible with runtime behavior.

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.

I follow typed Clojure with big interest, however, there is one thing I didn't read anything about: Speed.

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

Is there a reason that in clojure.core/map, the second type declaration uses (U nil (Seqable a)) instead of (Option (Seqable a))?

No reason.

I'm kind of surprised how close Typed Clojure is to Typed Racket. At a quick glance, they're almost indistinguishable.

It shouldn't be too surprising given the similarities between Clojure and Racket.

Typed Clojure and Typed Racket are very closely related in theory and implementation.

does typed clojure support dependent types? I would assume like cl it's powerful enough to.

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.