In my previous post, I mentioned limitcolimit 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:

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 KnasterTarski 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 termlevel 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 termlevel 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!
Does this imply that you get general recursion back out of this style of recursive types?
ReplyDeleteNo, 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.
ReplyDelete