The Coq mailing list

[Pierre-Evariste Dagand <pierre-evariste.dagand AT ens-cachan.org>]

[Resending from the right address. Apologies to the Coq-club 
moderator/bouncer.]

> Where I am having difficulties now is figuring out how to use signatures.  
> For
> example:
>
>     Definition FH' : (State → Type) → State → Type :=
>           ((FilePath ::= Closed) :>>: (fun _ => State))  (* fOpen *)
>       :+: ((unit ::= Open) :>>: (option nat ::= Open))   (* fGetC *)
>       :+: ((unit ::= Open) :>>: (unit ::= Closed)).      (* fClose *)
>
> [...]
> Is the Signature over State, or would it be over HF' in this example?  Or is
> it something else altogether?

Third option :-)

As I said, everywhere you've been manipulating endofunctors on State
-> Type, you need to define the equivalent operators over signatures.
This includes ":>>:" and ":+:":
 1) given a pre-condition P : State -> type and a post-condition Q :
State -> Type, you need to define a signature that will *interpret* to
something (extensionally) equal to your operator ":>>:". That's how
you are going to define operations individually.
 2) given two signatures S and S', you need to define a signature that
combines them, ie. that *interprets* to something (extensionally)
equal to your operator ":+:". That's how you are going to aggregate
operations together.

Having defined these combinators, you'll be able to write the same
definition for FH' but, this time, it will build a signature of State.
You can then use that signature to construct the free monad.

Concerning your definition:

>     Definition FH : Signature State :=
>       {| Operations := fun st : State => State -> Type     (* WRONG *)
>        ; Arities    := fun (st : State) ops => FH' ops st  (* WRONG? *)
>        ; Sorts      := fun (st : State) ops ars => st |}.  (* WRONG *)

that's absolutely wrong. You'll realize why after defining the
signature of ":>>:".

--
Pierre-Evariste