Saturday, December 4, 2010

Type-level Fix and generic folds

This article describes a fixpoint combinator for Haskell types, with some justification of why such a thing would be useful. It's meant to be an accessible introduction to material which is already covered elsewhere.

You'll need some basic Haskell knowledge, such as how to define and use polymorphic data types. And you might want to first study the value-level `fix` function. An excellent introduction can be found here.

This code is standard Haskell 98, except in the "GHC tricks" section.

Recursive types

Many useful data types are recursive:

``data Natural = Zero | Succ Natural     -- natural numbersdata List a  = Nil  | Cons a (List a)  -- listsdata Tree a  = Node a [Tree a]         -- rose trees``

In each case, the type declared on the left-hand side of "`=`" is mentioned on the right-hand side. This is fine, but just for fun let's see if there's another way.

We can imagine a language with a keyword "`self`", which refers to the type being defined:

``data Natural = Zero | Succ selfdata List a  = Nil  | Cons a selfdata Tree a  = Node a [self]``

Haskell doesn't have this keyword, so we'll make `self` into a type parameter:

``data NaturalF self = Zero | Succ selfdata ListF a  self = Nil  | Cons a selfdata TreeF a  self = Node a [self]``

We've changed the names because these aren't the types we wanted. They're non-recursive and each has an extra parameter.

To build the recursive type `Natural` using the non-recursive `NaturalF`, we need to "tie the knot":

``type Natural = NaturalF (NaturalF (NaturalF (NaturalF ...)))``

i.e.

``type Natural = NaturalF Natural``

But this is disallowed:

``````foo.hs:3:0:
Cycle in type synonym declarations:
foo.hs:3:0-30: type Natural = NaturalF Natural
``````

Since `type` defines a transparent synonym, this would generate an infinitely-large type-expression. Haskell disallows those. We need to hide the recursion behind a data constructor:

``newtype Natural = MkNat (NaturalF Natural)``

When we use this type, the "wrapper" constructor `MkNat` alternates with the constructors of `NaturalF`:

``toNatural :: Integer -> NaturaltoNatural 0 = MkNat ZerotoNatural n = MkNat . Succ \$ toNatural (n-1)``

Type-level `Fix`

So far this is just pointless complexity. We've replaced one type:

``data Natural = Zero | Succ Natural``

with two types:

``data    NaturalF self = Zero | Succ selfnewtype Natural       = MkNat (NaturalF Natural)``

Notice that the definition of `Natural` doesn't depend on the structure of natural numbers. Let's rename `Natural` to `Fix` and `MkNat` to `In`:

``newtype Fix   = In (NaturalF Fix)``

Then we'll abstract out `NaturalF` as a type parameter `f`:

``newtype Fix f = In (f (Fix f))``

Now `Natural` is just a synonym:

``type Natural = Fix NaturalF``

When we create values of type `Natural`, we still have "wrapper" constructors:

``toNatural :: Integer -> NaturaltoNatural 0 = In ZerotoNatural n = In . Succ \$ toNatural (n-1)``

Properties of `Fix`

Recall that the value-level `fix` function can be defined as

``fix f = f (fix f)``

This looks a lot like our type

``newtype Fix f = In (f (Fix f))``

The similarity is reflected at the type and kind levels:

``````GHCi> :t fix
fix :: (a -> a) -> a
GHCi> :k Fix
Fix :: (* -> *) -> *
``````

`fix` is a function which takes another function. `Fix` is a type constructor which takes another type constructor.

The types `Fix f` and `f (Fix f)` are isomorphic, and we'll want to convert between them. In one direction we'll use the data constructor

``In :: f (Fix f) -> Fix f``

and the other direction is easily defined as

``out :: Fix f -> f (Fix f)out (In x) = x``

Folding lists

So why bother writing types this way? Well, we usually don't. But factoring the recursion out of our data type enables us to factor the recursion out of our functions.

Consider taking the sum of a list:

