Wednesday, November 21, 2012

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(•β)
    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!


  1. Does this imply that you get general recursion back out of this style of recursive types?

  2. No, the really bizarre thing about this calculus is that it's still normalizing! See Nakano's 2000 LICS paper, "A Modality for Recursion" for a discussion of this issue.