The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Mon, Oct 6, 2014 at 1:20 PM, John Wiegley 
<johnw AT newartisans.com>
 wrote:
> Hello,
>
> I'm working on formalizing the contents of "Kleisli arrows of outrageous
> fortune" (https://github.com/jwiegley/coq-haskell/blob/master/Conor.v), and
> while I'm most of the way through, I'm having difficulty attempting to 
> encode
> the free monad using a modified W-type.  Following an example of something
> Conor posted in Coq-club long ago, I've tried this:
>
>     Inductive Kleene {I} (F : (I → Type) → I → Type) (p : I → Type) (i : I) 
> :=
>       | Ret : p i → Kleene F p i
>       | Do  : (forall q, F q i) → Kleene F p i.
>
> This is around line 970.
>
> However, I have a strong suspicion this can't be right.  Can anyone help me 
> to
> find a better direction?

Hmm, I don't really know the terminology "free monad", but my first
guess would have been something like this (for normal Types):

Inductive free_monad : Type -> Type :=
| free_return : forall {A:Type}, A -> free_monad A
| free_bind : forall {A B:Type}, free_monad A -> (A -> free_monad B) ->
                free_monad B.

Require Import Morphisms.

Inductive free_monad_eqv :
  forall {A:Type}, free_monad A -> free_monad A -> Prop :=
| free_monad_eqv_refl : forall {A}, Reflexive (@free_monad_eqv A)
| free_monad_eqv_sym : forall {A}, Symmetric (@free_monad_eqv A)
| free_monad_eqv_trans : forall {A}, Transitive (@free_monad_eqv A)
(*
| free_return_wd : forall {A}, Proper (eq ==> free_monad_eqv) (@free_return A)
*)
| free_bind_wd : forall {A B}, Proper
  (free_monad_eqv ==>
   (eq ==> free_monad_eqv) ==>
   free_monad_eqv)
  (@free_bind A B)
| free_monad_left_id : forall {A B:Type} (x:A) (f:A->free_monad B),
  free_monad_eqv (free_bind (free_return x) f) (f x)
| free_monad_right_id : forall {A B:Type} (x:free_monad A),
  free_monad_eqv (free_bind x free_return) x
| free_monad_assoc : forall {A B C:Type} (f:A->free_monad B)
  (g:B->free_monad C) (x:free_monad A),
  free_monad_eqv
  (free_bind (free_bind x f) g)
  (free_bind x (fun x0 => free_bind (f x0) g)).

Existing Instance free_monad_eqv_refl.
Existing Instance free_monad_eqv_sym.
Existing Instance free_monad_eqv_trans.
Existing Instance free_bind_wd.

Lemma free_return_wd : forall {A},
  Proper (eq ==> free_monad_eqv) (@free_return A).
Proof.
do 2 red; intros. rewrite H. reflexivity.
Qed.

Of course, this isn't all that interesting, as free_monad A reduces to
A modulo equivalence:

Require Import Program.
Program Fixpoint free_monad_inv {A:Type} (x : free_monad A) :
  { x0:A | free_monad_eqv x (free_return x0) } :=
match x with
| free_return A x0 => x0
| free_bind A B x f => free_monad_inv (f (free_monad_inv x))
end.
Next Obligation.
reflexivity.
Qed.
Next Obligation.
rewrite f0.
rewrite free_monad_left_id.
assumption.
Defined.

But if you added extra generators in free_monad, e.g. adding an
abstract element of free_monad bool, then things would presumably
become more interesting.
-- 
Daniel Schepler