The Coq mailing list

[John Wiegley <johnw AT newartisans.com>]

>>>>> Pierre-Evariste Dagand 
>>>>> <pierre-evariste.dagand AT ens-cachan.org>
>>>>>  writes:

> Now, to translate that paper, everywhere Conor is manipulating functors, you
> should work on 'Signatures'. Implementing such system in type theory is a
> Scottish cottage industry: you should many implementations north of the
> Border (perhaps starting with Brady's "Programming and Reasoning with
> Algebraic Effects and Dependent Types" and then harassing Stevan Andjelkovic
> -- Conor's student -- to first write and then publish his PhD thesis
> online).

Hi Pierre,

Thanks to your wonderful advice, I was able to implement the Kleene monad in
Coq and prove all the various laws regarding it.

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 *)
    
    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 *)

    Definition fOpen (p : FilePath) : (FH :* (const State)) Closed.
    Proof.
      apply Do.
      apply {| op := ?
             ; ar := ?
             ; xx := @Ret _ _ _  (* ? *)
             |}.
    Abort.

Is the Signature over State, or would it be over HF' in this example?  Or is
it something else altogether?

The current version of the code remains here:

    https://github.com/jwiegley/coq-haskell/blob/master/Conor.v#L1113

Many thanks!
  John