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 (bind…

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 (bind…