Codata/Data with Type Classes and Tagless Final Style

mspondee profile image Molossus Spondee ・2 min read

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.

Posted on by:


markdown guide