Saturday, September 12, 2009

Balanced brackets, finite sets and ordinal numbers

import Data.List
import Data.Set as Set
import Data.MultiSet as MultiSet -- not required

Balanced brackets

The Dyck language is the set of correctly parenthesised strings, like "(()(()()))".

data Dyck = Dyck [Dyck]

If you disregard the type constructor, an inhabitant looks like [[], [[], []]]. This type represents rooted trees. A rooted tree is a list of rooted trees. To convert a list of rooted trees to a rooted tree, you add the root. To convert back, you remove it.

Traversing the tree gives us the string:

string (Dyck x) = "(" ++ concatMap string x ++ ")"

To be honest, we're missing strings like ()() and the real Dyck type is [Dyck]. But it isn't important since these types are isomorphic as the picture above shows.

Hereditarily finite sets

If we use sets instead of lists, then we get hereditarily finite sets.

data HFS = HFS (Set HFS)

instance Eq HFS where
(==) (HFS x) (HFS y) = x == y

instance Ord HFS where
compare (HFS x) (HFS y) = compare x y

I was a bit surprised this works - to talk about Set HFS you have to implement comparision for HFS (since sets in Data.Set are binary search trees inside), but to implement comparision for HFS you have to define HFS first. Mutual recursion.

Here are A=\{\emptyset\} and B=\{\emptyset, \{\emptyset\}\}.

hfs = HFS . Set.fromList

setA = hfs [hfs []]
setB = hfs [hfs [], setA]

-- Every natural number can be written in binary:
data Binary = Natural -> Bool
-- We can write the exponents in binary too:
data Binary = Binary -> Bool
-- And, since a function into Bool represents some set,
data Binary = Set Binary

This is the same as the equation for HFS. To convert, recursively change a number to the set of exponents: 15 = {0,1,2,3} = {{},{0},{1},{0,1}} = {{}, {{}}, {{0}}, {{},{0}}} = {{}, {{}}, {{{}}}, {{},{{}}}}. It turns out there's a paper on this subject.

Ordinal numbers

Here's another example. If you don't know ordinal numbers skip this paragraph. I'll talk only about ordinals lesser than \epsilon_{0}. They can be written in the form


where a_i is a nonincreasing sequence of ordinal numbers. These a_i may be written recursively in that form too, and this recursion will always stop at some point. You can put coefficients after each \omega^{a_i} and require that the sequence is decreasing. This looks very similar to previous examples.

data ON = ON (MultiSet ON) -- (small) ordinal

instance Eq ON where
(==) (ON x) (ON y) = x == y

instance Ord ON where
compare (ON x) (ON y) = compare x y

on = ON . MultiSet.fromList

If you don't have multisets installed (cabal install multiset), you may use lists instead and think of them as multisets. Just be careful to always put the items on the list in nonincreasing order.

on [] is the empty sum - 0
on [on []] is \omega^0=1
on [on [on []]] is \omega^1=\omega
on [on [on []],on []] is \omega+1

It is interesting that the ordering given by instance Ord is exactly the standard ordering used in mathematics to compare ordinals. (It doesn't matter if you use multisets or sorted lists.) We got it out of nothing. Some other operations are also nicely implemented. The function \omega^x is simply f x = on [x]. The natural sum is sum of multisets (or merging of sorted lists). Normal addition isn't hard to write too.

Natural numbers

Peano's natural numbers can be written as

data Nat = Succ Nat | Zero


data Nat = Nat (Maybe Nat)

The common pattern

What we have done above was finding a type X such that X=F(X) for some type constructor F (lists, sets, multisets, Maybe). This is the fixed point of F!

data Y f = Y (f (Y f))
a = Y [Y [], Y [Y [], Y []]]

ghci> :t a
a :: Y []
ghci> :k Y
Y :: (* -> *) -> *

It works. However, we can't show it (deriving (Show) won't help).

Problem: Write an instance of Show. My solution is a workaround.


I do hope you tried and convinced yourself that something like

instance (Show (f a), Show a) => Show (Y f) where
show x = "Y " ++ (show x)

or similar won't work. What we want is, in pseudocode:

instance (forall a. Show a => Show (f a)) => Show (Y f) where
show x = "Y " ++ (show x)

In other words we require that f is a type constructor that conveys showability: if x is showable, then f x is showable too. I made a separate type class for such f.

class Show' f where
show' :: (Show a) => f a -> String

instance Show' [] where
show' = show

instance Show' Set where
show' = show

instance Show' Multiset where
show' = show

instance Show' f => Show (Y f) where
show (Y x) = "Y " ++ (show' x)

ghci> a
Y [Y [],Y [Y [],Y []]]

Much better solutions are given in comments.

The same boilerplate can be used for Eq and Ord to get two last examples as Y Set and Y Multiset. The instance of Ord gives you lexicographic order on the words in Dyck language (Y []), ordering of natural numbers written in binary (Y Set), ordering of natural numbers in unary (Y Maybe), and the normal ordering of ordinals (Y Multiset).


data H a = H (Maybe (Integer, a))

What is Y H? Write functions

convert :: that_type -> Y H
convert2 :: Y H -> that_type

If you're stuck, try to construct some value of type Y H.


Our fixed point equation is t = Maybe (Integer, t). I discussed this last time: these are lists. The conversion functions we are looking for are fold and unfold. I'll write another version of foldr I mentioned previously:

foldr2 :: (Maybe (a,b) -> b) -> [a] -> b
foldr2 f = foldr (curry (f . Just)) (f Nothing)

convert :: Y Helper -> [Integer]
convert2 :: [Integer] -> Y Helper

convert = unfoldr (\(Y (H x)) -> x)
convert2 = foldr2 (Y . H)

Many other recursive types like binary trees or infinite streams can be treated similarily.

I ought to add infinite lists are lurking here. Our balanced brackets type has other inhabitants, like [[],[],...] or [[[...]]]. You shouldn't worry about that. First, we don't have to use all values of the type: as long as we're careful, they won't show up unexpectedly and you may regard the type as the type of finite lists. Second, you can enforce that with strictness. Third and most important point, infinite lists appear quite naturally and they do have applications. I'll give an example later.

[Update: expanded on the hereditarily finite sets. Thanks to Ryan Ingram and Edward Kmett for great solutions of Show (Y f).]

[Update 17 Sep: I've found a paper (7 MB) covering very much of what I said. Haven't read it yet, but looks very promising.]


Ryan Ingram said...

This works for me, but sadly requires UndecidableInstances. I wonder if there is a way around that?

P.S. your comment box seems to disable cut/paste and arrow keys! Please fix? Also, all the buttons are in a language I don't know.

g said...

I changed the language. Thanks.

Are you using Firefox 3.0? It seems Blogger has some incompatibility issues ( I moved comments to a separate page.

Edward Kmett said...

You can use standalone newtype deriving to get the functionality you want. It lets you provide more context for the automatically generated instances.

{-# LANGUAGE StandaloneDeriving, FlexibleContexts, UndecidableInstances #-}
data Mu f = Mu (f (Mu f))
deriving instance Show (f (Mu f)) ⇒ Show (Mu f)
deriving instance Eq (f (Mu f)) ⇒ Eq (Mu f)
deriving instance Ord (f (Mu f)) ⇒ Ord (Mu f)