eighty-twenty

I don’t know what crack I was smoking the other day, but my implementation of general monads not only does not have the property I claimed for it, viz. that it provides the same level of type-checking as Haskell ahead of execution-time, but it cannot provide such a level of ahead-of-runtime checking, whether the hosting language is eager or lazy.

To see the first, try the following example:

> (run-io (mlet* ((_ (mdisplay "HERE\n"))
                  (_ sget))
            (return 232)))
HERE
wrong monad-class ((mclass #5(struct:<monad-class> io [...]))
      (m #3(struct:<monad> #5(struct:<monad-class> state [...]) [...]))) 

Note how an action is performed before the type error is detected. In general, it is not possible to detect the type-error ahead of time without abstract interpretation of the level of sophistication that Haskell’s type-checker provides, as the following example demonstrates:

> (define (goes-wrong)
    (run-io (mlet* ((val mread))
              (if val
                  (mlet* ((_ (mdisplay "Was true\n"))) (return 'apples))
                  'bananas)))) ;; Note: missing "(return ...)"!
> (goes-wrong)
#t
Was true
apples
> (goes-wrong)
#f
<monad>-ref: expects type <struct:<monad>> as 1st argument, given: bananas; other arguments were: 0
[...]

The problem is that the system can decide how to continue based on I/O performed at runtime, and so the composition performed by bind cannot be checked until after the left-hand-side has been fully evaluated. [Aside: the <monad>-ref error was a symptom of the unexpected problem described below — now that the code has been fixed, it instead complains “not a monad bananas”, as it should.]

This affects all my monad implementations, not just the IO monad:

> (run-st (mlet* ((a sget)
                  (b (mdisplay "OH NO\n"))
                  (_ (sput 4)))
            (return (+ a 1)))
          2)
OH NO
(3 . 4)

Actually, and this is unexpected ("OH NO" indeed!), here it’s even worse than just not catching the type-error before any actions have executed: it isn’t catching the error at all. Here’s what that mlet* expands into:

(>>= sget
     (lambda (a)
       (>>= (mdisplay "OH NO\n")
            (lambda (b)
              (>>= (sput 4)
                   (lambda (_)
                     (return (+ a 1))))))))

My implementation of >>= isn’t “reaching into the lambda” in the case of the IO monad. [Interlude; sounds of programming from behind the curtain.] The problem was my use of the (bad) “delayed monad” idea in implementing the IO monad — I’ve just replaced that idea with a more explicit representation of a delayed action, and the code now behaves as I expected. How embarrassing! Here’s the trace now that I’ve fixed that problem:

> (mlet* ((a sget)
          (b (mdisplay "OH NO\n"))
          (_ (sput 4)))
    (return (+ a 1)))
#3(struct:<monad> #5(struct:<monad-class> state [...]) [...])

This shows that before we run the monad, it appears to be a well-behaved state monad instance. Running it now causes the error to be detected:

> (run-st (mlet* ((a sget)
                  (b (mdisplay "OH NO\n"))
                  (_ (sput 4)))
            (return (+ a 1)))
          2)
wrong monad-class ((mclass #5(struct:<monad-class> state [...]))
      (m #3(struct:<monad> #5(struct:<monad-class> io [...]) [...]))) 

This demonstrates what I was hoping to show above, before I was derailed by the delayed-monad issue: that the impossibility of using this technique to type-check monad assemblies ahead of any actions being performed applies to all monad kinds, not just the IO monad. Of course, it’s less of a problem for non-side-effecting monads, such as the state monad, since performing an action (in the case immediately above, reading the hidden state variable) in such a monad has no effect on the outside world by the time the type-error is detected.

In conclusion, I was mistaken about Scheme’s ability to achieve the same level of ahead-of-execution type-checking as Haskell manages — I don’t believe it to be possible without essentially Haskell-equivalent abstract-interpretation machinery bolted on to the language. Nonetheless, the library I’ve developed does catch type errors eventually — so long as the faulty code is eventually run! This is no worse than regular dynamically-typed language code, and is still a useful system, so I’m not completely disappointed. I will still be able to use the idea to structure side-effects in ThiNG.