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.