``sumF :: (Num a) => List a -> asumF (In Nil)         = 0sumF (In (Cons x xs)) = x + sumF xs``

We traverse the structure with the combining function `(+)`, making a recursive call at each recursive position of the data type. How can we capture this pattern?

If we're reducing a value of type `List T` to get a result of type `R`, then a value of type `ListF T R` represents a list node with the recursive call's result already in place. So we might look for a function like

``cata :: (ListF a b -> b) -> List a -> b``

If we had this, we could write

``sumF :: (Num a) => List a -> asumF = cata f where  f Nil = 0  f (Cons x xs) = x + xs``

The function `f` specifies one step of reduction, and the magical function `cata` handles the rest.

The recursion pattern captured by `cata` is very similar to `foldr` on the built-in list type. In fact, we can implement `foldr` with `cata`:

``foldrF :: (a -> b -> b) -> b -> List a -> bfoldrF f z = cata g where  g Nil = z  g (Cons x xs) = f x xs``

If `foldr` is good enough, then what's so special about `cata`? The answer is that `cata` actually has this very general type:

``cata :: (Functor f) => (f a -> a) -> Fix f -> a``

I'll give the one-line definition of `cata` later. Writing it yourself is a fun puzzle.

We can see that we'll need this instance:

``instance Functor (ListF a) where  fmap _ Nil         = Nil  fmap f (Cons x xs) = Cons x (f xs)``

This `fmap` just takes a function and applies it to the `self`-typed field, if any. It's not recursive and has no relation to the `[]` instance of `Functor`, for which `fmap = map`.

Folding natural numbers

Let's put our generic `cata` to good use on another type. Every natural number is either zero, or the successor of another natural number:

``data NaturalF self = Zero | Succ selftype Natural = Fix NaturalF``

Again, `fmap` applies a function to each `self`-typed field:

``instance Functor NaturalF where  fmap _ Zero     = Zero  fmap f (Succ v) = Succ (f v)``

We can then use `cata` to define conversion to `Integer`:

``fromNatural :: Natural -> IntegerfromNatural = cata f where  f Zero     = 0  f (Succ n) = 1 + n``

as well as addition and multiplication:

``add :: Natural -> Natural -> Naturaladd n = cata f where  f Zero     = n  f (Succ m) = In \$ Succ mmul :: Natural -> Natural -> Naturalmul n = cata f where  f Zero     = In Zero  f (Succ m) = add n m``

Testing it:

``````GHCi> fromNatural (add (toNatural 2) (mul (toNatural 3) (toNatural 5)))
17

``````

Folding rose trees

Let's try one more structure, namely rose trees:

``data TreeF a self = Node a [self]type Tree  a      = Fix (TreeF a)instance Functor (TreeF a) where  fmap f (Node v xs) = Node v (map f xs)``

As before, `fmap` applies a function to each `self`-typed field. Since we have a list of these, we use `map`.

We define some traversals:

``valuesF :: Tree a -> [a]valuesF = cata (\(Node x xs) -> x : concat xs)depthF :: Tree a -> IntegerdepthF = cata (\(Node _ xs) -> 1 + maximum (0:xs))``

and test them:

``````GHCi> let n x = In . Node x
GHCi> let t1 = n 'a' []
GHCi> valuesF t1
"a"
GHCi> depthF t1
1
GHCi> let t2 = n 'a' [n 'b' [], n 'c' [n 'd' []], n 'e' []]
GHCi> valuesF t2
"abcde"
GHCi> depthF t2
3

``````

The definition of `cata`

As promised:

``cata :: (Functor f) => (f a -> a) -> Fix f -> acata g = g . fmap (cata g) . out``

Generic programming

We usually manipulate data because we care about its meaning. But some operations only depend on the data's structure. If we have some complex nested data value, we might want to pretty-print it, or serialize it with binary, or collect all the `String`s buried within. These are concepts which apply to any data type you like. Shouldn't our code be similarly adaptable?

