Introduction

The puzzle we explore in this post is that of writing a deep embedding of ADT declarations as well as exploring what the type of values of such a declaration should be. Let's settle on some minimal schema as an example, while keeping in mind our approach should be general.

Parameter primitive : Type.

Inductive type :=
| Prim : type
| Prod : type -> type -> type
| Sum  : type -> type -> type
| Box  : type -> type
| Var  : type
| Fix  : type -> type
.

Here, we have a variety of constructions one may want in their language. Note that we do not include functions because we restrict our study to strictly positive (or covariant) recursive positions. The Box constructor represents some sort of pointer or indirection. The Fix and Var constructors represent a fixpoint mechanism. When writing semantics for this type, we will want Fix (A x) to be equivalent in some sense to A (Fix (A x)).

To make this intent clearer, let us define what we mean by this, by implementing substitution of the variable.

(* subs t u := u[t/Var] *)
Fixpoint subs (t : type) (u : type) :=
match u with
| Prim     => Prim
| Prod x y => Prod (subs t x) (subs t y)
| Sum  x y => Sum (subs t x) (subs t y)
| Box  x   => Box (subs t x)
| Var      => t
| Fix  x   => Fix x (* Var is bound again here, do not substitute *)
end.

What we want now is value (Fix t) ≡ value (subs (Fix t) t). In the next sections, we explore different implementations of this pattern. Notably, we will start with a typical isorecursive (that is, ≡ is equivalence modulo explicit unfolding steps) that might be well-suited to most codebases, then address a novel equirecursive approach (that is, ≡ will be equality) and address the tradeoffs.

Explicit Substitution

Here the idea is to define a value type directly with type as an index. This approach will require some constructors to have Mu t as an index, which corresponds to a logical unfolding step rather than a logical value.

Inductive value : type -> Type :=
| VPrim (p : primitive) : value Prim
| VProd {t u} : value t -> value u -> value (Prod t u)
| VSumL {t u} : value t -> value (Sum t u)
| VSumR {t u} : value u -> value (Sum t u)
| VNull {t}   : value (Box t)
| VBox  {t}   : value t -> value (Box t)
(* No VVar! *)
| VFix  {t}   : value (subs (Fix t) t) -> value (Fix t)
.

The recursion mechanism is explicit: we do not need VVar because it is systematically substituted when reaching the Fix constructor.

Let's see with an example: the humble binary tree.

Definition bt :=
  Fix (Box (Prod Prim
                (Prod Var Var))).

Parameters p1 : primitive.
Example bt_value1 : value bt.
value bt
Proof.
value bt
  (* Opening proof mode to see what VFix does *)
  apply VFix.
value
  (subs (Fix (Box (Prod Prim (Prod Var Var))))
     (Box (Prod Prim (Prod Var Var))))
  cbn. (* run subs for clarity *)
value
  (Box
     (Prod Prim
        (Prod (Fix (Box (Prod Prim (Prod Var Var))))
           (Fix (Box (Prod Prim (Prod Var Var)))))))
  apply VBox, VProd.
value Prim
value
  (Prod (Fix (Box (Prod Prim (Prod Var Var))))
     (Fix (Box (Prod Prim (Prod Var Var)))))
  -
value Prim exact (VPrim p1).
  -
value
  (Prod (Fix (Box (Prod Prim (Prod Var Var))))
     (Fix (Box (Prod Prim (Prod Var Var))))) apply VProd.
value (Fix (Box (Prod Prim (Prod Var Var))))
value (Fix (Box (Prod Prim (Prod Var Var))))
    +
value (Fix (Box (Prod Prim (Prod Var Var)))) apply VFix.
value
  (subs (Fix (Box (Prod Prim (Prod Var Var))))
     (Box (Prod Prim (Prod Var Var)))) cbn.
value
  (Box
     (Prod Prim
        (Prod (Fix (Box (Prod Prim (Prod Var Var))))
           (Fix (Box (Prod Prim (Prod Var Var))))))) apply VNull.
    +
