Polymorphism and limit-colimit coincidence in reactive languages

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 F is positive whenever we have a function:

  map : ∀α,β. (α → β) → F(α) → F(β)

with the expected properties that:

1. map [A] [A] id = id
2. (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 lattice and f is monotone. Intuitively, you can see map 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 μ̂α.F(•α), where 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!