some thoughts on polymorphism

notes/polymorphic.org

+* Polymorphic GTT
+
+** Summary
+
+It seems like it's possibly *impossible* to combine the following
+properties:
+
+1. Graduality
+2. polymorphic casts to/from the dynamic type
+3. A safe type case for the dynamic type (i.e., intro/elim, beta,eta
+   for the dynamic type)
+4. Curry-style forall/exists, 
+5. Parametricity
+
+For the first 4, the following each seem to be valid workarounds, but
+each violates a principle of gradual/dynamic typing:
+1. Weaken graduality so we only have retraction, not projection
+2. Don't allow casting of polymorphic type variables, i.e., unknown
+   types are not "gradual"
+3. Disallow type case as a construct
+4. Use Church-style forall/exists, i.e., have the use of polymorphism
+   be *manifest* in the dynamic language, and instantiation is not
+   less than substitution.
+5. Parametricity theorems only apply to totally typed programs
+
+** Details
+First, we work in a GTT-like setting.
+Next, we consider the precision rules for incorporating polymorphism.
+
+First, we need to generalize type dynamism to open type dynamism.
+The following principles seem sensible for now
+1. Previous rules for GTT dynamism are *stable/fibred*: i.e., they
+   apply in any context. In particular, the dynamic type is the most
+   dynamic type *in any context*, meaning for instance that
+   X |- X <= ?
+2. Monotonicity: if X |- A <= B then for any A' <= B', A[A'/X] <=
+   B[B'/X]
+4. Functoriality: if X |- A <= B then forall X. A <= forall X. B
+5. Curry-style: if X |- A, then for any B, \forall X. A <= A[B/X]
+
+Contrast with the church-style rule which would be
+
+5. Church-style: (forall X. ?) <= ?
+
+The argument that something goes wrong comes down to what happens when
+we run type case when we've abstracted over some type variables?
+
+In particular what does
+
+    /\X. \x -> tycase (in_X x) { number? -> x + 1 | else. 0 } : forall X. X -> Num
+
+do?
+If instantiation is less dynamic than we know that choosing X = Num should get us:
+
+   (/\X. \x -> tycase (in_X x) { number? -> 1 | else. 0 }) [Num]
+   <=
+   \x -> tycase (in_Num x) { number? -> 1 | else. 0 }
+
+calling both sides with a number tells us that the LHS must be less
+dynamic than `ret 1`, so either it is equal to it or raises an error.
+On the other hand, instantiating X = String (really anything that
+doesn't satisfy number?) should get us that the LHS must be less
+dynamic than `ret 0`, but the parametricity theorem says that they
+need to produce the same answer, so they must both be error.
+
+on the other hand, consider the following slightly modified version:
+
+   (/\ X. \x -> tycase (in_X x) { number? -> 0 | else. 0 })
+
+should this raise an error?
+
+The runtime-sealing interpretation certainly would raise an error, but
+an eta principle for the dynamic type would say that this should be equivalent to
+
+   (/\ X. \x -> 0)
+
+i.e., that type-case is a *safe* operation, which it certainly is in
+a typical dynamically typed language.
+
+But how could we accomodate these semantics?
+It would seem to require that we run *both* sides of the computation
+and dynamically monitor them for equivalence, and that we would have
+to do this for every polymorphic type-case, possibly causing a huge
+runtime-overhead.
+
+This is possibly of interest as some kind of testing tool, but it's
+certainly *not* what sealing *does*, so we are left to ponder *why*
+sealing works the way it does, since it seems *unsound*: it rejects
+programs at runtime that are *semantically* polymorphic, but not
+satisfying the weirdly rigid notion of *syntactic* polymorphism: never
+interacting with a value in any way.
+