In my previous post, I mentioned limit-colimit coincidence, and how the ability to define fixed points makes that possible. It turns out there's a very pretty way of using parametricity to encode this. Now, inductive and coinductive types are definable in System F as follows:
μα. F(α) = ∀α. (F(α) → α) → α νβ. F(β) = ∃β. β × (β → F(β))
It's possible to show using parametricity that these type definitions
are actually the inductive and coinductive types we expect, whenever
F is a positive type. That is, a type constructor
is positive whenever we have a function:
map : ∀α,β. (α → β) → F(α) → F(β)
with the expected properties that:
map [A] [A] id = id
(map [A] [B] f); (map [B] [C] g) = map [A] [C] (f; g)
In lattice theory, you can apply the Knaster-Tarski theorem to get
a fixed point of a function
f : L → L when L is a complete
f is monotone. Intuitively, you can see
as the proof that the functor
F is monotone (really, functorial)
in the lattice (really, category) of types.
It turns out that in a temporal setting, we also need to specify that we can invoke the algebra/coalgebra operations at multiple times, which we can specify using the modal stability connective □A, which changes the definitions to:
μα. F(α) = ∀α. □(F(α) → α) → α νβ. F(β) = ∃β. β × □(β → F(β))
Now, suppose we have a Nakano style recursive type
every occurrence of the recursive type occurs beneath a delay modality.
Then, assuming that F is positive, we can show how to embed elements of
νβ. F(•β) into elements of
μα. F(•α) as follows:
embed : να. F(a) → μα. F(α) embed pack(β, (seed, h₁)) = // seed : β, h₁ : □(β → F(•β)) let stable(f) = h₁ in // f : β → F(•β) at all times Λα. λh₂. // h₂ : □(F(•α) → α) let stable(g) = h₂ in // g : F(•α) → α at all times let loop : β → α = fix loop = λb:β. // in body, loop can only be used later g(map [•α] [•β] (λd:•β. let •b' = d in •(loop b')) // has type •β → •α (f b)) // has type F(•β) in loop seed
This suggests that guarded term-level recursion is enough to make certain
least and greatest fixed points collapse. I say "suggests", since proving that
these types are equivalent requires a parametric model, which I haven't actually
constructed yet. It also means that just polymorphism and the stability modality
□A are enough to construct an interesting reactive language, even
without a term-level fixed point
fix x. e.
This function, minus the temporal staging, should also work for F plus ordinary general recursion. I had just never thought about how the coincidence plays out syntactically when you don't take recursive types as a primitive!