value (Fix (Box (Prod Prim (Prod Var Var)))) apply VFix.
value
  (subs (Fix (Box (Prod Prim (Prod Var Var))))
     (Box (Prod Prim (Prod Var Var)))) cbn.
value
  (Box
     (Prod Prim
        (Prod (Fix (Box (Prod Prim (Prod Var Var))))
           (Fix (Box (Prod Prim (Prod Var Var))))))) apply VNull.
Defined.

Now that we know how to create a value, we can show that a recursive type and its unfolding has isomorphic interpretions. More precisely, below we show that value (Fix t) is isomorphic to value (subs (Fix t) t), as the value folding and unfolding functions are mutual inverses.

Goal exists (g : forall {t},
              value (subs (Fix t) t) -> value (Fix t))
            (f : forall {t},
              value (Fix t) -> value (subs (Fix t) t)),
                 forall t,
                 forall v : value (subs (Fix t) t),
                 forall w : value (Fix t),
                 f (g v) = v
              /\ g (f w) = w.
exists
  (g : forall t : type,
       value (subs (Fix t) t) -> value (Fix t)) 
(f : forall t : type,
     value (Fix t) -> value (subs (Fix t) t)),
  forall (t : type) (v : value (subs (Fix t) t))
    (w : value (Fix t)),
  f t (g t v) = v /\ g t (f t w) = w
Proof.
exists
  (g : forall t : type,
       value (subs (Fix t) t) -> value (Fix t)) 
(f : forall t : type,
     value (Fix t) -> value (subs (Fix t) t)),
  forall (t : type) (v : value (subs (Fix t) t))
    (w : value (Fix t)),
  f t (g t v) = v /\ g t (f t w) = w
  exists @VFix.
exists
  f : forall t : type,
      value (Fix t) -> value (subs (Fix t) t),
  forall (t : type) (v : value (subs (Fix t) t))
    (w : value (Fix t)),
  f t (VFix v) = v /\ VFix (f t w) = w

Now let's define the inverse to VFix by getting its argument.

Definition refold {t} (v : value (Fix t)) : value (subs (Fix t) t).
t: type
v: value (Fix t)
value (subs (Fix t) t)
Proof.
t: type
v: value (Fix t)
value (subs (Fix t) t)
  now inversion_clear v.
Defined.
exists
  f : forall t : type,
      value (Fix t) -> value (subs (Fix t) t),
  forall (t : type) (v : value (subs (Fix t) t))
    (w : value (Fix t)),
  f t (VFix v) = v /\ VFix (f t w) = w

It is easy to show that refold is indeed the inverse of VFix.

  exists @refold.
forall (t : type) (v : value (subs (Fix t) t))
  (w : value (Fix t)),
refold (VFix v) = v /\ VFix (refold w) = w

  split.
t: type
v: value (subs (Fix t) t)
w: value (Fix t)
refold (VFix v) = v
t: type
v: value (subs (Fix t) t)
w: value (Fix t)
VFix (refold w) = w
  -
t: type
v: value (subs (Fix t) t)
w: value (Fix t)
refold (VFix v) = v reflexivity.
  -
t: type
v: value (subs (Fix t) t)
w: value (Fix t)
VFix (refold w) = w now refine (match w with VFix u => _ | _ => _ end).
Qed.

This approach is probably the simplest!

In the next section, we discuss how to ensure that all types that can be defined can be instantiated without self-reference.

Notation "'μ' X , A" := (Fix ((fun X => A) Var))
                        (X binder, at level 10).

Guards to the Rescue

Recall our goal was in part correctness by construction. While we have that for terms, our types have no guarantee of being well-formed with respect to some requirements. In this section, we use inhabitedness as an example requirement. Unfortunately, at this time, we allow some nonsensical types such as μ X, X. We could implement a predicate valid_type : type -> Prop but for the sake of preparing the future section, let's discuss how to make a guard checker inside of our type.

There are many different kinds of degenerate types. First of all, we want to avoid types where Var is free.

Goal value Var -> False.
value Var -> False
Proof.
value Var -> False intro v; inversion v. Qed.

