Stream: Equations devs & users

Topic: Denotational Semantics for Structs


view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Rudy Peterson (Mar 25 2023 at 00:23):

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

view this post on Zulip 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.

view this post on Zulip 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: May 28 2023 at 18:29 UTC