Crud. I actually want to reply to Matt's note, so I'm going to re-post it here.
In the other thread, Matt Oliveri wrote: I split this reply into two emails, one for a debate about monadic effects, one for everything else. This one is the monad debate. On Sun, Feb 15, 2015 at 9:42 AM, Keean Schupke <[email protected]> wrote: > Then the question is, if you have a general mechanism for > modelling things that effects behave like, why would you introduce another > mechanism into your type system. In my experience simpler, generic things > produce better, simpler type systems. That's a good question. My answer is that the way monads are used to encode effects in Haskell is a hack. Monads describe the structure of the way effects are reasoned about. (And other things, of course.) But they are just a magic trick when it comes to how effects are really implemented. As a pure language, Haskell is forced to acquire similar structures to math and logic for all that it does. This is a defect, because this structure is often artificial, from an implementation point of view. Monadic effects aren't the only misfeature where the structure of logic leaks onto your implementation. They probably aren't even the worst offender. But it's still not right. You might be aware that monadic types are logically similar to modal types. The difference is that modes are usually baked into the type system, which gives the language designer a more transparent way to make a special case of how they're implemented. In fact, effect systems are (probably) essentially modal type systems, using effect monads as the modes. But baking the effects into the system is the right way to make their implementation a special case. Again, the computer already has all the effects of the IO monad. Throwing them away with a pure language, then bringing them back via an encoding with monads is cutting corners. It's easy to do monads on top of a pure system. But this is not doing justice to the difference between how preexisting effects, and custom monadic functionality really ought to be implemented. > Parametric Monads use parameter sets > to mark effects in exactly the fine-grained way you describe. You should > read this: > > http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf I haven't read it, but I'm pretty sure I know the gist of it from what you've said. I've done similar things. > On 15 Feb 2015 10:34, "Matt Oliveri" <[email protected]> wrote: >> The difficulty of composing monads might be due to the huge amount of >> extra generality of monads over effects. The problem of composing >> monads in general is not a problem for BitC, AFAICT. > > Parametric monads solve a lot of the composition problems. Again monads are > simply a category, a bunch of things with similar properties that are > abstracted into a common pattern. If you don't allow the common pattern to > be expressed, then you will have to write boilerplate for each thing. That sounds right. In particular, monadic effects need not have composition problems, since they are, after all, effects. >> I don't see any reason why you couldn't do concurrent programming in >> the IO monad. But I also don't see any reason why BitC would _want_ >> to. > > Because the ML way of having impure arrows throws away control of > side-effects. And an effect system puts that control right back. > Taking the monadic approach leads to a much nicer, more > general type system that more closely resembles a logical-framework. Yes, it does resemble logic. That's the problem. See above. > These > things become important when you want to start proving things about > programs. I don't believe it. It's still cutting corners. You can reason about a program no matter how it's written, if it has formal semantics. Haskell's philosophy is to mix the programs and proofs together. But this restricts what you can express in either implementations or math, compared to keeping them separate. > Its also worth reading this: > > http://r6.ca/blog/20110520T220201Z.html I'll take a look. > As you can see IO is actually a datatype with a special deconstructor which > is where the side effects happen. It just happens to fit a composition > pattern that is called a Monad. Being monadic is an emergent property of the > semantics of the datatype, not something arbitrary imposed by the language. I hope by now you realize that I don't think it's arbitrary to view effects as monads, but that to organize their implementation based on how to reason about them is the tail wagging the dog. > So the discussion is not monadic or not-monadic, but are side effects best > represented by arrows or datatypes. That's not really the question either. It's whether we want to expose effects in the type system as a mere datatype, or some other type operator with special semantics. Either way, we can mix the operator into the arrow if it's not too yucky, but we don't have to. > On the basis that we need to represent > arities in types, separately from tuples, then we would need pure arrows, so > that applying a curried function does not result in side-effects. You are prescribing chemotherapy to treat a cold. It's no big deal to pick some other syntax for multi-arg applications and tuples, if indeed we want a difference. This idea that pure arrows is the right way to do multi-arg functions seems to be an artifact of the ML vs. Haskell war. Yeah, ML curries impure functions, which is wonky, and needlessly complicates the effects situation. But Haskell is not the only one doing it right. Most languages do it right by not frivolously currying in the first place. > We could > introduce a new type of arrow like this: > > f :: a-> b ~> c > > Where ~> is side-effectful application, however to add effects would require > a whole lot of different flavour arrows and ways to compose different arrow > types... its starting to look a mess. Effect systems _are_ a mess. But the mess is real, not accidental. BitC cannot afford to hide the way effects really work from the programmer, and it _definitely_ cannot afford to simply implement effects as if they were a datatype. > but I would rather use an existing mechanism like datatypes: > > f :: a -> b -> Eff e c > > Where 'e' is the set of inferred effects in function 'f'. Now it just so > happens that we can compose effects, and the composition rules share the > structure of a Monad. So if we declare (Eff e) to be a monad, with the > relevant composition rules, we can infer composed effects. Again, I'm not surprised one can compose effects, no matter how they're expressed. In many effect systems, the effects are gathered into a set, which is a parameter of the arrow, you know. > To me there is a natural structure to type-systems, and that should be > followed, rather than just making stuff up. That sounds great. If only Haskell hadn't just made up the idea that side-effecting programs are built on top of pure ones. Seriously, what you have to realize is that there's a natural structure to implementation techniques too. When we screw with _that_, performance goes down the hole. We can sort-of buy the privilege of writing programs that look nothing like their implementation, by using tremendously complicated optimizers. That's GHC, basically. But even that's not as good as actually being able to deal more directly with the implementation. I hear optimizing Haskell programs is strange, finicky, and hard, and it totally ruins any aesthetic appeal one might ascribe to regular Haskell code. Optimizing BitC should ideally be straightforward, if you know the hardware.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
