69 lines
1.8 KiB
Markdown
69 lines
1.8 KiB
Markdown
Below explanation is by Anupam Jain.
|
||
|
||
Here’s how to derive final tagless from first principles -
|
||
|
||
1. Final tagless is all about recursive data types.
|
||
2. The usual way to encode recursive data types is to encode the recursion manually. For example -
|
||
|
||
```haskell
|
||
data Tree = Leaf | Node Tree Tree
|
||
```
|
||
Here the definition for `Tree` mentions `Tree`. This is called the initial encoding.
|
||
|
||
3. A common trick for any recursion is to parametrise the recursive type.
|
||
|
||
```haskell
|
||
data Tree a = Leaf | Node a a
|
||
```
|
||
|
||
4. Once you parametrise, you can also convert this to a class.
|
||
|
||
```haskell
|
||
class Tree t where
|
||
leaf :: t
|
||
node :: t -> t -> t
|
||
```
|
||
|
||
This is called final encoding.
|
||
|
||
5. 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 -
|
||
|
||
```haskell
|
||
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.
|
||
|
||
6. A better solution is to use higher order type classes and `tag` the type of the tree -
|
||
|
||
```haskell
|
||
class Tree t where
|
||
leaf :: forall v. -> t v
|
||
node :: forall v. t v -> t v -> t v
|
||
```
|
||
|
||
7. 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 -
|
||
|
||
```haskell
|
||
sum :: t Int -> Int
|
||
```
|
||
|
||
This is the final tagless style.
|
||
|
||
8. Note that you can do the same thing with GADTs.
|
||
|
||
```haskell
|
||
data Tree v where
|
||
Leaf :: forall v. v -> Tree v
|
||
Node :: forall v. Tree v -> Tree v -> Tree v
|
||
```
|
||
and
|
||
|
||
```haskell
|
||
sum :: Tree Int -> Int
|
||
```
|
||
|
||
But GADTs aren't in `Haskell98`, and were considered “advanced” when final tagless was proposed.
|