Erasing that distinction enables some goodies such as first-class type constructors, which makes it possible to manipulate types of higher kind. This in turn, presumably enables things like Generalized Algebraic Data Types.
type MONAD (m : type ⇒ type) =
{
return a : a → m a;
bind a b : m a → (a → m b) → m b
};
map a b (m : type ⇒ type) (M : MONAD m) (f : a → b) (mx : m a) =
M.bind a b mx (fun (x : a) ⇒ M.return b (f x)) (* : m b *)
not too bad.. though I wonder if things are defined structurally instead of nominally, which monad instance are you going to get for a given expression. Haskell's "one instance per class" rule means the compiler figure out which monad instance to apply.
This looks more flexible, but also looks like it will require more annotations and explicit parameters.
If you combine this with [modular implicits](http://www.meetup.com/NYC-OCaml/events/222026251/), which are hopefully going to be added to OCaml soon, then you'll get something which is nearly as syntactically neat as type classes but more powerful.
The proposed OCaml implementation of modular implicits[1] considers ambiguity a compile-time error, so in that case you'd have to manually indicate which module you're passing in. (This is in contrast to Scala, in which there's an elaborate mechanism for resolving ambiguity in implicits which makes it hard to know which is being selected.)
So the OCaml implementation shouldn't make it any more difficult to discover which implicit is in use in a given context, because if an implicit is used, then it must necessarily be unique and there will be no ambiguity.
You have to explicitly pass the monad "vtable". If 1ML also grabs up modular implicits then you'll have a sensible way of passing implicit arguments not exactly unlike that of Haskell, but modularity and global canonicity are at odds so you have a more complex reasoning task.
