News for hackers. Stuff that matters.

A comment on The limits of type theory: computation vs. interaction. Parent comment

Re:The limits of type theory: computation vs. interaction by cousin_it on Monday June 08, 2015 @12:57PM (#9680403)
People keep getting it wrong because monads are the wrong abstraction. The right abstraction is algebraic effects. They correspond much more directly to "interactions", because the types of effect handlers are exactly the types of allowed "interactions". As a bonus, algebraic effects commute with each other, while monads usually don't. (For example, there's a gratuitous difference between Maybe (List a) and List (Maybe a), and people who want to program with effects shouldn't have to think about such differences.)

There was a great quote saying that when you get something almost right but not completely right, you have to explain it to people over and over again. IMO people should pay more attention to that quote, it applies to monads perfectly.

[ Parent | on HN ]
Re:The limits of type theory: computation vs. interaction by dragonwriter on Monday June 08, 2015 @02:17PM (#9680990)
> For example, there's a gratuitous difference between Maybe (List a) and List (Maybe a)

In what sense is the difference "gratuitous"? Seems to me its a pretty significant, meaningful difference and that the two types represent radically different things.

[ Parent | on HN ]
Re:The limits of type theory: computation vs. interaction by cousin_it on Monday June 08, 2015 @02:25PM (#9681082)
Yes, I agree. But that difference is irrelevant and distracting to people who just want to do effectful programming. A computation that's allowed to call handlers A and B should be always convertable to a computation that can call handlers B and A. There's no point in using a more general abstraction (monads) that doesn't give you the operations you need.
[ Parent | on HN ]
Re:The limits of type theory: computation vs. interaction by dllthomas on Monday June 08, 2015 @05:39PM (#9682639)
This is handwavy and wrong.

Imagine we have two effects that need handling. One is "failure" - terminating the computation and propagating the fact of failure. The other is "emit", producing some value for an external process.

If I combine these two, the question arises as to the behavior of "emit 3; fail" - does it emit or bury the 3? Depending on the circumstance, either could be useful, and it's a tremendous difference that is neither irrelevant nor distracting.

[ Parent | on HN ]
Re:The limits of type theory: computation vs. interaction by cousin_it on Tuesday June 09, 2015 @03:05AM (#9684421)
If I understand algebraic effects correctly, the computation "emit 3; fail" might emit or bury the 3 (or do something even more strange) depending on which effect handlers you pass to it. Keeping effect handlers outside of computations is what allows for commutativity etc.
[ Parent | on HN ]
Re:The limits of type theory: computation vs. interaction by dllthomas on Tuesday June 09, 2015 @01:08PM (#9687101)
I am not objecting to algebraic effects; I am objecting to your calling the different orderings "irrelevant and distracting." It is a vitally important detail that can easily make the difference between correct and broken code. When a code snippet can be written making no assumptions about ordering, exposing it as polymorphic with respect to ordering is great. When it must rely on a particular ordering, pretending it doesn't will bite you.
[ Parent | on HN ]
Re:The limits of type theory: computation vs. interaction by danghica on Monday June 08, 2015 @02:12PM (#9680951)
I agree with monads, not so sure about algebraic effects. Having to define the effect feels like "simulation" to me. It's OK for a meta-language, but to me it feels wrong for actual effectful programming.
[ Parent | on HN ]
Re:The limits of type theory: computation vs. interaction by cousin_it on Monday June 08, 2015 @02:32PM (#9681156)
Can you explain your wish in more detail? I feel like you might have a point, but I'm having trouble verbalizing it for myself :-(
[ Parent | on HN ]
Re:The limits of type theory: computation vs. interaction by Dewie3 on Tuesday June 09, 2015 @05:09AM (#9684726)
Do you know of any introduction to algebraic effects that is more programming-focused than theoretical?
[ Parent | on HN ]
Re:The limits of type theory: computation vs. interaction by cousin_it on Tuesday June 09, 2015 @05:46AM (#9684861)
Here's one: http://math.andrej.com/2010/09/27/programming-with-effects-i...
[ Parent | on HN ]