Typed Clojure by Example

http://nathanic.org/posts/2013/typed-clojure-tour/

by austengary • 13 years ago

91 16 13 years ago

BMarkmann• 13 years ago

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.

sherbondy• 13 years ago

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

tommmmmm• 13 years ago

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

ambrosebs6• 13 years ago

No reason.

dilap3• 13 years ago

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

ambrosebs6• 13 years ago

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.

dilap3• 13 years ago

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

tel• 13 years ago

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.

batgaijin• 13 years ago

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

ambrosebs6• 13 years ago

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.

terranstyler• 13 years ago

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?

ambrosebs6• 13 years ago

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.

gecko• 13 years ago

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

ambrosebs6• 13 years ago

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.

Typed Clojure by Example

Related Stories