Compare commits
2 commits
9db42001f4
...
ca5e28e244
Author | SHA1 | Date | |
---|---|---|---|
Sanchayan Maity | ca5e28e244 | ||
Sanchayan Maity | 0686c83ab2 |
68
FinalTagless.md
Normal file
68
FinalTagless.md
Normal file
|
@ -0,0 +1,68 @@
|
||||||
|
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.
|
|
@ -2,6 +2,8 @@ https://gist.github.com/CMCDragonkai/b203769c588caddf8cb051529339635c
|
||||||
|
|
||||||
http://iveselov.info/posts/2012-08-30-existential-types.html
|
http://iveselov.info/posts/2012-08-30-existential-types.html
|
||||||
|
|
||||||
|
https://markkarpov.com/post/existential-quantification.html
|
||||||
|
|
||||||
Great explanation by Anupam Jain in FPNCR Telegram channel :)
|
Great explanation by Anupam Jain in FPNCR Telegram channel :)
|
||||||
|
|
||||||
Everything gets a forall.
|
Everything gets a forall.
|
||||||
|
|
Loading…
Reference in a new issue