Codata/Data with Type Classes and Tagless Final Style

Lately I have been playing with tagless final style, a way of writing data structures in Haskell which is supposedly more extensible. I don't really see it as all that advantageous myself.

A trivial linked list example.

class List t where nil :: t cons :: Int -> t -> t instance List AsList where nil = AsList [] cons h (AsList t) = AsList (h : t) mylist :: List t => t mylist = cons 3 (cons 6 nil) 

In this way we transform our data structures into generic computer programs that are interpreted to output our data structures.

This post isn't really about tagless final style so I won't go into too much more detail. Really this post is about Scott encodings.

There is a funny little Combinator known as Mu which can be used to encode recursion in a tricky way.

newtype Mu f = Mu (forall a. (f a -> a) -> a) 

Of course in Haskell you don't really need such a cumbersome encoding. This is just theory.

I have found it useful on occassion to box up tagless final data on occasion even though you are not really supposed to.

newtype Box k = Box (forall a. k a => a) 

Notice something? In the core language type classes are desugared to record parameters implicitly passed in. So Box is just a funny variant of Mu!

There is another well known way of encoding recursion.

data Nu f = forall a. Nu a (a -> f a) 

This is suggestive of another style of encoding.

class Stream t where hd :: t -> Int tl :: t -> t 

data CoBox k = forall a. k a => CoBox a 

And indeed this works fine.

toList :: CoBox Stream -> [Into] toList (CoBox x) = loop x where loop x = hd x : tl x 

Tagless "final" style is revealed for what it really is. A style of open recursion based around functors.

This is suggestive of a new approach.

class Stream f where hd :: f a -> Int tl :: f a -> a cons :: Int -> a -> f a newtype Fix f = Fix (f (Fix)) toList :: Stream f => Fix f -> [a] toList (Fix x) = hd x : toList (tl x) 

But this is a digression for another time.