`Mu`

can be implemented in Scala and how you can use it to derive a generic model for catamorphism and some cool type level data structures. Recently I have been reading TAPL by Benjamin Pierce that gives a very thorough treatment of the theories and implementation semantics of types in a programming language. And

`Mu`

we meet again. Pierce does a very nice job of explaining how `Mu`

does for *types*what

`Y`

does for *values*. In this post, I will discuss my understanding of

`Mu`

from a type theory point of view much of what TAPL explains. As we know, the collection of types in a programming language forms a category and any equation recursive in types can be converted to obtain an endofunctor on the same category. In an upcoming post I will discuss how the fixed point that we get from

`Mu`

translates to an isomoprhism in the diagram of categories.Let's have a look at the

`Mu`

constructor - the fixed point for type constructor. What does it mean ? Here's the ordinary fixed point combinator for functions (from values to values) ..

`Y f = f (Y f)`

and here's

`Mu`

`Mu f = f (Mu f)`

Quite similar in structure to

`Y`

, the difference being that `Mu`

operates on type constructors. Here `f`

is a type constructor (one that takes a type as input and generates another type). List is the most commonly used type constructor. You give it a type `Int`

and you get a concrete type `ListInt`

.So,

`Mu`

takes a type constructor `f`

and gives you a type `T`

. This `T`

is the fixed point of `f`

, i.e. `f T = T`

.Consider the following recursive definition of a List ..

`// nil takes no arguments and returns a List data type`

nil : 1 -> ListInt

// cons takes 2 arguments and returns a List data type

cons : (Int x ListInt) -> ListInt

Taken together we would like to solve the following equation :

`a = Unit + Int x a // ..... (1)`

Now this is recursive and can be unfolded infinitely as

`a = Unit + Int x (Unit + Int x a)`

= Unit + Int x (Unit + Int x (Unit + Int x a))

= ...

TAPL shows that this equation can be represented in the form of an infinite labeled tree and calls this infinite type regular. So, generally speaking, we have an equation of the form

`a = τ`

where1. if

`a`

does not occur in `τ`

, then we have a finite solution which, in fact is `τ`

2. if a occurs in

`τ`

, then we have an infinite solution represented by an infinite regular treeSo the above equation is of the form

`a = ... a ...`

or we can say `a = F(a)`

where `F`

is the type constructor. This highlights the recursion of types (not of values). Hence any solution to this equation will give us an object which will be the fixed point of the equation. We call this solution `Mu a . F`

. Since

`Mu a . F`

is a solution to `a = F(a)`

, we have the following:`Mu a . F = F {Mu a . F / a}`

, where the rhs indicates substitution of all free `a`

's in `F`

by `Mu a . F`

.Here

`Mu`

is the fixed point combinator which takes the type constructor `F`

and gives us a type, which is the fixed point of `F`

. Using this idea, the above equation (1) has the solution `ListInt`

, which is the fixed point type ..`ListInt = Mu a . Unit + Int x a`

In summary, we express recursive types using the fix point type constructor

`Mu`

and show that `Mu`

generates the fixed point for the type constructor just like `Y`

generates the same for functions on values.
## No comments:

Post a Comment