This idea is called generic programming. Implementations in Haskell include syb, uniplate, multiplate, instant-generics, GHC's built-in support, and many other efforts.

Each of these libraries demands certain information about each data type, and in return provides some generic operations. In this view, our above development of `Fix` constitutes a really tiny generics library. We require

• that you write recursive types as `Fix F`, where `F` is non-recursive, and
• that you provide `instance Functor F`.

In return, you get the single generic operation `cata`, which reduces a recursive structure to a "summary" value, by replacing each constructor with an arbitrary computation.

Our toy generics library is simple, but it doesn't actually save much work. Using `Fix` adds noise to the code, and our `Functor` instances aren't much shorter than a custom fold function for each type. Conversely, our uses of `cata` aren't much simpler than explicit recursive traversals.

Practicality aside, I think it's cool to define folding "once and for all". I'm interested to learn (from you!) what else can be done with `Fix`'d data or similar techniques.

For a non-trivial generics library built around similar ideas, see multirec and the accompanying paper.

Odds and ends

Nomenclature

`Fix` is sometimes named `Mu`, because the Greek letter μ is used to represent least fixed points.

`cata` stands for catamorphism.

Some of this stuff shows up in "Evolution of a Haskell Programmer". They build a factorial function using not only catamorphisms but also zygomorphisms and paramorphisms. Tell your friends!

In TaPL there's a discussion of equirecursive versus isorecursive type systems. Haskell is in the latter category. `Fix f` is isomorphic to, but not equivalent to, `f (Fix f)`. The functions `In` and `out` provide the isomorphism. If we defined `Fix` using `data` instead of `newtype`, the isomorphism would fail because of the extra value `In ⊥`.

Isomorphisms

`NaturalF` is isomorphic to `Maybe`:

``data NaturalF self = Zero    | Succ selfdata Maybe    a    = Nothing | Just a``

The `Functor` instances are also the same.

`NaturalF` is also isomorphic to `ListF ()`, ignoring undefined values.

GHC tricks

While the above is standard Haskell, we can pull a few more tricks by using a couple of GHC extensions.

GHC could help us reduce boilerplate by deriving `Functor` instances.

With some GHC extensions, we can write `Show` for `Fix`:

``instance (Show (f (Fix f))) => Show (Fix f) where  showsPrec p (In x) = showParen (p >= 11) (showString "In " . showsPrec 11 x)``

Testing it:

``````GHCi> toNatural 3
In (Succ (In (Succ (In (Succ (In Zero))))))
``````

This requires `-XFlexibleContexts` `-XUndecidableInstances`. The latter is required because `f (Fix f)` is a syntactically larger type than `Fix f`, so GHC can't convince itself that instance resolution will definitely terminate. For well-behaved arguments to `Fix`, it works out. We'll have something like

``-- from aboveinstance (Show (f (Fix f)))       => Show (Fix f)-- from 'deriving (Show)' on NaturalFinstance (Show self)       => Show (NaturalF self)``

which instantiates to

``instance (Show (NaturalF (Fix NaturalF)))       => Show (Fix NaturalF)instance (Show (Fix NaturalF))       => Show (NaturalF (Fix NaturalF))``

and GHC is clever enough to resolve the mutual recursion.

Remarkably, GHC can derive this instance with `-XStandaloneDeriving`:

``deriving instance (Show (f (Fix f))) => Show (Fix f)``

That's how I got the precedence-correct code above, via `-ddump-deriv`.

