I agree with most of what you have said over several posts. There are two things I disagree with:
- Type systems are logical frameworks, and keeping as close to some logic as possible makes them most useful. In my own work I have included a Prolog like logic interpreter in the type system so that simple types are inferred (the inference algorithm is very short and elegant in logic too). Various ad-hoc type system extensions can naturally be expressed in logic, and the curry-howard isomorphism makes this an elegant approach. Logic and type - systems really are the same thing. - That this necessarily means poor performance, or that you have to compile like Haskell. My project uses unboxed types with no garbage collection and compiled imperative code in the IO monad directly to 'C' like code. So really performance is as 'C' but with a proper logical type system. In all likelihood I am not going to persuade everyone that this is the right approach for BitC, but I feel it is worth sharing the thoughts so far from my own work and discussing, as I might learn something useful. Keean. On 16 Feb 2015 06:07, "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
