effect system

Stream: Is there code for X?

[MangoIV]

To get more familiar with Lean, I want to start writing an effect system ala Haskell's fused-effects, has anybody tried that and/or has any warnings/ ideas?

[Henrik Böving]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/algebraic.20effects.20and.20handlers.3F/near/231512479

[MangoIV]

Yeah, it would be identical to mtl in terms of performance

[MangoIV]

So we get it to be fast if we specialise.

[MangoIV]

But if that’s already done then I don’t think there’s a fundamental issue?

[Henrik Böving]

further below there was this attempt at already doing it: https://git.envs.net/iacore/lean-eff

[MangoIV]

I’ve seen this but this seems to be Free monad based which is expected to be slow because of passes linear in effects

[MangoIV]

@Henrik Böving do you know whether there’s a specific reason why it would be slower than mtl-style which I gather is what lean does?

[Henrik Böving]

I don't know specific reasons myself no.

[MangoIV]

https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/mpc2015.pdf says:

Strict Languages In the absence of lazy evaluation, the inductive datatype
definition of the free monad is not practical.
Kammar et al. [9] briefly sketch an implementation based on delimited contin-
uations. Schrijvers et al. [17 ] show the equivalence between a delimited continua-
tions approach and the inductive datatype; hence the fusion technique presented
in this paper is in principle possible. However, in practice, the codensity monad
used for fusion is likely not efficient in strict languages. Hence, effective fusion
for strict languages remains to be investigated

I'll see how it goes heh