Scope of mu (μ) bindings in type theory

Question

A list in Haskell might look like this:

data List a = Nil | Cons a (List a)

A type theoretic interpretation is:

λα.μβ.1+αβ

which encodes the list type as the fixed point of a functor. In Haskell this could be represented:

data Fix f = In (f (Fix f))
data ListF a b = Nil | Cons a b
type List  a   = Fix (ListF a)

I'm curious about the scope of the earlier μ binder. Can a name bound in an outer scope remain available in an inner scope? Is, say, the following a valid expression:

μγ.1+(μβ.1+γβ)γ

...perhaps it's the same as:

μβ.μγ.1+(1+γβ)γ

...but then how would things change when the name is reused:

μβ.μγ.1+(μβ.1+γβ)γ

Are the above all regular types?

Belike

I think type List = ... ought to be type List a = .... – Analyze

Answer 1

Scoping of μ works no different from other binders, so yes, all your examples are valid. They are also regular, because they do not even contain a λ. (*)

As for equality, that depends on what sort of μ-types you have. There are basically two different notions:

• equi-recursive: in that case, the typing rules assume an equivalence

  μα.T = T[μα.T / α]

  i.e., a recursive type is considered equal to its one-level 'unrolling', where the μ is removed and the μ-bound variable is replaced by the type itself (and because this rule can be applied repeatedly, one can unroll arbitrary many times).

• iso-recursive: here, no such equivalence exists. Instead, a μ-type is a separate form of type with its own expression forms to introduce and eliminate it -- they are usually called roll and unroll (or fold and unfold), and are typed as follows:

  roll : T[μα.T / α] → μα.T

  unroll : μα.T → T[μα.T / α]

  These must be applied explicitly on the term level to mirror the equation above (once for each level of unrolling).

Functional languages like ML or Haskell usually use the latter for their interpretation of datatypes. However, the roll/unroll is built into the use of the data constructors. So each constructor is an injection into an iso-recursive type composed with an injection into a sum type (and inversely when matched).

Your examples are all different under the iso-recursive interpretation. The first and the third are the same under an equi-recursive interpretation, because the outer μ just disappears when you apply the above equivalence.

(*) Edit: An irregular recursive type is one whose infinite expansion does not correspond to a regular tree (or equivalently, can not be represented by a finite cyclic graph). Such a case can only be expressed with recursive type constructors, i.e., a λ that occurs under a μ. For example, μα.λβ.1+α(β×β) -- corresponding to the recursive equation t(β) = 1+t(β×β) -- would be irregular, because the recursive type constructor α is recursively applied to a type "larger" than its argument, and hence every application is a recursive type that "grows" indefinitely (and consequently, you cannot draw it as a graph).

It's worth noting, however, that in most type theories with μ, its bound variable is restricted to ground kind, so cannot express irregular types at all. In particular, a theory with unrestricted equi-recursive type constructors would have non-terminating type normalisation, so type equivalence (and thus type checking) would be undecidable. For iso-recursive types you'd need higher-order roll/unroll, which is possible, but I'm not aware of much literature investigating it.

Cottar

So an irregular type must contain a λ? Could you give an example? – Belike

Answer 2

Your μ type expressions are valid. I believe your types are regular as well since you only use recursion, sum, and products.

The type

T1 = μγ.1+(μβ.1+γβ)γ

does not look equal to

T2 = μβ.μγ.1+(1+γβ)γ

since inr (inr (inl *, inr (inl *)), inl *) has the second type but not the first.

The last type

T3 = μβ.μγ.1+(μβ.1+γβ)γ

is equal to (α-converting the first β)

μ_.μγ.1+(μβ.1+γβ)γ

which is, unfolding the top-level μ,

μγ.1+(μβ.1+γβ)γ

which is T1.

Basically, the scope of μ-bound variables follows the same rules of λ-bound variables. That is, the value of each occurrence of a variable β is provided by the closest μβ on top of it.

Vaucluse