Semantics of
Recursive Types

This Scala definition is recursive:

enum List[A]:
  case Nil()
  case Cons(head: A, tail: List[A])

Syntax of STLC + recursive types:

\begin{aligned} \text{Terms} &\quad t ::= x \mid \lambda x. t \mid t_1 \; t_2 \\ \text{Types} &\quad T ::= T_1 \to T_2 \; \, {\color{#a626a4} \bf \mid X \mid \mu X. T} \end{aligned}

Additionally using unit, disjoint sum and pair types, we can define:

\text{List[A]} \triangleq \mu X. \, Unit + (A, X)

A recursive type can be unfolded:

\begin{aligned} \mu X. \, & Unit + (A, X) \\ \equiv \; & Unit + (A, \mu X. \, Unit + (A, X)) \\ \equiv \; & Unit + (A, Unit + (A, \mu X. \, Unit + (A, X))) \\ \end{aligned}

We want a typing rule to unfold:

\frac{\Gamma \vdash t : \mu X. T}{\Gamma \vdash t : T[X \mapsto \mu X. T]}

And one to fold:

\frac{\Gamma \vdash t : T[X \mapsto \mu X. T]}{\Gamma \vdash t : \mu X. T}

The value interpretation defines what it means for a value to have a syntactic type:

Fixpoint interp (T: Ty) (v: Value) : Prop :=
  match T with
  | TBool => exists b, v = vbool b
  | TFun A B =>
      exists env body, v = vabs env body
      /\ forall arg, interp A arg ->
           tinterp (arg::env) body (interp B)
  end.

The term interpretation defines what it means for a term to have a semantic type:

Definition tinterp (env: list Value) (t: Term)
                   (T: Value -> Prop) : Prop :=
  exists v fuel,
    eval fuel env t = Some (Some v) /\ T v.

The semantic typing judgement is defined as:

Definition sem_typed (tenv: list Ty) (t: Term)
                     (T: Ty) : Prop :=
  forall env, Forall2 interp tenv env ->
    tinterp env t (interp T).

It allows us to prove typing rules:

Lemma sem_typed_app: forall tenv f a A B,
  sem_typed tenv f (TFun A B) ->
  sem_typed tenv a A ->
  sem_typed tenv (tapp f a) B.
Proof.
  …
Qed.

\frac{ \Gamma \vDash f : A \to B \qquad \Gamma \vDash a : A }{ \Gamma \vDash f \; a : B }

Recursive types have a body, and an implicit de Bruijn binder. TVar i refers to i-th bound type.

Inductive Ty : Type :=
  …
  | TVar : nat -> Ty
  | TMu : Ty -> Ty.

Remember, we want \mu X. T \equiv T[X \mapsto \mu X. T].

Tentative interp using substitution:

Fixpoint interp_wrong (T: Ty) (v: Value) : Prop :=
  match T with
  …
  | TVar i => False
  | TMu B => interp (subst_ty 0 (TMu B) B)
  end.

We need step-indexing to break the circularity.

Semantic typing quantifies over all steps:

Definition sem_typed (tenv: TyEnv) (t: Term)
                     (T: Ty) : Prop :=
  forall env k,
    Forall2 (fun T v => interp T k v) tenv env ->
    tinterp env t (fun v => interp T k v).

Remember, we want \mu X. T \equiv T[X \mapsto \mu X. T].

But the well-founded version of interp gives us only \llbracket \mu X. T \rrbracket^k \equiv \llbracket T[X \mapsto\mu X. T] \rrbracket^{k-1}.

We define a later type \triangleright \, T to mean “T but one step later”, so we have: \mu X. T \equiv \triangleright \, T[X \mapsto\mu X. T].

Interpretation of “later”:

interp (TLater T') 0 v := True;
interp (TLater T') (S k') v := interp T' k' v;

We can then prove the following typing rules for recursive types:

\frac{ \Gamma \vDash t : \triangleright \, T[X \mapsto \mu X. T] }{ \Gamma \vDash t : \mu X. T } \qquad \frac{ \Gamma \vDash t : \mu X. T }{ \Gamma \vDash t : \triangleright \, T[X \mapsto \mu X. T] }

Can we get rid of these spooky triangles?

We can avoid the later type in the folding rule if we require that semantic types are downward closed:

T^{k} \subseteq T^{k'} \text{ for all } k' \le k

where S \subseteq T means \forall v, S \, v \implies T \, v.

This is not true with our definition, due to function types contravariance.

Downward-close interp by quantifying over smaller steps in the interpretation of function types:

interp (TFun A B) k v :=
  exists env body, v = vabs env body
  /\ forall j (Hj: j <= k) arg, interp A j arg ->
       tinterp (arg::env) body (interp B j);

Thanks to downward closure of interp, we can now have \llbracket \mu X. T \rrbracket^k \subseteq \llbracket T[X \mapsto\mu X. T] \rrbracket^k, so we can get rid of the later type in the folding rule:

\frac{ \Gamma \vDash t : T[X \mapsto \mu X. T] }{ \Gamma \vDash t : \mu X. T } \qquad \frac{ \Gamma \vDash t : \mu X. T }{ \Gamma \vDash t : \triangleright \, T[X \mapsto \mu X. T] }

Later types in the wild: Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers

Instead of using later types, can we move steps from the interpretation to the typing judgement?

\frac{ \Gamma \vDash_k t : \mu X. T }{ \Gamma \vDash_{k-1} t : \, T[X \mapsto \mu X. T] }

Definition sem_typed (tenv: TyEnv) (n: nat)
                     (t: Term) (T: Ty) : Prop :=
  forall env k, n < k ->
    Forall2 (fun T v => interp T k v) tenv env ->
    tinterp env t (fun v => interp T (k - n) v).

It makes sense:

Lemma sem_typed_distribute: forall env tenv n e T,
  sem_typed tenv n e T ->
  (forall k,
     Forall2 (fun T v => interp T k v) tenv env) ->
  tinterp env e (fun v => forall j, interp T j v).

For the application rule to go through, we also need to allow a gap inside the function interpretation:

Inductive Ty : Type :=
  …
  | TFun : nat -> Ty -> Ty -> Ty
  …

interp (TFun g A B) k v :=
  exists env body, v = vabs env body
  /\ forall j (Hjlo: g < j) (Hjhi: j <= k) arg,
       interp A j arg ->
       tinterp (arg::env) body (interp B (j - g));

So we still have noise in the syntax,
and now also in the typing rules:

\frac{ \Gamma \vDash_{i} f : A \to_j B \qquad \Gamma \vDash_{k} a : A }{ \Gamma \vDash_{i + j + k} f \; a : B }

Definition approx (k: nat) (F: SemTy): SemTy :=
  fun j v => j < k /\ F j v.

Definition wf (F: SemTy -> SemTy) : Prop :=
  forall k Z,
    approx (S k) (F Z)
    = approx (S k) (F (approx k Z)).

Lemma F_well_founded: forall tenv B,
  contractive B ->
  wf (fun X => interp (X :: tenv) B).

Definition contractive (T: Ty) : Prop :=
  match T with
  | TVar _ => False
  | TBool => True
  | TFun _ _ => True
  | TMu _ => False
  end.

Means the binder only occurs under other types.
\mu X. X is not contractive, but \mu X. X \to X is.