PLEASE HALT THE MONAD DEBATE HERE IMMEDIATELY It's a very good and very important debate to have. In order for us to have any hope of finding it later, it is important that it occur under a different subject heading.
Matt: Please re-post this email under a different subject line. All: Please reply on the appropriate monad thread rather than here. I really thought I had already asked us not to mix up this thread with the monad discussion! shap On Sun, Feb 15, 2015 at 10:07 PM, Matt Oliveri <[email protected]> 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 > >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
