3 ms·

Yeah, that's my point. Contrary to the claim in the post I'm replying to, it seems clear that having the ability to do unsafe impure things in a language doesn'

Yeah, that's my point. Contrary to the claim in the post I'm replying to, it seems clear that having the ability to do unsafe impure things in a language doesn't mean users of that language "loose all ability to reason reliably". To the extent that the libraries and the ecosystem doen't make inappropriate use of unsafe behavior, you can have your impurity and reliable referential transparency too.

Quekid5 7y ago
I definitely agree that "lose all ability[...]" is probably a tad too strong :). > To the extent that the libraries and the ecosystem doen't make inappropriate use of unsafe behavior, you can have your impurity and reliable referential transparency too. The key qualitative difference between Haskell and e.g. O'Caml/Scala/whatever here is that it's quite trivial to verify that your program doesn't use side effects inappropriately (aka. is not referentially transparent): Just make sure it contains no unsafeFoo calls. There's no such mechanism in O'Caml/Scala, etc. (I'm not sure, but I imagine it might even be undecidable unless you restrict to a teeny tiny subset of the language, e.g. just the pure arithmetic expression language.) The qualitative difference in how confident you can be that moving a bit of code around won't change the semantics of your program is profound (or: bonkers) -- and before I'd experienced it myself I could have (rightly!) been extremely skeptical of such claims, yet here I am making that claim. Yes, unless you really want to fully vet all of your transitive dependencies you will have quite a large TCB, but I find that it's actually really rare for libraries to use unsafeFoo willy-nilly. Some of the low-level stuff like Text, Vector, etc. do, but AFAICT it's mostly for performance reasons... and DGMW quite serious bugs have been found in these. However, because these are isolated data structures these bugs get fixed once and they are immediately fixed for all users. Another wart wrt. a large TCB in Haskell is IO. Unfortunately, it has a very large surface area, but there's no really much that can be done about that at this point. Even still, as a programmer you can choose to use e.g. polysemy/fused-effects/etc. to define the semantics of effectful code in a much more fine-grained way such that the only point of contact between your code and IO is in a tiny "interpretation of semantics" layer.

Quekid5 7y ago

I definitely agree that "lose all ability[...]" is probably a tad too strong :). > To the extent that the libraries and the ecosystem doen't make inappropriate use of unsafe behavior, you can have your impurity and reliable referential transparency too. The key qualitative difference between Haskell and e.g. O'Caml/Scala/whatever here is that it's quite trivial to verify that your program doesn't use side effects inappropriately (aka. is not referentially transparent): Just make sure it contains no unsafeFoo calls. There's no such mechanism in O'Caml/Scala, etc. (I'm not sure, but I imagine it might even be undecidable unless you restrict to a teeny tiny subset of the language, e.g. just the pure arithmetic expression language.) The qualitative difference in how confident you can be that moving a bit of code around won't change the semantics of your program is profound (or: bonkers) -- and before I'd experienced it myself I could have (rightly!) been extremely skeptical of such claims, yet here I am making that claim. Yes, unless you really want to fully vet all of your transitive dependencies you will have quite a large TCB, but I find that it's actually really rare for libraries to use unsafeFoo willy-nilly. Some of the low-level stuff like Text, Vector, etc. do, but AFAICT it's mostly for performance reasons... and DGMW quite serious bugs have been found in these. However, because these are isolated data structures these bugs get fixed once and they are immediately fixed for all users. Another wart wrt. a large TCB in Haskell is IO. Unfortunately, it has a very large surface area, but there's no really much that can be done about that at this point. Even still, as a programmer you can choose to use e.g. polysemy/fused-effects/etc. to define the semantics of effectful code in a much more fine-grained way such that the only point of contact between your code and IO is in a tiny "interpretation of semantics" layer.