5 ms·

so you are telling me if getChar::Char haskell wouldn't return the same char all the time? Or are you telling me it needs a rather elaborate type signature(Wor

by xfer 8y ago

so you are telling me if getChar::Char haskell wouldn't return the same char all the time? Or are you telling me it needs a rather elaborate type signature(World -> (Char, World)), which is entirely the point the author is making here why haskell as being a lazy language needed monads but not ML.

edflsafoiewq 8y ago
In a pure language, whether lazy or not, x: T always "returns" the same value x. getChar: IO Char always "returns" the same element of IO Char. The sense in which getChar returns a Char belongs to the semantics of the "inner" language associated to the IO constructor and the properties of the "outer" language, like whether it is lazy or "has monads" or even is itself impure like ML, have little bearing on it. Again, monads are just an abstraction. A language does not need monads to do IO because it is pure or lazy. And a language does not not need monads because it is already impure.
- xfer 8y ago
  My point is that lazy semantics memoizes evaluation, so you need an elaborate signature to make sure that it can't(which is how the IO type looks like). The "inner" type of IO is very much relevant to the semantics of the "outer" language.
  - edflsafoiewq 8y ago
    The evaluation semantics of a language are not something you can change by giving some king of elaborate signature. Anyway, we don't need some elaborate type, a minimal IO can defined freely from the combinators getChar: IO Char putChar: Char -> IO () pure: forall a . a -> IO a ap: forall a b . IO a -> (a -> IO b) -> IO b which makes a value of IO a just a common tree. The semantics of the inner language (written [[x]]) can be given in terms of the semantics of the outer language (written [x]) by [[p: IO a]] is a program that produces an [a] (or diverges) [[getChar]] := program that reads a character, c, from the input and produces c: [Char] [[putChar c]] := program that: 1. "runs" (see below) [c]: [Char] producing a character 2. prints that character to the output 3. produces [()]: [()] [[pure (x: a)]] := program that produces [x]: [a] [[ap (x: IO a) (f: a -> IO b)]] := program that: 1. runs [[x]], producing y: [a] 2. then computes p = [f] y: [IO b] 3. then runs the program [[p]], whose result is the final result The semantics of the "inner" language do not have any effect on the semantics of the "outer" language. The semantics of the inner are strictly layered on top of the semantics of the outer. But what I said was that the semantics of the inner language do not depend on the properties of the outer language such as purity, evaluation order, etc., which is certainly so. The only things that the inner semantics really require of the outer is that * we can apply f: [a->b] to x: [a] to get f x: [b] * there is a way to regard a character c as a member of [c] * there is a way to "run" an element of [Char] and get a character, in some sense appropriate to the outer language. For normal pure functional languages [Char] will just be the set of characters plus possibly some additional data to model non-termination so this is easy, but it works even if the language is impure (in this case, the effect of running [c] would precede the effect of printing), if it is non-deterministic (in this case, the output stream bifurcates whenever you print a character), etc. There is no place in which whether the outer language "has monads" enters in. (Unlike the above list of requirements, where the notion of a monad has certainly entered in :-) But that is what Moggi used them for after all.)
    - xfer 8y ago
      It seems that you have built the IO type and it's monadic properties into the language? I am talking about the concrete type of IO has and how using it, without the monads as abstraction would be so cumbersome that haskell "needed" monads. You can't change the semantics but you can emulate the desired semantics, which is what i argue IO type does.
      - lmm 8y ago
        > I am talking about the concrete type of IO has and how using it, without the monads as abstraction would be so cumbersome that haskell "needed" monads. It would be comparable to working with e.g. Lwt in OCaml, which is very much a practical way of programming.
