3 ms·
Thanks. This is very interesting, but different from what I used to believe about Haskell (as you can imagine, I'm not an active Haskell programmer). I will hav
by mafribe 11y ago
Thanks. This is very interesting, but different from what I used to believe about Haskell (as you can imagine, I'm not an active Haskell programmer). I will have to revisit my ideas.
I still wonder how this would work with scope extrusion of references. Consider this little Ocaml program
let ( impure, pure ) =
let i = ref 0 in
let impure x = ( i := !i + 1; x + !i ) in
let pure x = (
i := !i + 1;
let res = !i + x in
i := !i - 1;
res - !i ) in
( impure, pure );;
which returns two functions called "pure" and "impure". Both are of type int -> int. The function "pure" is computing the successor function (let's ignore corner cases), but using hidden state. The function "impure" is using the same hidden state, but is clearly impure.
Is it possible to do the same in Haskell? By "the same" I mean giving "pure" the type int -> int, despite using hidden state that is used elsewhere?
- dllthomas 11y agoIt's harder to be confident about impossibility than about possibility, but I think this would require "cheating". I'm not sure if you meant it as a bug, but note that outside of a single-threaded context "pure" isn't referentially transparent - there seems to be a race condition that could lead to pure computing different values if impure is called during pure's execution. Something with a similar form that would be more realistic to ask for would be a cache for a pure-but-expensive function and some IO operations to inspect/manipulate that cache. I believe you would need a call to unsafePerformIO, but that could be a reasonable thing to do.
- mafribe 11y agoThanks. I know that "pure" is not thread-safe. I'm quite happy to consider the expressivity of Haskell's monadic approach to effects in a sequential setting first -- much easier to reason about. I wonder if anybody has investigated this expressivity problem. If not, there's an interesting problem waiting to be tackled.
- dllthomas 11y agoI don't see the problem. Pure code being automatically thread-safe is a boon. I would much rather be unable to write thread-unsafe code without noticing (and able to when I deliberately decide to).
- mafribe 11y agoMy interest is in proving expressivity results. Such proofs are much easier in a sequential setting. Indeed, at this point I don't even have a strong intuition what exactly the expressivity limitations of Haskell's monadic effect control are.