## Stream: Equations devs & users

### Topic: Denotational Semantics for Structs

#### Rudy Peterson (Mar 24 2023 at 21:16):

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!

#### Paolo Giarrusso (Mar 24 2023 at 22:43):

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

#### Paolo Giarrusso (Mar 24 2023 at 22:46):

(with your construction you'd get an isomorphism not an equality, so vectors might be more useful in what you attempted)

#### Paolo Giarrusso (Mar 24 2023 at 22:46):

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.

#### Rudy Peterson (Mar 25 2023 at 00:23):

Thanks! Would something like prodN loose information that the `Type`s in `list Type` come from `denote_typ`?

#### Paolo Giarrusso (Mar 25 2023 at 02:59):

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.

#### Paolo Giarrusso (Mar 25 2023 at 03:01):

(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: Sep 28 2023 at 10:01 UTC