- atombender 8y ago
  I don't think this is accurate. Haskell "cheats" by making IO special and magical [1]. GHC has this definition: newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #)) The Haskell standard, last I heard, specifies the implementation of IO as being compiler-specific. I may be wrong, but I believe you can't reimplement IO yourself in pure Haskell, at least not the way GHC needs it to be defined. As the article points out, this has little to do with monads. You can force ordering using unique types [2] (e.g. used in Clean) by having I/O functions take a file handle and return a new file handle in every call. But IO fits nicely into the monadic pattern. [1] http://blog.ezyang.com/2011/05/unraveling-the-mystery-of-the-io-monad/ http://blog.ezyang.com/2011/05/unraveling-the-mystery-of-the... [2] https://en.wikipedia.org/wiki/Uniqueness_type https://en.wikipedia.org/wiki/Uniqueness_type
  - edflsafoiewq 8y ago
    I'm not really talking about Haskell. Certainly not GHC.
tikhonj 8y ago
No, it's more that getChar :: IO Char does not need to know anything about "monads"—it only depends on having some IO type for "IO actions" or "IO procedures" or whatever you want to call them. Combine the concrete IO type with a few built-in library functions for building larger IO actions out of smaller ones and you have a perfectly good (albeit unextensible) effect system without every saying the word "monad". Interestingly, the programming experience with this is going to be pretty much the same as using a language with promises. It would be like working in JavaScript with no blocking IO, but with some abstraction and syntax sugar to make it less powerful. Or, more pointedly, it would be like working in OCaml. OCaml might not "need" monads, but all serious OCaml is full of monads anyway, at least depending on LWT or Asyc for concurrency.
- xfer 8y ago
  > Combine the concrete IO type Why does it need that concrete type (taking one world and producing another)? Why can't i just have it's concrete type be Char? (obviously you would implement with some unsafe inside). But does referential transparency still hold?
  - JadeNB 8y ago
    Well, as you said in your earlier post, referential transparency can’t hold unless you only ever want to `get` one `Char`; that’s the definition.
  - tikhonj 8y ago
    Haskell doesn't "need" an IO type—it wants one. The IO type gives us a language-level way to separate code that has side-effects from code that doesn't. It's a powerful tool to help manage complexity in our programs. One of the advantages of keeping IO in an explicit IO type is that code that isn't in IO becomes easier to refactor. This is what people mean by referential transparency: since I know that a `Char` cannot implicitly depend on the state of the rest of the program, I am always free to move it around, put it in a variable or replace it with an equivalent expression without changing the meaning of the program. You would not get this with getChar :: Char because two getChars could give you different results, so moving them around or reordering them would change the semantics of your program.
squiggleblaz 8y ago
But the point is the language doesn't need monads. You could express the same solution to the problem more verbosely without monads if the language couldn't express monads. Consequently, monads are beside the point. Haskell needs to constrain the order of evaluation when it's dealing with the real world. There's a solution to that problem (require and yield `World`). Then we choose to use `IO` (i.e. a monad) to implement that solution. But the abstraction that is a monad is independently justified and worthwhile in languages like Typescript (I wish!) and ML which don't have the same IO issue. As long as we teach monads as if they have anything to do with IO we're confusing people. IO uses monads because it's convenient and apt. But monads don't control order of evaluation. They've got nothing to do with order of evaluation.
- xfer 8y ago
  > Then we choose to use `IO` (i.e. a monad) to implement that solution. Yes, we are in agreement, however i am arguing that haskell had to use monads here otherwise it would be very difficult to use. > As long as we teach monads as if they have anything to do with IO we're confusing people. Sure, but the introduction of monads in haskell came out of a real necessity is my point. Category theory is powerful tool for abstraction and useful in any language. > But monads don't control order of evaluation. They've got nothing to do with order of evaluation. Right, but they can hide the trick and make it all seem transparent, which imho is very important point to keep in mind.
- thesz 8y ago
  Haskell does not constrain the order of evaluation when dealing with real world. It constrains order of effects. The code "putStrLn this >> putStrLn that" is allowed to evaluate this and that in any order, basically. "that" may depend on "this" and vice versa. The very expressions "putStrLn a" is also not an action, but expression, being evaluated into actions. And the constrainment of effects is what makes Haskell special.
