Support for dependently typed labels for variables and binders

[JasonGross]

It would be nice to support well-typed-by-construction expression types, such as nested abstract syntax where we have expr : Type -> Type, we label both variables in expr V with labels of type V and we label binders with unit, and we have abs : unit -> expr (option V) -> expr V (i.e., a new binder extends V into option V); or intrinsically typed syntax where we have a type of type codes type, and we label binders with type and we label variables in expr ctx with indices of ctx, where ctx : list type, and where abs : forall (t : type), expr (t :: ctx) -> expr ctx.

I believe (one of) the construction(s) you need for this is to generalize monoid to dependent monoid. I haven't seen this anywhere in the literature, and as far as I know, @Soares came up with it:

Require Import Coq.Unicode.Utf8.
Reserved Infix "▷" (at level 70, right associativity).
Reserved Infix "⊙" (at level 40).
Notation "( x ; y ; .. ; z )" := (existT _ .. (existT _ x y) .. z) : core_scope.
Notation Σ := sigT (only parsing).
Import EqNotations.
Record DependentMonoid (X : Type) (M : X → Type) :=
  { ext : Σ M → X
    where "x ▷ y" := (ext (x; y))
  ; I : ∀ {x : X}, unit → M x
  ; T : ∀ {x : X}, { y : M x & M (x ▷ y) } → M x
    where "y ⊙ z" := (T (y; z))
  ; I_law : ∀ {x : X}, x = (x ▷ I tt)
  ; T_law : ∀ {x : X} {y : M x} {z : M (x ▷ y)}, ((x ▷ y) ▷ z) = (x ▷ (y ⊙ z))

  ; runit : ∀ {x : X} {y : M x}         , y =    y ⊙ I tt
  ; lunit : ∀ {x : X} {y : M (x ▷ I tt)}, y = I tt ⊙ rew [M] I_law in y
  ; assoc : ∀ {x : X} {y : M x} {z : M (x ▷ y)} {w : M ((x ▷ y) ▷ z)},
      (y ⊙ (z ⊙ w)) = ((y ⊙ z) ⊙ rew [M] T_law in w)
  }.

Note that DependentMonoid X M is isomorphic to a category whose objects are X and whose morphisms from x to y are of type { m : M x | ext (x; m) = y }, where composition is given by T. Equivalently, a category with objects X and morphisms Hom x y is isomorphic to a dependent monoid with X := X and M x := { y : X & Hom x y } (ext is "target", i.e., fun v => projT1 (projT2 v), and T is composition). Said another way, a dependent monoid looks like a category where morphisms are indexed only on their source and not also on their target.

You can specialize this to a non-dependent monoid by setting X := unit.

Do you think this will allow handling nested abstract syntax and intrinsically typed syntax?

[dunnl]

Hi Jason, sorry to be slow. I've been trying to write up what I do know. I don't know how to accommodate this sort of construction but would very much like to.

Can you clarify where the dependent monoid abstraction might be used? Right now, where we use monoids, it is always a list of binder values. As you are getting at, the list of in-scope binders at a variable node does not actually constrain the possibles values for that variable. I think I understand the dependent monoid abstraction itself but I don't see where it might fit into the bigger picture, can you sketch an example?

[JasonGross]

Sorry it took me so long to get back to you. On looking at things again, I think monoids are already enough to give intrinsic typing (the DTM abstraction needs to be upgraded to allow the variable type and the expression type to be indexed over the "current monoid-element of binders in scope"; is there any reason to disallow this?). Dependent monoids would allow an extension from simply-typed lambda calculus to something like dependently-typed lambda calculus (you'd need to separate "term-level terms" and "type-level terms"), by allowing the type of "next binder" to depend on the binders already in scope.

[dunnl]

I think you are right and there is no reason not to do this. It starts to look a lot like Fiore et. al's presheaf approach, except it tracks free and bound variables separately instead of dumping them into a single context. I think term1.t, term2.t, and term3.t are all isomorphic and they gradually change from a common style to a Tealeaves-style definition. (Using non-dependent monoids for now.)

From Tealeaves Require Export
  Backends.LN.
From Coq Require Import
  Vectors.Vector.
Import Setlike.Functor.Notations. (* ∈ *)

Parameter base_typ : Type.

Inductive typ :=
| base : base_typ -> typ
| arr : typ -> typ -> typ.

Module term1.

  (* Track the variable scope in the type of terms, but track free and
     bound variables separately. *)
  Inductive t_ (Γ : list atom) (bs : nat) : Type :=
  | fvar : forall (a : atom), a ∈ Γ -> t_ Γ bs
  | bvar : Fin.t bs -> t_ Γ bs
  | lam : typ -> t_ Γ (bs + 1) -> t_ Γ bs
  | app : t_ Γ bs -> t_ Γ bs -> t_ Γ bs.

  (* Top-level terms have some free variables but we have not gone
  under any binders yet. *)
  Definition t (Γ : list atom) : Type := t_ Γ 0.

End term1.

Module term2.

  (* Track the free variable scope in the type of terms. The second
  argument is the type of bound variables, which is parameterized by
  the binding depth. *)
  Inductive t_ (Γ : list atom) (bs : nat -> Type) :=
  | fvar : forall (a : atom), a ∈ Γ -> t_ Γ bs
  | bvar : bs 0 -> t_ Γ bs
  | lam : typ -> t_ Γ (precompose (plus 1) bs) -> t_ Γ bs
  | app : t_ Γ bs -> t_ Γ bs -> t_ Γ bs.

  (* Top-level terms have some free variables and bound variables are
  the finite set with cardinality equal to the binding depth. *)
  Definition t (Γ : list atom) : Type := t_ Γ Fin.t.

End term2.

Module term3.

  (* Tealeaves style, where there is a single variable constructor and
  a single type of variables. *)
  Inductive t_ (vars : nat -> Type) :=
  | var : vars 0 -> t_ vars
  | lam : typ -> t_ (precompose (plus 1) vars) -> t_ vars
  | app : t_ vars -> t_ vars -> t_ vars.

  (* A locally nameless variable is a free variable or a de Bruijn
  index in the proper range. *)
  Inductive LN (Γ : list atom) (n : nat) : Type :=
  | fvar : forall (a : atom), a ∈ Γ -> LN Γ n
  | bvar : Fin.t n -> LN Γ n.

  Definition t (Γ : list atom) := t_ (LN Γ).

End term3.

This is for locally nameless but could be adapated for de Bruijn or even fully named.