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.
Top comments (0)