thesz 8y ago
World -> (World, Char) is one possible type for getChar. There was an approach called Fudgets [1], based on stream processing, and in this case the signature would be getChar :: SP Response Char. Stream processing type used in Fudgets also admits monadic interface implementation. [1] https://research.chalmers.se/en/publication/1015 https://research.chalmers.se/en/publication/1015

by xfer 8y ago

edflsafoiewq 8y ago

In a pure language, whether lazy or not, x: T always "returns" the same value x. getChar: IO Char always "returns" the same element of IO Char. The sense in which getChar returns a Char belongs to the semantics of the "inner" language associated to the IO constructor and the properties of the "outer" language, like whether it is lazy or "has monads" or even is itself impure like ML, have little bearing on it. Again, monads are just an abstraction. A language does not need monads to do IO because it is pure or lazy. And a language does not not need monads because it is already impure.

xfer 8y ago
My point is that lazy semantics memoizes evaluation, so you need an elaborate signature to make sure that it can't(which is how the IO type looks like). The "inner" type of IO is very much relevant to the semantics of the "outer" language.
- edflsafoiewq 8y ago
  The evaluation semantics of a language are not something you can change by giving some king of elaborate signature. Anyway, we don't need some elaborate type, a minimal IO can defined freely from the combinators getChar: IO Char putChar: Char -> IO () pure: forall a . a -> IO a ap: forall a b . IO a -> (a -> IO b) -> IO b which makes a value of IO a just a common tree. The semantics of the inner language (written [[x]]) can be given in terms of the semantics of the outer language (written [x]) by [[p: IO a]] is a program that produces an [a] (or diverges) [[getChar]] := program that reads a character, c, from the input and produces c: [Char] [[putChar c]] := program that: 1. "runs" (see below) [c]: [Char] producing a character 2. prints that character to the output 3. produces [()]: [()] [[pure (x: a)]] := program that produces [x]: [a] [[ap (x: IO a) (f: a -> IO b)]] := program that: 1. runs [[x]], producing y: [a] 2. then computes p = [f] y: [IO b] 3. then runs the program [[p]], whose result is the final result The semantics of the "inner" language do not have any effect on the semantics of the "outer" language. The semantics of the inner are strictly layered on top of the semantics of the outer. But what I said was that the semantics of the inner language do not depend on the properties of the outer language such as purity, evaluation order, etc., which is certainly so. The only things that the inner semantics really require of the outer is that * we can apply f: [a->b] to x: [a] to get f x: [b] * there is a way to regard a character c as a member of [c] * there is a way to "run" an element of [Char] and get a character, in some sense appropriate to the outer language. For normal pure functional languages [Char] will just be the set of characters plus possibly some additional data to model non-termination so this is easy, but it works even if the language is impure (in this case, the effect of running [c] would precede the effect of printing), if it is non-deterministic (in this case, the output stream bifurcates whenever you print a character), etc. There is no place in which whether the outer language "has monads" enters in. (Unlike the above list of requirements, where the notion of a monad has certainly entered in :-) But that is what Moggi used them for after all.)
  - xfer 8y ago
    It seems that you have built the IO type and it's monadic properties into the language? I am talking about the concrete type of IO has and how using it, without the monads as abstraction would be so cumbersome that haskell "needed" monads. You can't change the semantics but you can emulate the desired semantics, which is what i argue IO type does.
    - lmm 8y ago
      > I am talking about the concrete type of IO has and how using it, without the monads as abstraction would be so cumbersome that haskell "needed" monads. It would be comparable to working with e.g. Lwt in OCaml, which is very much a practical way of programming.
atombender 8y ago
I don't think this is accurate. Haskell "cheats" by making IO special and magical [1]. GHC has this definition: newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #)) The Haskell standard, last I heard, specifies the implementation of IO as being compiler-specific. I may be wrong, but I believe you can't reimplement IO yourself in pure Haskell, at least not the way GHC needs it to be defined. As the article points out, this has little to do with monads. You can force ordering using unique types [2] (e.g. used in Clean) by having I/O functions take a file handle and return a new file handle in every call. But IO fits nicely into the monadic pattern. [1] http://blog.ezyang.com/2011/05/unraveling-the-mystery-of-the-io-monad/ http://blog.ezyang.com/2011/05/unraveling-the-mystery-of-the... [2] https://en.wikipedia.org/wiki/Uniqueness_type https://en.wikipedia.org/wiki/Uniqueness_type
- edflsafoiewq 8y ago
  I'm not really talking about Haskell. Certainly not GHC.

