Julin Shaji (Nov 30 2022 at 04:21): 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.
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?)
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