Effects Without Monads: Non-determinism (Back to the Meta Language)

[xacid]

https://arxiv.org/pdf/1905.06544.pdf

Effects Without Monads: Non-determinism
Back to the Meta Language

Oleg Kiselyov, 2019

Comments

[juan_gandhi]

Ok, in 2019 he just looks funny.
Sad.

[xacid]

imho, there he is more adequate:

http://okmij.org/ftp/Computation/having-effect.html

[juan_gandhi]

Non-categorical flavor of all this gets me puzzled. What's the point? Building a whole theory about pretty simple things, if expressed categorically.

[xacid]

His point is a practical implementation of non-trivial extensible denotational semantics with effects in a DSLs embedded into existing typed functional languages like Haskell, OCaml, Scala, Rust, F#.

The idea is that any effect is just an interaction with some external context (what is a composition of handlers) through simple freer monad T q a = Done a | Req q (a -> T q a) where q is type of effects list (union) and a is a domain, or in simple cases it could be even a just direct composition of algebras. Extensibility is achieved through tagless final encoding.

Also he has some intuition of lambda or p calculus as effects systems - so as even variable dereference, abstraction and application are really effects (at least in parallel and distribute environments, but even just an environment for bound variables is a stateful effect in denotation).