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

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