4 ms·

Purity is growing more and more day by day. What I meant was this: a language should not be pure by default, rather, it should be possible to say (and get chec

by mafribe 11y ago

Purity is growing more and more day by day. What I meant was this: a language should not be pure by default, rather, it should be possible to say (and get checked by the compiler): this is pure. Quite how to set up a pragmatically viable type and effect system to guarantee this is unclear. PS what is the "normal" definition of purity?

tel 11y ago
Hm, I think given your stance now I'm not sure whether I properly understood what you said elsewhere on this matter. "Purity" is a tricky technical concept that can be defined, but rather than do so explicitly I'd rather note that it necessarily requires the asserter to take a stance on what "observable" means. Haskell is clearly impure in that its laziness is implemented using mutation "behind the scenes", but it is also taken to have an "observable" semantics where such mutation is invisible and IO is merely an interesting value. This gives it purity [0] according to that degree of observability. I think I'm having difficulty parsing your interpretation of purity because you're moving smoothly between analytic and synthetic judgements of the notion. Agda, as an example, is a system which has a synthetic notion of purity as the "language" is thought to not contain terms which represent effects. Haskell plays a trick where it has, essentially, two sets of semantics. The first shares this property (modulo non-termination, see [0]) and is where most "programming" occurs---here we use monads as a system for constructing terms of the second semantics, IO. The second, IO, semantics are vastly impure. To the degree that this trick is "purity in a language" then purity is becoming a very popular idea. Haskell uses its type system to provide synthetic distinction between the two choices of semantics, but if you use a language lacking that discipline then you can merely call this "isolation of side effecting code" and then nobody will disagree with you. If you don't want to call this "purity", and maybe you don't, then I feel you're in the minority though you aren't without an island to stand on. Frankly, both are sort of an overloading of the term, though. [0] Actually, it gets a lot trickier. It's well known that non-termination is an effect and it's a little slippery to define Haskell's notion of "observability" so as to no longer observe non-termination. I mean "slippery" here to say that it takes some technical finesse and that it tends to go against people's intuition a bit more harshly than the rest.

by mafribe 11y ago

tel 11y ago

Hm, I think given your stance now I'm not sure whether I properly understood what you said elsewhere on this matter. "Purity" is a tricky technical concept that can be defined, but rather than do so explicitly I'd rather note that it necessarily requires the asserter to take a stance on what "observable" means. Haskell is clearly impure in that its laziness is implemented using mutation "behind the scenes", but it is also taken to have an "observable" semantics where such mutation is invisible and IO is merely an interesting value. This gives it purity [0] according to that degree of observability. I think I'm having difficulty parsing your interpretation of purity because you're moving smoothly between analytic and synthetic judgements of the notion. Agda, as an example, is a system which has a synthetic notion of purity as the "language" is thought to not contain terms which represent effects. Haskell plays a trick where it has, essentially, two sets of semantics. The first shares this property (modulo non-termination, see [0]) and is where most "programming" occurs---here we use monads as a system for constructing terms of the second semantics, IO. The second, IO, semantics are vastly impure. To the degree that this trick is "purity in a language" then purity is becoming a very popular idea. Haskell uses its type system to provide synthetic distinction between the two choices of semantics, but if you use a language lacking that discipline then you can merely call this "isolation of side effecting code" and then nobody will disagree with you. If you don't want to call this "purity", and maybe you don't, then I feel you're in the minority though you aren't without an island to stand on. Frankly, both are sort of an overloading of the term, though. [0] Actually, it gets a lot trickier. It's well known that non-termination is an effect and it's a little slippery to define Haskell's notion of "observability" so as to no longer observe non-termination. I mean "slippery" here to say that it takes some technical finesse and that it tends to go against people's intuition a bit more harshly than the rest.