A challenge for typed Clojure

gistfile1.txt

; A simple example for using the writer monad

(domonad (writer-m "")
         [x (m-result 1)
          _ (write "first step\n")
          y (m-result 2)
          _ (write "second step\n")]
         (+ x y))

; where write (defined in algo.monads) is:

(defmonadfn write [v]
  (let [[_ a] (m-result nil)]
    [nil (writer-m-add a v)]))

; Now suppose we move to a monad system based on types/protocols.
; We'd have

(domonad
    [x (m-result 1)
     _ (write "first step\n")
     y (m-result 2)
     _ (write "second step\n")]
    (+ x y))

; plus type annotations in the various definitions. Can typed Clojure infer
; that (m-result 1) must return the type representing the writer monad with
; a string accumulator from the known facts which are:
; 1) The return type of write is "writer monad type"
; 2) The argument of write is a string.
; 3) The m-bind chain into which the domonad macro expands can only
;    be made type-consistent if the return type of m-result is the
;    the same as the return type of (write "").

The point of my example is not to improve typing of protocol monads (which should indeed not present any difficulty), but to see if typed Clojure can combine the full genericity of algo.monads with the performance advantages of protocol monads. Apparently the answer is no.

Ah yes. I'm pretty sure I agree with that.