Presentation for effect systems meetup on evidence passing

This commit is contained in:
Sanchayan Maity 2023-07-01 17:32:08 +05:30
parent 70b90c7cb9
commit 0e73a0ea05
6 changed files with 176 additions and 4 deletions

View File

@ -0,0 +1,11 @@
all:
make slide slideshow
slide:
pandoc -t beamer --include-in-header=./style.tex effects-evidence.md -f markdown-implicit_figures -V colorlinks=true -V linkcolor=blue -V urlcolor=red -o effects-evidence.pdf
slideshow:
pandoc -t beamer --include-in-header=./style.tex effects-evidence.md -f markdown-implicit_figures -V colorlinks=true -V linkcolor=blue -V urlcolor=red -i -o effects-evidence-slideshow.pdf
view:
zathura --mode=presentation effects-evidence.pdf &

Binary file not shown.

View File

@ -0,0 +1,160 @@
---
title:
- Effect Systems in Haskell - Part II
author:
- Sanchayan Maity
theme:
- default
classoption:
- aspectratio=169
---
# Agenda
- Cover two papers on Effect Systems.
* Generalized Evidence Passing for Effect Handlers[^1]
* Effect Handlers in Haskell, Evidently[^2]
- Some sections today's discussion isn't going to cover
* Efficiency/Performance of the library or effect system itself
* How to use effect systems
* Comparison of effect system libraries or how to choose one
[^1]: [Generalized Evidence Passing for Effect Handlers](https://dl.acm.org/doi/pdf/10.1145/3473576)
[^2]: [Effect Handlers in Haskell, evidently](https://xnning.github.io/papers/haskell-evidently.pdf)
# Recap, what's it all about
- **Separate syntax from semantics**
- **Interpret your abstract syntax tree in various ways**
- **Not losing performance while having both**
# Recap, why effect systems
- Monads to model effects but monads don't compose[^3]
- transformers/mtl has limitations
* Monad transformer stacks are rigid
* Doesn't allow handling something like `Reader Int (Reader String)` due to functional dependencies
```haskell
class Monad m => MonadReader r m | m -> r
```
* More than a few effects in stack become unwieldy
* n-square instances problem
[^3]: [Composing Monads by Mark Jones and Luc Duponcheel](https://web.cecs.pdx.edu/~mpj/pubs/RR-1004.pdf)
# Evidence passing based effect system libraries
- `EvEff`
- `MpEff`
- `speff`
- `cleff` based on `ReaderT IO`
- `effectful` based on `ReaderT IO`
- others?
# Some myths[^4]
- Many extensible effects libraries are implemented with free(r) monads (True)
- Therefore extensible effects = free(r) monads (False)
- Free(r) monads require certain mathematical concepts to grasp (True)
- Free(r) monads don't have very good performance (True, to some extent)
- Therefore extensible effects are slow, ivory-towerish toys (False)
[^4]: [ReaderT pattern is just extensible effects](https://喵.世界/2022/02/03/readert-is-extensible-effects/)
# Effects can be implemented in various way
- `free` monads
- `ReaderT IO`
- `CPS`
- `delimited continuations`
# What's the gist
- How do you pass the `handler` for the `effect`?
# Generalized control flow
- Languages that expose a yield primitive actually have a way to access delimited continuations! Central result of the paper by James-Sabry [^5][^6].
[^5]: [Yield: Mainstream Delimited Continuations](https://legacy.cs.indiana.edu/~sabry/papers/yield.pdf)
[^6]: [Delimited Continuations are all you need](https://www.youtube.com/watch?v=uRbqLGj_6mI)
# WTH are delimited continuations
- Delimited Continuations for Everyone[^7]
[^7]: [Delimited Continuations for Everyone](https://github.com/papers-we-love/pwlconf-info/tree/master/2017/kenichi-asai)
# How does one define an effect
```haskell
data Reader a e ans = Reader { ask :: !(Op () a e ans)
}
data State a e ans = State { get :: !(Op () a e ans)
, put :: !(Op a () e ans)
}
```
# Multi-prompt delimited control
```haskell
data Ctl e a = Pure { result :: !a }
| forall h b e' ans.
Control {
-- prompt marker to yield to (in type context `::ans`)
marker :: Marker h e' ans,
-- the final action, just needs the resumption (:: b -> Eff e' ans) to be evaluated.
op :: !((b -> Eff e' ans) -> Eff e' ans),
-- the (partially) build up resumption;
-- (b -> Eff e a) :~: (b -> Eff e' ans)` by the time
-- we reach the prompt
cont :: !(b -> Eff e a) }
data Context e where
CCons :: !(Marker h e' ans) -> !(h e' ans) -> !(ContextT e e')
-> !(Context e) -> Context (h :* e)
CNil :: Context ()
newtype Eff e a = Eff { unEff :: Context e -> Ctl e a }
```
# Key ideas
- Multi Prompt
- Evidence Passing
- Tail Resumptive Operations
- Bubbling Yields
- Short cut resumptions
- Monadic Translation
- Bind-inlining and Join-Point Sharing
# Dig in
- Dig in to the paper!
# Resources
- [Alexis King on "Delimited Continuations, Demystified" @ZuriHac2023](https://www.youtube.com/watch?v=DRFsodbxHQo)
- [GHC Proposal: Delimited continuation primops](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0313-delimited-continuation-primops.rst)
- [Delimited Continuations](https://calwoo.github.io/posts/2020-02-03-delimited.html)
- [Efficient Compilation of Algebraic Effect Handlers - Ningning Xie](https://www.youtube.com/watch?v=tWLPrPfb4_U)
- [From Folklore to Fact: Comparing Implementations of Stacks and Continuations](https://kavon.farvard.in/papers/pldi20-stacks.pdf)
- [Compiler and Runtime Support for Continuation Marks](https://www-old.cs.utah.edu/plt/publications/pldi20-fd.pdf)
- [Capturing the Future by Replaying the Past Functional Pearl](https://arxiv.org/pdf/1710.10385.pdf)
- [From Delimited Continuations to Algebraic Effects in Haskell](https://blog.poisson.chat/posts/2023-01-02-del-cont-examples.html)
- [Concurrent System Programming with Effect Handlers](https://kcsrk.info/papers/system_effects_feb_18.pdf)
- [Eff Directly in OCaml](https://arxiv.org/pdf/1812.11664.pdf)
- [Retrofitting Effect Handlers onto OCaml](https://kcsrk.info/papers/drafts/retro-concurrency.pdf)
# Questions?
- Reach out on
* Email: sanchayan@sanchayanmaity.net
* Mastodon: https://sanchayanmaity.com/@sanchayan
* Blog: https://sanchayanmaity.net
* Telegram:
- t.me/fpncr
- t.me/SanchayanMaity

Binary file not shown.

View File

@ -0,0 +1 @@
\logo{\includegraphics[height=0.5cm]{../images/Haskell.jpg}\vspace{220pt}\hspace{8pt}}

View File

@ -1,5 +1,5 @@
---
title:
title:
- Effect Systems in Haskell - Part I
author:
- Sanchayan Maity
@ -50,7 +50,7 @@ classoption:
- `effectful` based on `ReaderT IO`
- others?
# Free monads
# Free monads
Given a `Functor f`, `Free f` is a `Free` monad.
@ -125,7 +125,7 @@ data FFree f a where
Pure :: a → FFree f a
Impure :: f x → (x → FFree f a) → FFree f a
instance Monad (FFree f) where
instance Monad (FFree f) where
Impure fx k >>= k = Impure fx (k >>> k)
```
@ -189,7 +189,7 @@ data Eff r a where
- Reach out on
* Email: sanchayan@sanchayanmaity.net
* Mastodon: https://sanchayanmaity.com/@sanchayan
* Mastodon: https://sanchayanmaity.com/@sanchayan
* Blog: https://sanchayanmaity.net
* Telegram:
- t.me/fpncr