Rubrication

In my last post I described how unbelievably cool modules are in Coq. Well it turns out that there is some disagreement in the community about whether one should even use them! Why? Because the type system in Coq is so powerful we hardly even need them. In fact with a bit of syntactic sugar for inductively defined types and the generation of constructors we magically get something like first class modules (first-class meaning modules that are actually values that can be passed around to functions etc...). Enter the Record. Record MonadBind : Type := { M : forall (A : Type), Type; bind : forall (A B : Type), M A -> (A -> M B) -> M B; ret : forall (A : Type), A -> M A; left_unit : forall (A B : Type) (f : A -> M B) (a : A), bind A B (ret A a) f = f a; right_unit : forall (A B : Type) (m : M A), bind A A m (ret A) = m; bind_assoc : forall (A B C : Type) (m : M A) (f : A -> M B) (g : B -> M C) (x : B), bind B C (bi...

I've been playing with the Coq proof assistant over the past few days, following closely on some frustrations that I've been having with using SML's module system and a bit of toying with type-classes in Haskell. The gist of the problem is this. Although you can define type-classes and modules such that external users of these modules/type-classes see a uniform interface, consistency is left as an exercise for the implementer. This is not really acceptable in my view. When you are writing software, often times *you* are the implementer. What you really want is for these modules not just to provide a consistent interface to outsiders, but to guarantee the correctness of the implementation! Isn't that the whole point of types? If we can't do that, why are we using types? Ok, so in Coq I *can* get the properties I've been wanting out of SML's module system. For instance take the following implementation of the Monad signature: Module Type MONAD. S...