show how recursive types work as least pre-fixed points

notes/recursive-types.org

@@ -61,6 +61,89 @@ 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*
+Or should we say that in fact they are *least pre-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.
+
+The lfp rules are simple. We say first that the type mu X. A is a pre-fixed point of X.A:
+
+-----------------------
+A[mu X. A/X] <= mu X. A
+
+and second that it is the *least* such pre-fixed point:
+
+A[A'/X] <= A'
+-------------
+mu X. A <= A'
+
+From this we can derive that lfp are functorial:
+
+X <= X' |- A <= A'
+--------------------
+mu X. A <= mu X'. A'
+
+by using the lfp property and monotonicity of all connectives:
+
+A[mu X'. A'/X] <= A'[mu X'. A'/X'] <= mu X'. A'
+-----------------------------------------------
+A[mu X'. A'/X] <= mu X'. A'
+---------------------------
+mu X. A <= mu X'. A'
+
+* Recursive Types as a Precision-Least Pre-fixed Point
+
+Here's an interesting idea, somewhat inspired by denotational
+semantics. What if the recursive type mu X. A were just *defined* to
+be the least pre-fixed point of X.A in the dynamism ordering? That is,
+we treat mu X. A similar to the dynamic type ? in that we only
+interact with it via casts.
+
+Then we could define for example:
+
+G |- V : A[mu X. A/X]
+------------------------------------------------------
+G |- roll(V) : mu X. A =: <mu X. A <--< A[mu X. A/X]>V
+
+and
+
+G |- V : mu X. A
+------------------------------------------------------------
+G |- unroll(V) : A[mu X. A/X] =: <A[mu X.A/X] <--< mu X.A>V
+
+where the dynamism derivation of the latter comes from
+
+A <= A  and  A[mu X. A/X] <= mu X.A
+-------------------------------subst
+A[A[mu X.A/X]/X] <= A[mu X.A /X]
+----------------------least pre-fixed point
+mu X. A <= A[mu X.A/X]
+
+we can prove that roll, unroll form an isomorphism from our proof that
+equi-dynamic types are isomorphic.
+
+What's even cooler than that is we can derive reduction rules:
+
+Say we have a derivation
+A[A'/X] <= A'
+-------------lfp
+mu X. A <= A'
+
+Then there is an upcast
+
+<A' <--< mu X. A>V
+
+We can derive a reduction rule for this cast when it is applied to roll:
+
+<A' <--< mu X.A>roll(V)
+= <A' <--< mu X.A><mu X. A <--< A[mu X.A/X]>V
+= <A' <--< A[A'/X]><A[A'/X] <--< A[mu X.A/X]>V
+
+By coherence of upcasts, we need only verify that appropriate type
+dynamism derivations can be constructed:
+1. A[A'/X] <= A'
+2. A <= A   and   mu X.A <= A'
+   -----------------------------subst
+   A[mu X.A/X] <= A[A'/X]
+
+TODO: look at the downcasts involving mu, and dualize everything for
+computation types.