From 93199cbcd796eca7e6bc2905974eb83b099041c6 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Tue, 12 Feb 2019 17:41:21 -0500
Subject: [PATCH] some notes on extending GTT with recursive types

---
 notes/recursive-types.org | 66 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 66 insertions(+)
 create mode 100644 notes/recursive-types.org

diff --git a/notes/recursive-types.org b/notes/recursive-types.org
new file mode 100644
index 0000000..0569381
--- /dev/null
+++ b/notes/recursive-types.org
@@ -0,0 +1,66 @@
+* Inductive, Coinductive and Recursive Types in GTT
+
+In order to apply the GTT model to non-trivial (statically typed)
+programs, we need to add some facility for inductive, co-recursive
+and/or recursive types.
+
+In principle this should not be a problem: the uniqueness principles
+are derivable in the presence of functoriality of connectives, and
+recursive types don't disrupt that. One difficulty is in establishing
+formally that the casts we derive for *recursive* types are actually
+values for recursive value types and stacks for recursive stack types.
+The usual presentation of recursive types by just adding in an
+isomorphism between (rec X. A) and A[rec X.A] is not sufficient
+because we would use something like the Y combinator to implement
+functorial stuff. This presentation is useful for minimalistic
+*operational* semantics, but is insufficient for a minimalistic
+*axiomatic* semantics.
+
+By contrast, Inductive and Co-inductive types present no difficulty at
+all. We add in an injection and the induction principle, with the
+induction principle being a *value form*. This makes it easy to show
+that the upcast implementation is a value. The same holds in the dual:
+the coinduction principle for co-inductive computations should be
+astack.
+
+Then the result should hold because any recursive type can be written
+using inductive types and *guarded* recursive types where guarded here
+means the variable occurs under a thunk.
+
+That is any recursive value type `rec X. A` can be written in the form
+`rec X. μ X'. [A]` where every occurrence of `X'` in `A` is strictly
+positive and every occurrence of `X` in `A` occurs under a thunk `U`.
+For example, take a simple Schemish CBV dynamic type:
+
+    rec D. 1 + (D * D) + U(D -> F D)
+
+The intuition about this type is that dynamically typed values are
+S-Expressions whose leaves are either nil or a unary procedure.
+The factorization makes this clearer:
+
+    rec D. μ T. 1 + (T * T) + U(D -> F D)
+
+We can think of `D` as the full recursive dynamic type and `T` as
+representing the inductive first-order component of the type:
+S-expressions.
+
+I haven't worked out the details but I think this observation should
+be sufficient to prove syntactically that upcasts are values/downcasts
+are stacks.
+
+
+* Precision and Equi-Recursion vs Iso-Recursion
+
+Static typing naturally lends itself to iso-recursion whereas dynamic
+typing naturally lends itself to equi-recursion. Gradual typing can
+accommodate this difference quite easily: in the cast calculus, the
+recursion is iso-recursive, but the *precision* is equi-recursive.
+
+But what rules should we have? Should we just state that they are
+equi-dynamic with their one level unrolling?
+
+    rec X. A == A[rec X.A]
+
+Or should we say that in fact they are *least/greatest fixed points*
+in the precision ordering? I haven't thought through the consequences
+yet but my gut says least fixed point will be more useful.
-- 
GitLab