Indeed, this type is not inhabited. But it is not the only case. As previously stated, μ X, X and derivatives cannot be instantiated without self-reference or infinite memory.

Goal value (μ X, X) -> False.
value (μ X, X) -> False
Proof.
value (μ X, X) -> False intro v.
v: value (μ X, X)
False
  remember (μ X, X) as ι eqn:H.
ι: type
H: ι = μ X, X
v: value ι
False
  revert H.
ι: type
v: value ι
ι = μ X, X -> False
  induction v; try discriminate.
t: type
v: value (subs (Fix t) t)
IHv: subs (Fix t) t = Fix Var -> False
Fix t = Fix Var -> False
  intro H.
t: type
v: value (subs (Fix t) t)
IHv: subs (Fix t) t = Fix Var -> False
H: Fix t = Fix Var
False
  apply IHv.
t: type
v: value (subs (Fix t) t)
IHv: subs (Fix t) t = Fix Var -> False
H: Fix t = Fix Var
subs (Fix t) t = Fix Var
  inversion_clear H.
t: type
v: value (subs (Fix t) t)
IHv: subs (Fix t) t = Fix Var -> False
subs (Fix Var) Var = Fix Var
  now cbn.
Qed.

Ideally, we would like to be able to prove forall t, value t. So when should a type be considered well-formed? It seems clear that a non-recursive type is trustworthy, as long as it does not contain Var. Let's call this condition closedness. The only remaining case is Fix t. Of course, t need not be closed here. Rather, we want to ensure the type is inhabited. Let's call this condition guardedness.

Notice that if a type is closed then it is guarded, hence we only need three different categories: closed and guarded (Closed), open and guarded (Guarded), and open and unguarded (Open). For instance, a product type is guarded if and only if both factors are guarded. On the other hand, a sum type is guarded if and only if at least one factor is guarded. We can define a three-element structure that encapsulates these ideas.

Inductive guard := Closed | Guarded | Open.

Notation "x ⊔ y" := (guard_join x y) (at level 70).
Notation "x ⊓ y" := (guard_meet x y) (at level 70).
Notation "□ x"  := (x ⊔ Closed) (at level 60).

The law definitions are a bit convoluted, but they do correspond to the intuitive description above. Here are the operation tables:

Note that it is not a lattice: openness is contagious. These two operations offer the building blocks for the behaviours we would want. Meet offers the expected conjunction of guardedness, join keeps the best guardedness but worse openness. Another construction is □ g. It is always guarded but it is only closed when g is.

Now we can index our type by its guardedness.

Inductive type_ : guard -> Type :=
| Prim_ : type_ Closed
| Prod_ {g1 g2} : type_ g1 -> type_ g2 -> type_ (g1 ⊓ g2)
| Sum_  {g1 g2} : type_ g1 -> type_ g2 -> type_ (g1 ⊔ g2)
| Box_  {g} : type_ g -> type_ (□ g)
| Var_  : type_ Open
| Fix_  : type_ Guarded -> type_ Closed
.

Definition type_g := type_ Closed.

Now we can ensure the substitution returns a closed type.

Fixpoint subs_g {g} (t : type_g) (u : type_ g) : type_g :=
match u with
| Prim_     => Prim_
| Prod_ x y => Prod_ (subs_g t x) (subs_g t y)
| Sum_  x y => Sum_ (subs_g t x) (subs_g t y)
| Box_  x   => Box_ (subs_g t x)
| Var_      => t
| Fix_  x   => Fix_ x
end.

The rest is completely similar, but now we only have to define value for closed types!

Inductive value_g : type_g -> Type :=
| VgPrim (p : primitive) : value_g Prim_
| VgProd {t u} : value_g t -> value_g u -> value_g (Prod_ t u)
| VgSumL {t u : type_g} : value_g t -> value_g (Sum_ t u)
| VgSumR {t u : type_g} : value_g u -> value_g (Sum_ t u)
| VgNull {t : type_g}   : value_g (Box_ t)
| VgBox  {t}   : value_g t -> value_g (Box_ t)
(* No VgVar! *)
| VgFix  {t}   : value_g (subs_g (Fix_ t) t) -> value_g (Fix_ t)
.