tikhonj 8y ago

No, it's more that getChar :: IO Char does not need to know anything about "monads"—it only depends on having some IO type for "IO actions" or "IO procedures" or whatever you want to call them. Combine the concrete IO type with a few built-in library functions for building larger IO actions out of smaller ones and you have a perfectly good (albeit unextensible) effect system without every saying the word "monad". Interestingly, the programming experience with this is going to be pretty much the same as using a language with promises. It would be like working in JavaScript with no blocking IO, but with some abstraction and syntax sugar to make it less powerful. Or, more pointedly, it would be like working in OCaml. OCaml might not "need" monads, but all serious OCaml is full of monads anyway, at least depending on LWT or Asyc for concurrency.

xfer 8y ago
> Combine the concrete IO type Why does it need that concrete type (taking one world and producing another)? Why can't i just have it's concrete type be Char? (obviously you would implement with some unsafe inside). But does referential transparency still hold?
- JadeNB 8y ago
  Well, as you said in your earlier post, referential transparency can’t hold unless you only ever want to `get` one `Char`; that’s the definition.
- tikhonj 8y ago
  Haskell doesn't "need" an IO type—it wants one. The IO type gives us a language-level way to separate code that has side-effects from code that doesn't. It's a powerful tool to help manage complexity in our programs. One of the advantages of keeping IO in an explicit IO type is that code that isn't in IO becomes easier to refactor. This is what people mean by referential transparency: since I know that a `Char` cannot implicitly depend on the state of the rest of the program, I am always free to move it around, put it in a variable or replace it with an equivalent expression without changing the meaning of the program. You would not get this with getChar :: Char because two getChars could give you different results, so moving them around or reordering them would change the semantics of your program.

squiggleblaz 8y ago

But the point is the language doesn't need monads. You could express the same solution to the problem more verbosely without monads if the language couldn't express monads. Consequently, monads are beside the point. Haskell needs to constrain the order of evaluation when it's dealing with the real world. There's a solution to that problem (require and yield `World`). Then we choose to use `IO` (i.e. a monad) to implement that solution. But the abstraction that is a monad is independently justified and worthwhile in languages like Typescript (I wish!) and ML which don't have the same IO issue. As long as we teach monads as if they have anything to do with IO we're confusing people. IO uses monads because it's convenient and apt. But monads don't control order of evaluation. They've got nothing to do with order of evaluation.

xfer 8y ago
> Then we choose to use `IO` (i.e. a monad) to implement that solution. Yes, we are in agreement, however i am arguing that haskell had to use monads here otherwise it would be very difficult to use. > As long as we teach monads as if they have anything to do with IO we're confusing people. Sure, but the introduction of monads in haskell came out of a real necessity is my point. Category theory is powerful tool for abstraction and useful in any language. > But monads don't control order of evaluation. They've got nothing to do with order of evaluation. Right, but they can hide the trick and make it all seem transparent, which imho is very important point to keep in mind.
thesz 8y ago
Haskell does not constrain the order of evaluation when dealing with real world. It constrains order of effects. The code "putStrLn this >> putStrLn that" is allowed to evaluate this and that in any order, basically. "that" may depend on "this" and vice versa. The very expressions "putStrLn a" is also not an action, but expression, being evaluated into actions. And the constrainment of effects is what makes Haskell special.

thesz 8y ago

World -> (World, Char) is one possible type for getChar. There was an approach called Fudgets [1], based on stream processing, and in this case the signature would be getChar :: SP Response Char. Stream processing type used in Fudgets also admits monadic interface implementation. [1] https://research.chalmers.se/en/publication/1015 https://research.chalmers.se/en/publication/1015