The Coq mailing list

[Lars Rasmusson <Lars.Rasmusson AT sics.se>]

Hi,

I'm trying to implement the postfix parser in sec. 3.1 of Ralf Hinze's Functional Pearl Compile Time Parsing [1] (for Haskell) with the definitions of Monad and the Continuation Passing Style Monad given below.

To do that I need to be able to type  for instance this term. 

   (return_ tt _ leaf)

but Coq gives the error below.  Is there some way to type this program in Coq?  

(Probably I have made an error somewhere, but I'm not able to spot it.)

Thankful for any help!

/Lars

[1] http://www.cs.ox.ac.uk/people/ralf.hinze/publications/Quote.pdf

(**********************************************************************)

Class Monad (m: Type -> Type): Type :=

  {

    return_ {A}:     A -> m A;

    bind    {A B}:   m A -> (A -> m B) -> m B;

    right_unit {A}:  forall (a: m A), bind a return_ = a;

    left_unit  {A}:  forall (a: A) B (f: A -> m B),

                       bind (return_ a) f = f a;

    associativity {A B C}:

                     forall a (f: A -> m B) (g: B -> m C),

                       bind a (fun x => bind (f x) g) = bind (bind a f) g

}.

Notation "a >>= f" := (bind a f) (at level 50, left associativity).

Definition lift {m} {M:Monad m} {A B: Type} (f: A->B) (a: A): m B :=

  return_ (f a).

Definition CPS (S:Type) := forall A, (S->A) -> A.

Instance CPSMonad : Monad CPS  :=

  {|

    return_ S s A f := f s ;

    bind    A B m k C c := m _ (fun a => k a _ c)

  |}.

auto. auto. auto. Defined.

(**********************************************************************)

Inductive Tree := Leaf | Fork (_ _:Tree).

Definition leaf_ ST (st:ST) := (st, Leaf).

Definition leaf {ST:Type}   := lift (leaf_ ST).

Definition

(* this works *)

Check (return_ tt) >>= leaf.

(* this doesn't work *)

Check return_ tt _ leaf.

(*

Toplevel input, characters 19-23:

Error:

The term "leaf" has type "unit -> CPS (unit * Tree)"

while it is expected to have type "unit -> ?T"

(unable to find a well-typed instantiation for "?T": cannot ensure that

"Type@{max(Top.27, Top.29+1)}" is a subtype of "Type@{Top.29}").

 *)

(* More like in the paper, just for fun 

Module example.

  Definition quote := return_ tt.

  Definition leaf_ ST (st:ST) := (st, Leaf).

  Definition leaf {ST:Type}   := lift (leaf_ ST).

  Definition fork_ ST (st:(ST * Tree) * Tree) :=

    match st with ((st',l),r) => (st', Fork l r) end.

  Definition fork {ST}               := lift (fork_ ST).

  Definition endquote (st:unit*Tree) := match st with (_,t) => t end.

  (* this constructs the Tree (Fork Leaf Leaf) *)

  Compute (quote >>= leaf >>= leaf >>= fork >>= (lift endquote)) _ (fun x=>x).

  Arguments quote {_} _.

  (* this should do the same but fails with the same error as above*)

  Check quote leaf leaf fork endquote.

End example.

*)