Hello!
I am trying to implement denotational semantics for a language with structs/records by embedding structs as heterogeneous vectors in Coq. However I get stuck b/c I end of having to partially apply the denote function in its recursive definition:
Require Coq.Vectors.Vector.
Module Vec := Coq.Vectors.Vector.
Import Vec.VectorNotations.
From Equations Require Import Equations.
Module VecEq.
Derive Signature NoConfusion NoConfusionHom for Vec.t.
End VecEq.
(** Heterogeneous vector library. *)
Module HetVec.
Section Hetero.
Polymorphic Universe a b.
Polymorphic Context {A : Type@{a}}.
Polymorphic Variable B : A -> Type@{b}.
Polymorphic Inductive t : forall {n : nat}, Vec.t A n -> Type@{b} :=
| nil : t []%vector
| cons {n : nat} {a : A} {v : Vec.t A n} :
B a -> t v -> t (a :: v)%vector.
Polymorphic Derive Signature NoConfusion NoConfusionHom for t.
End Hetero.
Arguments nil {A}%type_scope {B}%type_scope.
Arguments cons {A}%type_scope {B}%type_scope {n}%nat_scope {a} {v}.
Module HetVecNotations.
Declare Scope het_vec_scope.
Delimit Scope het_vec_scope with het_vec.
Notation "[ ]" := nil (format "[ ]") : het_vec_scope.
Notation "h :: t" := (cons h t) (at level 60, right associativity)
: het_vec_scope.
Notation "[ x ]" := (x :: [])%het_vec : het_vec_scope.
Notation "[ x ; y ; .. ; z ]"
:= (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : het_vec_scope.
End HetVecNotations.
Section Hetero.
Import HetVecNotations.
Local Open Scope het_vec_scope.
Polymorphic Universe a b.
Polymorphic Context {A : Type@{a}}.
Polymorphic Variable B : A -> Type@{b}.
Polymorphic Equations hd :
forall {n : nat} {a : A} {v : Vec.t A n},
t B (a :: v)%vector -> B a :=
hd (b :: _) := b.
Polymorphic Equations tl :
forall {n : nat} {a : A} {v : Vec.t A n},
t B (a :: v)%vector -> t B v :=
tl (_ :: r) := r.
Polymorphic Equations append :
forall {m n : nat} {v1 : Vec.t A m} {v2 : Vec.t A n},
t B v1 -> t B v2 -> t B (v1 ++ v2)%vector := {
append [] hv := hv;
append (b :: r) hv := b :: append r hv }.
Polymorphic Equations nth :
forall {n : nat} (fn : Fin.t n) {v : Vec.t A n},
t B v -> B (Vec.nth v fn) := {
nth Fin.F1 (b :: _) := b;
nth (Fin.FS fn) (_ :: r) := nth fn r }.
Section Inject.
Variable (f : forall a : A, B a).
Polymorphic Equations inject :
forall (l : list A), t B (Vec.of_list l) := {
inject []%list => [];
inject (a :: r)%list => f a :: inject r
}.
End Inject.
Section Map.
Polymorphic Universe c.
Polymorphic Context
{C : A -> Type@{c}}.
Polymorphic Variable f : forall {a : A}, B a -> C a.
Polymorphic Equations map
: forall {n : nat} {v : Vec.t A n}, t B v -> t C v := {
map [ ] := [ ];
map (b :: r) := f b :: map r }.
End Map.
End Hetero.
Module NotationsFun.
Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : het_vec_scope.
Infix "++" := append : het_vec_scope.
End NotationsFun.
End HetVec.
(** Program types. *)
Inductive typ : Set :=
| Unit
| Bool
| Nat
| Arr (t1 t2 : typ)
| Struct (ts : list typ).
(** Denotation. *)
Fail Equations denote_typ : typ -> Set := {
denote_typ Unit := unit;
denote_typ Bool := bool;
denote_typ Nat := nat;
denote_typ (Arr t1 t2) := denote_typ t1 -> denote_typ t2;
denote_typ (Struct ts) := HetVec.t denote_typ (Vec.of_list ts)
}.
I get the error:
The command has indeed failed with message:
Recursive definition of denote_typ is ill-formed.
In environment
denote_typ : typ -> Set
t : typ
ts : list typ
Recursive call to denote_typ has not enough arguments.
Recursive definition is:
"fun t : typ => match t with
| Unit => unit
| Bool => bool
| Nat => nat
| Arr t1 t2 => denote_typ t1 -> denote_typ t2
| Struct ts => HetVec.t denote_typ (Vec.of_list ts)
end".
Is there a way to embed typ
structs as a heterogeneous vector? Or is there a better embedding/denotation in Coq for this?
Thanks!
You can define prodN : list Type -> Type
by structural recursion, and apply that to map denote_typ ts
: I might be mistaken but this seems structurally recursive
(with your construction you'd get an isomorphism not an equality, so vectors might be more useful in what you attempted)
You can also go through a vector instead of a list; the result is going to be propositionally equal, but maybe that helps elsewhere somehow.
Thanks! Would something like prodN loose information that the Type
s in list Type
come from denote_typ
?
I'm not sure prodN
makes a difference: if your proof is about denote_typ t
or denote_typ (Struct ts)
, there's no problem, and if it's about an arbitrary Set
you've lost the information either way: you can't test whether a Set is an HetVec.t.
(I'm also seeing that denote_typ returns a Set, but that could work out for now, since you haven't added polymorphic functions).
Last updated: May 28 2023 at 18:29 UTC