Must a Language that Implements Monads be Statically Typed?

Question

I am learning functional programming style. In Don't Fear the Monads, Brian Beckman gave a brilliant introduction about Monad. He mentioned that Monad is about composition of functions so as to address complexity.

A Monad includes a unit function that transfers type T to an amplified type M(T); and a Bind function that, given function from T to M(U), transforms type M(T) to another type M(U). (U can be T, but is not necessarily).

In my understanding, the language implementing monad should be type-checked statically. Otherwise, type errors cannot be found during compilation and "Complexity" is not controlled. Is my understanding correct?

Answer 1

There are lots of implementations of monads in dynamically typed languages:

• The Maybe Monad in Ruby
• OO Monads and Ruby (site is down, but the article is available in the Internet Archive's Wayback Machine)
• Monads in Ruby Part 1: Identity, Monads In Ruby Part 1.5: Identity, Monads in Ruby Part 2: Maybe (then again Maybe not)
• Monads in Ruby
• Monads on the Cheap I: The Maybe Monad in JavaScript, More Monads on the Cheap: Inlined fromMaybe
• Monads in Ruby (with nice syntax!), List Monad in Ruby and Python
• Haskell-style monad do-notation for Ruby

In general, the Church-Turing-Thesis tells us that everything that can be done in one language can also be done in every other language.

As you can probably tell from the selection of examples above, I am (mostly) a Ruby programmer. So, just as a joke, I took one of the examples above and re-implemented it in a language that I know absolutely nothing about, that is usually thought of as a not very powerful language, and that seems to be the only programming language on the planet for which I was not able to find a Monad tutorial. May I present to you … the Identity Monad in PHP:

<?php
class Identity {
  protected $val;
  public function __construct($val) { $this->val = $val; }
  public static function m_return($a) { return new Identity($a); }
  public static function m_bind($id_a, $f) { return $f($id_a->val); }
}

var_dump(Identity::m_bind(
  Identity::m_return(1), function ($x) {
    return Identity::m_return($x+1);
  }
));
?>

No static types, no generics, no closures necessary.

Now, if you actually want to statically check monads, then you need a static type system. But that is more or less a tautology: if you want to statically check types, you need a static type checker. Duh.

With regards to your question:

In my understanding, the language implementing monad should be type-checked statically. Otherwise, type errors cannot be found during compilation and "Complexity" is not controlled. Is my understanding correct?

You are right, but this has nothing to do with monads. This is just about static type checking in general, and applies equally well to arrays, lists or even plain boring integers.

There is also a red herring here: if you look for example at monad implementations in C#, Java or C, they are much longer and much more complex than, say, the PHP example above. In particular, there's tons of types everywhere, so it certainly looks impressive. But the ugly truth is: C#'s, Java's and C's type systems aren't actually powerful enough to express the type of Monad. In particular, Monad is a rank-2 polymorphic type, but C# and Java only support rank-1 polymorphism (they call it "generics", but it's the same thing) and C doesn't support even that.

So, monads are in fact not statically type-checked in C#, Java and C. (That's for example the reason why the LINQ monad comprehensions are defined as a pattern and not as a type: because you simply cannot express the type in C#.) All the static type system does, is make the implementation much more complex, without actually helping. It requires a much more sophisticated type system such as Haskell's, to get actual type-safety for monads.

Note: what I wrote above only applies to the generic monad type itself, as @Porges points out. You can certainly express the type of any specific monad, like List or Maybe, but you cannot express the type of Monad itself. And this means that you cannot type-check the fact that "List IS-A Monad", and you cannot type-check generic operations that work on all instances of Monad.

(Note that checking that Monad also obeys the monad laws in addition to conforming to the monad type is probably too much even for Haskell's type system. You'd probably need dependent types and maybe even a full-blown automatic theorem prover for that.)