The Coq mailing list

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

*postfix* parsing, that is...

On Tue, Mar 15, 2016 at 8:48 AM, Lars Rasmusson <Lars.Rasmusson AT sics.se> wrote:

Thanks a lot for your explanation. I have to think some more about this, but it seems reasonable that one could create infinite loops with continuation passing, so it is difficult to type...

Fortunately, for the "compile time parsing", the full power of the CPS monad is not required, at least not for post-fix parsing.  I was able to define prefix parsing like this:

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

  (* make "constructor functions" that require a stack of previously constructed values *)

  (* a leaf can take any stack, a fork needs a stack with at least two trees on top of it *)

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

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

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

  (* wrap the functions as described in the functional pearl *)

  Definition quote {A } (f:unit->A) := f tt.

  Definition lift {A B} C (f:A->B) (st:A) (cont:B->C) := cont (f st).

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

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

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

  Notation "<|" := quote. Notation "|>" := endquote.

  (* this is how to create abstract terms of type Tree using the concrete syntax with leaf and fork *) 

  Definition t := <| leaf leaf leaf fork leaf fork leaf fork leaf leaf fork fork fork |>.

  (* It works!*)

  Check eq_refl : <| leaf leaf fork leaf fork |> = Fork (Fork Leaf Leaf) Leaf.

  (* This is not allowed *)

  Check <| leaf fork |>.

On Sun, Mar 13, 2016 at 8:20 PM, Roger Witte <rogerwite AT yahoo.co.uk> wrote:

The error message is indicating s universe inconsistency.  i have encountered this error when a declaration that should be monographic is declared polymorphic.  Unfortunately the declaration concerned is not the one in which the error occurs.

If possible, just make your project Universe Monographic.  If you still get universe inconsistency, you may need to check that you really haven't hit a paradox.

If you are sure that you are not trying to put a proper class inside a set, then you need to ensure that you fon't do so accidently.

There ate two approaches:

Explicit declaration and specification of universes or explicit declaration of monomorphic and polymorphic.  These are not mutually exclusive.

Personally I find this difficult and end up doing s fair amount of trial and error.  I find that polymorphic things often default to being in too large a universe but that monomorphic things or things with explicitly declared universes end up in too small a universe.

i know Regis list contains experts who will offer you more precise and helpful advice, but I am hoping that by highlighting precisely what I have and have not been able to learn from the reference manual, I can help them to improve the documentation.

Sent from Yahoo Mail on Android

On Sun, 13 Mar, 2016 at 18:56, Lars Rasmusson

<Lars.Rasmusson AT sics.se> wrote:

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.

*)