## Stream: Coq users

### Topic: ✔ A PHOAS example

#### Julin Shaji (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?

#### 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`.

#### 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.
``````

#### 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.
``````

#### 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`?)

#### Julin Shaji (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!

#### Notification Bot (Dec 02 2022 at 07:55):

Julin S has marked this topic as resolved.

#### 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: Oct 03 2023 at 02:34 UTC