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?

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`

.

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

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

(Although I guess that in the real function, you probably want to recursively call in `Abs`

and `App`

?)

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!

Julin S has marked this topic as resolved.

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