4 ms·

> Pretending that modern type systems provide anything near an adequate control of effects is misleading at best Adequate for what exactly? Programmers all ar

• pron 11y ago
  > I've been writing Haskell every working day for over two years and one of the things I most appreciate about it is its effect system. Haskell's type system is not an effect system. > And pray tell, what would an effect system look like that's not monadic? Something like this -- http://research.microsoft.com/en-us/projects/koka/ http://research.microsoft.com/en-us/projects/koka/ -- but with notions of ordering and better composition. > Hope it appears at some point! It's up there now.
  • tome 11y ago
    > Haskell's type system is not an effect system. Haskell's type system models effects through things like monads, applicatives, categories. If you don't agree with this then you're going to have to tell me what your definition of "effect system" and "type system" are. > Something like this -- http://research.microsoft.com/en-us/projects/koka/ http://research.microsoft.com/en-us/projects/koka/ -- but with notions of ordering and better composition. I'll give it a look, thanks, > It's up there now. Wow, that was good timing!
    • pron 11y ago
      > Haskell's type system models effects through things like monads, applicatives, categories. If you don't agree with this then you're going to have to tell me what your definition of "effect system" and "type system" are. Haskell's type system, as you rightly note, models effects through types on return values combined with monads. But Haskell code -- since the language is pure -- by definition has no effects. It triggers effects in the runtime by returning monadic values, but it doesn't actually have effects (if it did, it wouldn't have been pure). An effect system[1] describes the effect impure functions have rather than the types of the values they return (i.e. they don't require effects to be modeled as values). An example of an effect system is Java's checked exceptions, or Koka's effects. > Wow, that was good timing! You'll be disappointed if you're expecting a discussion of effect systems... [1]: https://en.wikipedia.org/wiki/Effect_system https://en.wikipedia.org/wiki/Effect_system
      • tome 11y ago
        > > Wow, that was good timing! > You'll be disappointed if you're expecting a discussion of effect systems... I'm expecting a discussion of why continuations are enough.
        • pron 11y ago
          That's discussed but without a proof. I'm working on a blog post (to be published today or tomorrow) which links to the proof and provides a more in-depth discussion.
          • tome 11y ago
            Great, I'm looking forward to it!
      • tome 11y ago
        OK, I think there's a fundamental misunderstanding at play here, of what purity, effects and monads are. Koka's effects system is monadic! Crazy huh? Well look: function main() { bind(foo, bar) } function foo() { println("Returning 3") return 3 } function bar(x) { println("Adding 1 to my argument and printing") y = x + 1 println(y) } function bind(x : () -> e a, f : a -> e b) : e b { y = x() return f(y) } function return_(x) { return x } I can define return and bind generically over effects e just like in Haskell! Checked exceptions in Java are also monadic! Well, in a sense but I don't know enough about Java to write down the types correctly. Maybe the types can't even be written, but it doesn't stop the nature of checked exceptions being monadic. Specifically, if I have A method1() throws Exception1, Exception2, ... B method2(A) throws Exception1, Exception2, ... then combining them thusly method2(method1()) is exactly binding in a monad. It's not a monad defined as a specific datastructure in your language, but it is a monadic operation. It's pretty much the same monadic operation as the bind in the hypothetical "universal monad"[2] you propose in your talk. The reason effects are monadic is that if you have a computation C1 that does effects of type E and that returns a value of type A, and an computation C2 that does effects of type E and that takes a value of type A as argument and returns a value of type B, then you can combine them to form a function that does effects of type E and returns a value of type B. This is the bind of a monad! Different languages may have different levels of support for the syntax of effects/monads at the type or value level, for programming generically with effects/monads, and for defining your own and combining them, but the fact remains that effects are monadic. The misunderstanding is that you seem to think a monad is a value along with some extra stuff. In particular, you think that in a pure language a value of type IO is a value along with some extra stuff. This is wrong! It's understandable that you came to this conclusion given the thousand misleading monad tutorials that say "a monad is a value in a context" or "when you use IO you are building up a computation for an impure runtime to run". But this is wrong! Haskell is not a "pure language". "Pure language" is a not a well-defined concept. It's simply a neat slogan to summarize one of Haskell's characteristics without getting technical. What is pure in Haskell is let bindings and function application. That's it. (In fact I would classify Koka under the slogan "pure language" since you can tell from its type whether a function performs any effects.) IO in Haskell is exactly an effect type like 'console' in Koka. It is monadic in Haskell, like in Koka. In Haskell it's slightly more awkward because let bindings and function application are pure so you are forced to use monad combinators (or do notation) to combine them, but this is just a syntactic difference not one of any substance[1]. Koka has better support for combining effects through essentially the "universal monad"[2] you mentioned in your talk. In the implementation of Haskell[3] a function of type 'a -> IO b' is exactly the same as a function of type 'a -> b'[4]. It isn't a function "which returns an 'IO b' which is an instruction to an impure runtime to run some effectful code". It isn't "a 'b' in a context". It isn't "a 'b' with some other stuff". Haskell does not "trigger effects in the runtime by returning monadic values". Haskell has effects! I'll reiterate because this is important. A function of type 'a -> IO b' is exactly a function 'a -> b'. It's just been tagged with an effect type called 'IO'. We combine these effect types with monadic combinators because the nature of effects in monadic, not for any other reason. Some other monads (Either, Maybe, State) are more like what you are thinking of. But they're different monads! They don't somehow subsume the entire nature of monads. Monads, like effect types, can simply be used for tracking effects. Monads will always be part of effect systems. [1] I am very happy to consider syntactic improvements that make effects more easy to work [2] I disagree that the "universal monad" is not typeable in Haskell. At least some version of a "universal monad" is typeable. It may look a bit awkward though. [3] At least in GHC. Other implementations are free to do what they want. [4] Actually slightly augmented with a trick to stop the optimizer breaking, but that's not of substance.