3 ms·

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 "in

by 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.

by xfer 8y ago

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.