1.8 KiB
1.8 KiB
Below explanation is by Anupam Jain.
Here’s how to derive final tagless from first principles -
- Final tagless is all about recursive data types.
- The usual way to encode recursive data types is to encode the recursion manually. For example -
data Tree = Leaf | Node Tree Tree
Here the definition for Tree mentions Tree. This is called the initial encoding.
- A common trick for any recursion is to parametrise the recursive type.
data Tree a = Leaf | Node a a
- Once you parametrise, you can also convert this to a class.
class Tree t where
leaf :: t
node :: t -> t -> t
This is called final encoding.
- How would you add values to this tree structure? Consider a tree with values at leaf levels, you could use multi parameter type classes like below but that has its own can of worms -
class Tree t v where
leaf :: v -> t
node :: t -> t -> t
One problem here is that the node function still has no information about the leaf values, which causes issues with type inference.
- A better solution is to use higher order type classes and
tagthe type of the tree -
class Tree t where
leaf :: forall v. -> t v
node :: forall v. t v -> t v -> t v
- Now it’s possible to add things that only work on some types of trees, for example sum all the leaves of the tree that works only for Integer trees -
sum :: t Int -> Int
This is the final tagless style.
- Note that you can do the same thing with GADTs.
data Tree v where
Leaf :: forall v. v -> Tree v
Node :: forall v. Tree v -> Tree v -> Tree v
and
sum :: Tree Int -> Int
But GADTs aren't in Haskell98, and were considered “advanced” when final tagless was proposed.