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?

Fideism

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

Kimberykimble

There's also Clojure's very nice clojure.contrib.monads library, complete with a number of great tutorials (links to some of them are included in the library's source). – Angloindian

I think the last paragraph-and-a-bit is misleading. It's the interface Monad<T> which isn't implementable in Java/C# (and tautologically therefore not type-checked!). It is, on the other hand, most certainly possible for a specific monad to be statically type-checked. – Rearmost

Answer 2

It's certainly not the case that a language implementing monads must be statically typed, as your question title asks. It may be a good idea, for the reasons you outline, but errors failing to be detected at compile time has never stopped anyone. Just look at how many people write PHP.

Centrality

I'm not sure, but any pattern in PHP is monad? – Fideism

Answer 3

You need closures for the State monad. I looked it up, PHP has closures since 5.3. So that wouldn't be a problem anymore.

Epigenous

PHP 5.3 has anonymous function which is not exactly closure. – Fideism

The full power of the closure is not really necessary; all we need to do is chain and transform functions; anonymous functions will do fine. – Dalmatian

Answer 4

No, in php it is not possible to implement monads. You need closures for that. Never the less, the concept of Maybe can be still useful, when you simulate pattern matching with classes:

abstract class Maybe {
        abstract public function isJust();
        public function isNothing(){
                return !$this->isJust();
        }
}

class Just extends Maybe {
        protected $val = null;
        public function __construct($val){
                $this->val = $val;

        }
        public function isJust(){
                return true;
        }
        public function getVal(){
                return $this->val;
        }

}
class Nothing extends Maybe {
        protected $val = null;
        public function __construct(){

        }
        public function isJust(){
                return false;
        }
}

function just(){
        print "isJust";
}
function nothing(){
        print "nothing";
}
function MaybeFunc(Maybe $arg){
        if(get_class($arg) == 'Just'){
                print "Just";
        } else {
                print "Nothing";
        }
}

MaybeFunc(new Just(5));
MaybeFunc(new Nothing());

Epigenous

I doubt that. First off, PHP does have closures. And secondly, I don't see why you would need closures to implement monads. See my answer for an implementation of the Identity Monad in PHP, which doesn't use closures. After all, PHP is Turing-complete language and everything you can do in one Turing-complete language can be done in every other Turing-complete language as well. So, if you can implement monads in Haskell, then you can do it in PHP. – Dallman