Since subs_g only produces closed types, we never have to talk about the open body of Fix_ in the type of values. Hopefully now we can show all such types are well-formed (our criterion was inhabitedness).

Example inhabited : primitive -> forall t, value_g t.
primitive -> forall t : type_g, value_g t

The proof is mainly contained in the following lemma, which simply checks that our guardedness condition does what we wish. That is, any guarded type, even if open (expressed using □ g), is inhabited.

Lemma guarded_inhabited : primitive ->
  forall g (t : type_ (□ g)) (r : type_g),
  value_g (subs_g r t).
primitive ->
forall (g : guard) (t : type_ (□ g)) (r : type_g),
value_g (subs_g r t)

The proof amounts to an induction that eliminates all irrelevant cases by using the laws defined for guard.

To a human reader, I would argue that a closed type t is equal to subs Prim_ t. By the lemma, we have the expected result. To Rocq, an induction that uses the lemma for the Fix_ case is easier to write.

Example btg :=
  Fix_ (Box_ (Prod_ Prim_
                   (Prod_ Var_ Var_))).
Eval compute in (inhabited p1 btg).
= VgFix VgNull
: value_g btg

Note that guardedness can be used to mean something other than inhabitedness. For instance, even without the VNull, we would reasonably claim that a pointer is guarded because a single block takes finite memory to represent. The reader is free to adapt their definition to obtain their chosen guardedness property.

Coinductives à la carte

Data types à la carte [Swierstra2008] proposes an approach to write composable type components. Here we adopt a similar methodology to create a variant of our types that is equirecursive. The result will hence not require explicit unfolding steps in the value.

Let's recall the basic method used to turn a type into a component. It is as simple as replacing every recursive occurrence by a brand new argument.

Inductive typeF {β} :=
| PrimF : typeF
| ProdF : β -> β -> typeF
| BoxF  : β -> typeF
(* and so on... *)
.

And then we can write type as the least fixpoint of typeF.

Inductive typeFix :=
  rollFix : @typeF typeFix -> typeFix.

Example basicFix := rollFix (ProdF (rollFix (BoxF (rollFix PrimF)))
                                   (rollFix PrimF)).

So why not declare the whole type that way? Let's use one more trick to incorporate a guard checker. We will add a second argument α to the inductive that will represent what the Fix constructor is allowed to use. That way, we can get rid of Var and also specify what it means to be guarded. However we will not ensure inhabitedness, for the sake of simplicity.

Inductive type𝕗 {α β} :=
| Prim𝕗 : type𝕗
| Prod𝕗 : β -> β -> type𝕗
| Sum𝕗  : β -> β -> type𝕗
| Fix𝕗  : α -> type𝕗
.
Arguments type𝕗 α β : clear implicits.

So what should α be? The desired usecase would be something like Fix𝕗 (Guarded Expr where α := True). Indeed, when α is True, Fix𝕗 can be used much like Var before. Then how can we guard an expression? By setting α to False! That way, the Fix constructor may never be called. We see α has many hats. In order to implement this, we need an idea of what we meant by Expr. An expression should be able to embed another type and to unroll type𝕗 as many times as needed.

This construction is called the free monad on type𝕗.

Inductive expr𝕗 {α β} :=
| Ret : β -> expr𝕗
| Do  : type𝕗 α expr𝕗 -> expr𝕗
.
Arguments expr𝕗 α β : clear implicits.

Definition guarded_expr𝕗 β := type𝕗 False (expr𝕗 True β).

We can finally tie the knot and define the fixpoint we are interested in:

Inductive Ftype :=
 roll : type𝕗 (guarded_expr𝕗 Ftype) Ftype -> Ftype.

Here is a summary of the type we constructed:

Given how many different contexts there are in this hierarchy, it is suitable to implement smart constructors. Indeed, we want to be able to use prod regardless of whether we are building an expr𝕗 or a guarded_expr𝕗.