1. As an aside: in a strict language the least and greatest fixed point actually diverge. (In fact in a language with subtyping, they can further divide up based on the variance of the base functor. For example:

https://github.com/scalaz/scalaz/blob/master/core/src/main/scala/scalaz/Recursion.scala

2. I think the idea originated from this paper "Functional Programming with Overloading and Higher-Order Polymorphism".

3. This comment has been removed by a blog administrator.

4. I just made a generic programming library around the exact same idea. Using the Foldable and Traversable type classes on top of Functor, you can do much more than just catamorphisms: http://hackage.haskell.org/package/fixplate

You can also make Show work in the Haskell98 setting with a minimal amount of extra boilerplate.

5. Nice article, thanks for the information. It's very complete information. I will bookmark for next reference
jaring futsal | jaring golf | jaring pengaman proyek |
jaring pengaman bangunan | jaring pengaman gedung
http://www.jual-jaring.blogspot.com/
http://www.agen-jaring.blogspot.com/
http://www.pancasamudera-safetynet.blogspot.com/
http://www.toko-jaring.blogspot.com/
http://www.pusat-jaring.blogspot.com/
http://jualjaringpengaman.blogspot.com/
https://pancasamudera.wordpress.com/
https://pasangjaringfutsal.wordpress.com/
https://jualtambangmurah.wordpress.com/
https://tokojaring.wordpress.com/
https://jualjaringfutsal.wordpress.com/
https://jaringfutsal.wordpress.com/

6. الفك والتركيب والتغليف والتحرك من خلال شركة نقل اثاث بجدة متميزة تحتاج الي ركن البيت للاستفادة من خدماتها التي لا تقدم غير خدمات نقل اثاث بجدة رائعة لتلبية طلبات العميل. فرؤية الشركة لدينا وضعت طريقة جيدة وضعت كخبراء في نقل الخدمات التي يحتاجها العملاء عند التعاون مع شركة نقل عفش بجدة فاختيار المواد الخاصة بك التي تستخدم في تغليف الاثاث فهذه المواد أو الأشياء ستكون موجودة على عتبة المنزل للتحرك بكل آمن و بقوة إلى المكان الذي ترغب فيه
شركة نقل الاثاث بالدمام
استخدام الأصول الأولى داخل الاستراتيجية التي تستخدمها شركة نقل عفش بالدمام لدينا تدفعنا إلى التفكير في إعطاء نوع من الخدمات المتميزة الي العملاء التي تترك نجاحا مباشرا يمكن أن تنقش على نفسية الزبائن التي تقدم لهم خدمة نقل العفش.فلدينا ميل إلى أن يشار جيدا إلى العاملون والفنين والمغلفون ان يقوموا بعملهم في شركة نقل اثاث بالدمام نتيجة للمعيار والتنمية والعقل
شركة نقل الاثاث بمكة
مجموعة معينة لدينا في شركة نقل عفش بمكة تساعدنا في خدمتك في أي وقت من اليوم، وأنهم على استعداد للبقاء على طول هذه الخطوط لاعطاءك خدمة متميزة عن باقي شركات نقل اثاث بمكة التي توجد بهذه المنطقة فلا أحد لدينا في خدمات النقل يترك شيئا حتي لا نقع في قليلا من السخط.
شركة تخزين الاثاث بالرياض
التعبئة والتغليف يبدأ بالعمل المتميز من اجل الحصول علي شركة تخزين عفش بالرياض متميزة تمتلك مستودعات تخزين اثاث بالرياض تحافظ علي الممتلكات الخاصة بكم من الخراب. كما ان التعبئة والتغليف على استعداد فريد للتعامل مع كل نوع من الأدوات والأشياء الزجاجية والمواد التي تميل إلى الإضرار أو تحمل بانتظام أسوأ جزء في عملية الحركة. فخدمات شركة تخزين اثاث بالرياض تقوم بإرسال أفضل مجموعة يتقن الوصول إليها في الوقت المناسب لتلبية طلب العميل وفقا لمتطلبات محددة خاصة بك في هذا المجال بسبب الطريقة التي كانت لدينا مجموعة من الخبراء في كيفية ادارة مستودعات تخزين اثاث منذ فترة طويلة في هذه الصناعة لفترة طويلة جدا.
شركة تخزين اثاث
شركة تخزين عفش