Stream: Coq users

Topic: ✔ A PHOAS example


view this post on Zulip Julin S (Nov 30 2022 at 04:21):

I was trying to do PHOAS style of representing variable binding in Coq and got this:

Inductive type : Set :=
| Nat: type
| Arrow: type -> type -> type.

Fixpoint typeDenote (t:type): Type :=
  match t with
  | Nat => nat
  | Arrow t1 t2 => (typeDenote t1) -> (typeDenote t2)
  end.

Inductive exp (V:type->Type): type -> Type :=
| Var: forall t:type, V t -> exp V t
| App: forall t1 t2:type, exp V (Arrow t1 t2) -> exp V t1 -> exp V t2
| Abs: forall t1 t2:type, (V t1 -> exp V t2) -> exp V (Arrow t1 t2)
| Const: nat -> exp V Nat
| Plus: exp V Nat -> exp V Nat -> exp V Nat.
Arguments Var {V t}.
Arguments App {V t1 t2}.
Arguments Abs {V t1 t2}.
Arguments Const {V}.
Arguments Plus {V}.

Fixpoint expDenote {t:type} (e: exp typeDenote t)
  : typeDenote t :=
  match e in (exp _ t0)
  return (typeDenote t0)
  with
  | Var x => x
  | App f e' => (expDenote f) (expDenote e')
  | Abs f => fun e' => expDenote (f e')
  | Const n => n
  | Plus e1 e2 => (expDenote e1) + (expDenote e2)
  end.

Then we tried foldexpr function to perfom constant folding so that expressions like 5 + 2 would become just 7.

(* Attempt constant folding *)
Fixpoint foldexpr {t:type} (V:type->Type) (e:exp V t) : exp V t :=
  match e in (exp _ t0)
  return
    match t0 with
    | Nat => exp V Nat
    | Arrow a b => exp V (Arrow a b)
    end
  with
  | Const _ => e
  | Var _ => e  (* error at [e] here *)
  | Plus e1 e2 =>
      let e1' := foldexpr V e1 in
      let e2' := foldexpr V e2 in
      match e1', e2' with
      | Const x, Const y => Const (x+y)
      | _, _ => Plus e1' e2'
         (* in case if either e1 or e2 had scope for folding,
            that will be dealt with in this last branch. *)
      end
  | Abs f => e
  | App f e' => e
  end.

But it's giving error in the Var branch of foldexpr.

Error:
In environment
foldexpr : forall (t : type) (V : type -> Type),
           exp V t -> exp V t
t : type
V : type -> Type
e : exp V t
t0 : type
v : V t0
The term "e" has type "exp V t"
while it is expected to have type
 "match t0 with
  | Nat => exp V Nat
  | Arrow a b => exp V (Arrow a b)
  end".

I couldn't understand why this was showing up.

The value being matched is of type exp V t, the function's return type is also exp V t, and I'm returning e itself. But still error crept in.

Would a general match statement be of help here?

view this post on Zulip Guillaume Melquiond (Nov 30 2022 at 04:53):

As a rule of thumb, never use the expression you are matching on (i.e., e here) inside the branches of the match, especially not when you are performing a dependent match. So, instead of Var _ => e, you should have Var v => Var v, and similarly for the other branches. Moreover, I don't understand why you are using such a complicated return clause. Why not use just exp V t0? In fact, you don't even need to use it explicitly, since that is the first thing Coq will try if you just write match e with.

view this post on Zulip Meven Lennon-Bertrand (Nov 30 2022 at 10:11):

Another version using the as keyword to bind patterns, so that you do not have to explicitly name anything:

(* Attempt constant folding *)
Fixpoint foldexpr {t:type} (V:type->Type) (e:exp V t) : exp V t :=
  match e with
  | Const _ as e' | Var _ as e' | Abs _ as e' | App _ _ as e' => e'
  | Plus e1 e2 =>
      let e1' := foldexpr V e1 in
      let e2' := foldexpr V e2 in
      match e1', e2' with
      | Const x, Const y => Const (x+y)
      | _, _ => Plus e1' e2'
         (* in case if either e1 or e2 had scope for folding,
            that will be dealt with in this last branch. *)
      end
  end.

view this post on Zulip Meven Lennon-Bertrand (Nov 30 2022 at 10:15):

Or even neater:

Fixpoint foldexpr {t:type} (V:type->Type) (e:exp V t) : exp V t :=
  match e with
  | Plus e1 e2 =>
      let e1' := foldexpr V e1 in
      let e2' := foldexpr V e2 in
      match e1', e2' with
      | Const x, Const y => Const (x+y)
      | _, _ => Plus e1' e2'
         (* in case if either e1 or e2 had scope for folding,
            that will be dealt with in this last branch. *)
      end
  | _ as e' => e'
  end.

view this post on Zulip Meven Lennon-Bertrand (Nov 30 2022 at 10:15):

(Although I guess that in the real function, you probably want to recursively call in Abs and App?)

view this post on Zulip Julin S (Dec 02 2022 at 07:54):

I see that returning the value being matched itself just like that was casuing the problem. Something for me to keep in mind.
And I wasn't aware of the as e' syntax.

Thanks!

view this post on Zulip Notification Bot (Dec 02 2022 at 07:55):

Julin S has marked this topic as resolved.

view this post on Zulip Meven Lennon-Bertrand (Dec 02 2022 at 10:35):

The deeper issue is that if you are in branch, the type of the scrutinee does not change. So here in the branch for Const e still has type exp V t while the type of e' is exp V Nat, which is really what you want. And regarding the as keyword, it can be used to name any part of a branch pattern, not just the top-level one, which can prove handy at times.


Last updated: Jun 18 2024 at 08:01 UTC