Section smart_constructors.
   Definition expr := expr𝕗 True Ftype.
   Definition guarded_expr := guarded_expr𝕗 Ftype.
   Class MkPrim (R : Type) := prim : R.
   Class MkProd (U : Type) (R : Type) := prod : U -> U -> R.
   Class MkSum  (U : Type) (R : Type) := sum  : U -> U -> R.
   Class MkFix  (R : Type) := ffix : guarded_expr𝕗 Ftype -> R.
   (* instances... *)
End smart_constructors.

Notation "L ⨂ L'" := (prod L L')
                      (at level 40, left associativity).
Notation "L ⨁ L'" := (sum L L')
                      (at level 50, left associativity).
Notation "'μ:' X , A" := (ffix ((fun X => A) (Do (Fix𝕗 I))))
                         (X binder, at level 180).

Example bintree : Ftype := μ: T, prim ⨁ (T ⨂ T).

We still want to define value as an inductive that has our type as an index. However, the current type is very complicated. Instead, we would like to have access to the regular tree of our type. The regular tree of a recursive type is the tree obtained by infinitely unfolding the Fix constructions.

To define the type of a regular tree, we can reuse type𝕗. The idea is to simply reuse the guard trick at every level, having α := False.

CoInductive FType :=
  Roll : type𝕗 False FType -> FType.

The unfolding function is a bit tedious to write, but it always has the same layered structure.

CoFixpoint regular_tree (t : Ftype) : FType := (* ... *)

(* Here I wish I could make it be hidden by default
   but unfoldable... *)

And now that we have our nicely unfolded type, we can freely define the type of values without any fuss.

 Inductive Fvalue : FType -> Type :=
 | FVPrim (p : primitive) : Fvalue prim
 | FVProd {t u} : Fvalue t -> Fvalue u -> Fvalue (prod t u)
 | FVSumL {t u} : Fvalue t -> Fvalue (sum t u)
 | FVSumR {t u} : Fvalue u -> Fvalue (sum t u)
 (* No VVar AND no VFix! *)
 .

 Definition FValue t := Fvalue (regular_tree t).

In order to actually construct values, we also need some computation lemmas to make Rocq happy. This is due to Rocq's type checking needing to terminate: it only ever computes cofixpoints if they are the scrutinee of a match expression. The unfolding step happens at the proof stage of constructing a term through applications of this lemma but it is then erased from the term, as the lemma only contains compute.

Lemma FTypeCompute t : t = match t with Roll u => Roll u end.
t: FType
t = match t with
    | Roll u => Roll u
    end
Proof.
t: FType
t = match t with
    | Roll u => Roll u
    end now destruct t. Defined.

From this, we can deduce a set of tactics (this one is very simple, and a user would likely want to implement a reification tactic from a raw value type to make constructing values outside of proof mode more convenient) to help applying this unfolding step on each constructor call.

 Ltac vcompute := match goal with
                  |- context [Fvalue ?x] => rewrite (FTypeCompute x)
                  end.
 Ltac vcons := vcompute; simpl; constructor.
 Ltac vsplitr := vcompute; simpl; apply FVSumR.
 Ltac vsplitl := vcompute; simpl; apply FVSumL.

 Example bintreeV : FValue bintree.
FValue bintree
 Proof.
FValue bintree
   unfold FValue.
Fvalue (regular_tree bintree)
   vcompute.
Fvalue
  match regular_tree bintree with
  | Roll u => Roll u
  end
   simpl.
Fvalue
  (Roll
     (Sum𝕗
        ((cofix go (u : expr) : FType :=
            match u with
            | Ret t => regular_tree t
            | Do Prim𝕗 => Roll Prim𝕗
            | Do (Prod𝕗 x y) =>
                Roll (Prod𝕗 (go x) (go y))
            | Do (Sum𝕗 x y) =>
                Roll (Sum𝕗 (go x) (go y))
            | Do (Fix𝕗 _) =>
                Roll
                  (Sum𝕗 (go prim)
                     (go (Do (Fix𝕗 I) ⨂ Do (Fix𝕗 I))))
            end)
           prim)
        ((cofix go (u : expr) : FType :=
            match u with
            | Ret t => regular_tree t
            | Do Prim𝕗 => Roll Prim𝕗
            | Do (Prod𝕗 x y) =>
                Roll (Prod𝕗 (go x) (go y))
            | Do (Sum𝕗 x y) =>
                Roll (Sum𝕗 (go x) (go y))
            | Do (Fix𝕗 _) =>
                Roll
                  (Sum𝕗 (go prim)
                     (go (Do (Fix𝕗 I) ⨂ Do (Fix𝕗 I))))
            end)
           (Do (Fix𝕗 I) ⨂ Do (Fix𝕗 I)))))
   apply FVSumR.
Fvalue
  ((cofix go (u : expr) : FType :=
      match u with
      | Ret t => regular_tree t
      | Do Prim𝕗 => Roll Prim𝕗
      | Do (Prod𝕗 x y) => Roll (Prod𝕗 (go x) (go y))
      | Do (Sum𝕗 x y) => Roll (Sum𝕗 (go x) (go y))
      | Do (Fix𝕗 _) =>
          Roll
            (Sum𝕗 (go prim)
               (go (Do (Fix𝕗 I) ⨂ Do (Fix𝕗 I))))
      end)
     (Do (Fix𝕗 I) ⨂ Do (Fix𝕗 I)))
   vcons.
Fvalue
  ((cofix go (u : expr) : FType :=
      match u with
      | Ret t => regular_tree t
      | Do Prim𝕗 => Roll Prim𝕗
      | Do (Prod𝕗 x y) => Roll (Prod𝕗 (go x) (go y))
      | Do (Sum𝕗 x y) => Roll (Sum𝕗 (go x) (go y))
      | Do (Fix𝕗 _) =>
          Roll
            (Sum𝕗 (go prim)
               (go (Do (Fix𝕗 I) ⨂ Do (Fix𝕗 I))))
      end)
     (Do (Fix𝕗 I)))
Fvalue
  ((cofix go (u : expr) : FType :=
      match u with
      | Ret t => regular_tree t
      | Do Prim𝕗 => Roll Prim𝕗
      | Do (Prod𝕗 x y) => Roll (Prod𝕗 (go x) (go y))
      | Do (Sum𝕗 x y) => Roll (Sum𝕗 (go x) (go y))
      | Do (Fix𝕗 _) =>
          Roll
            (Sum𝕗 (go prim)
               (go (Do (Fix𝕗 I) ⨂ Do (Fix𝕗 I))))
      end)
     (Do (Fix𝕗 I)))
   -
Fvalue
  ((cofix go (u : expr) : FType :=
      match u with
      | Ret t => regular_tree t
      | Do Prim𝕗 => Roll Prim𝕗
      | Do (Prod𝕗 x y) => Roll (Prod𝕗 (go x) (go y))
      | Do (Sum𝕗 x y) => Roll (Sum𝕗 (go x) (go y))
      | Do (Fix𝕗 _) =>
          Roll
            (Sum𝕗 (go prim)
               (go (Do (Fix𝕗 I) ⨂ Do (Fix𝕗 I))))
      end)
     (Do (Fix𝕗 I))) vsplitl.
Fvalue
  ((cofix go (u : expr) : FType :=
      match u with
      | Ret t => regular_tree t
      | Do Prim𝕗 => Roll Prim𝕗
      | Do (Prod𝕗 x y) => Roll (Prod𝕗 (go x) (go y))
      | Do (Sum𝕗 x y) => Roll (Sum𝕗 (go x) (go y))
      | Do (Fix𝕗 _) =>
          Roll
            (Sum𝕗 (go prim)
               (go (Do (Fix𝕗 I) ⨂ Do (Fix𝕗 I))))
      end)
     prim)
     vcons.
primitive exact p1.
   -
Fvalue
  ((cofix go (u : expr) : FType :=
      match u with
      | Ret t => regular_tree t
      | Do Prim𝕗 => Roll Prim𝕗
      | Do (Prod𝕗 x y) => Roll (Prod𝕗 (go x) (go y))
      | Do (Sum𝕗 x y) => Roll (Sum𝕗 (go x) (go y))
      | Do (Fix𝕗 _) =>
          Roll
            (Sum𝕗 (go prim)
               (go (Do (Fix𝕗 I) ⨂ Do (Fix𝕗 I))))
      end)
     (Do (Fix𝕗 I))) vsplitr.
Fvalue
  ((cofix go (u : expr) : FType :=
      match u with
      | Ret t => regular_tree t
      | Do Prim𝕗 => Roll Prim𝕗
      | Do (Prod𝕗 x y) => Roll (Prod𝕗 (go x) (go y))
      | Do (Sum𝕗 x y) => Roll (Sum𝕗 (go x) (go y))
      | Do (Fix𝕗 _) =>
          Roll
            (Sum𝕗 (go prim)
               (go (Do (Fix𝕗 I) ⨂ Do (Fix𝕗 I))))
      end)
     (Do (Fix𝕗 I) ⨂ Do (Fix𝕗 I)))
     vcons; vsplitl; vcons; exact p1.
 Defined.

The reader is probably terrified, as we just defined a value by using rewriting tactics at each step. It turns out the resulting term is exactly the one we want, with no trace of unfolding.

 Eval compute in bintreeV.
= FVSumR
    (FVProd (FVSumL (FVPrim p1))
       (FVSumR
          (FVProd (FVSumL (FVPrim p1))
             (FVSumL (FVPrim p1)))))
: FValue bintree

The one hidden issue is that the implicit arguments are huge and difficult to infer. This is why we cannot take the returned term and use it as our definition.

 Fail Definition bintreeV' :=
   FVSumR (FVProd (FVSumL (FVPrim p1))
                  (FVSumR (FVProd (FVSumL (FVPrim p1))
                                  (FVSumL (FVPrim p1)))))
   : FValue bintree.
The command has indeed failed with message:
The term
 "FVSumR
    (FVProd (FVSumL (FVPrim p1))
       (FVSumR
          (FVProd (FVSumL (FVPrim p1))
             (FVSumL (FVPrim p1)))))"
has type
 "Fvalue
    (?t
     ⨁ (prim ⨁ ?u)
       ⨂ (?t0 ⨁ (prim ⨁ ?u0) ⨂ (prim ⨁ ?u1)))"
while it is expected to have type "FValue bintree".

We see that in the end, our type system is equirecursive as far as types and values are concerned. The construction of values does require the unfolding step because of Rocq's core being conservative around cofixpoints.

Conclusion

We have described tools for expressing a deep embedding of (positive) recursive types. All the tools we explored can be mixed and matched to a specific codebase's needs. How may one decide what is most appropriate?

If having isorecursive types is not a problem, considering explicit substitution first is probably the safest bet as this approach is compact and provides good recursors. On the other hand, if equirecursive types are what you are looking for, the coinductive trick might be a good fit.

When it comes to deciding for or against the functor fixpoint approach, two factors come to mind. The first is composability. Using mechanism described in [Swierstra2008] and Rocq's typeclass system, one can expect full composability of type systems. This means that to add Box to our second example, you would not need to change the rest of its logic. The second criterion is reasoning capabilities. As the functor stack grows in size, the eliminators provided by Rocq lose in power. From my experience, it is easy to eliminate values and types, but an induction relating a value and its type is much tougher to write. Perhaps consider this as future work. On the same note, the guard checking mechanisms are not free, as they too weaken inductive reasoning and send the user to a reasonably bearable layer of "dependent hell".

For my original usecase, I ended up going with the explicit unfolding with guard checking, as I intended to perform erasure on values anyway, which allowed me to recover some aspect of equirecursiveness. However, equirecursive types still seem to not be well-understood yet, and I wanted to document the corecursive trick somewhere.