4 ms·

unsafePerformIO invalidates any guarantees in Haskell :(

by tumdum_ 11y ago

dllthomas 11y ago
Less than you might think, in practice. I see unsafePerformIO used three places. First, debugging. While there are sometimes better approaches, this is unobjectionable. Second, I'll sometimes use it in throw-away scripts. Here I am knowingly losing some guarantees, but in a sufficiently constrained portion of the system that it's rarely a problem. Third, where it's known to be safe and necessary. This one is the most worrisome, but the community is pretty at expecting uses to 1) be very rare, and 2) have both safety and necessity justified. Really, the fact that all values are inhabited by bottom is a bigger issue. Still, IME, Haskell provides guarantees that are sufficiently reliable to be tremendously useful.
- 15155 11y ago
  > where it's known to be safe and necessary To give a valid, non-objectionable example: FFI that is known to be pure will often be wrapped with unsafePerformIO to present a clean interface to Haskell code.
  - chadaustin 11y ago
    Indeed. Consider https://github.com/chadaustin/buffer-builder/blob/master/src/Data/BufferBuilder.hs#L164 https://github.com/chadaustin/buffer-builder/blob/master/src... The API is pure, but it's implemented with a high-performance effectful monad, and none of the implementation details are exported. A perfect use of unsafe[Dupable]PerformIO.
- tumdum_ 11y ago
  I think you misunderstood me. I'm not saying it is common to use unsafe functions in Haskell for 'bad things'. All I'm saying is that due to existence unsafe functions it is possible to lie about your real side effects and memory safety. Which considering that op article was about guarantees seems to be critical issue. If I give you only the signature of function, You can't be sure what exactly it's doing, just like in C - http://lpaste.net/5209148331879563264 http://lpaste.net/5209148331879563264
kpmah 11y ago
I deliberately ignore that :) I don't think escape hatches added as a practical concern should count against the language, as long as they're used appropriately by the community. You can defeat Rust's guarantees by using an `unsafe` block, and you can defeat Python's memory safety by adding a C extension. Like I say at the start, if I were going to be strict about this it would be a very short blog post!
nickpsecurity 11y ago
There's methods for handling that safely even down to assembler language or gates. Quite a few. FLINT was first I saw. There's also SPARK with integrity checks that assume hardware or something else might goof. Chlipala's Bedrock can emulate some of it. Microsoft came up with one, Vx86, for their VCC verification system that they applied to Hyper-V. They also did CoqASM and used TAL in VerveOS. So, all kinds of methods of getting some guarantees out of unsafe code that can be paired with safe HLL's like Haskell.

unsafePerformIO invalidates any guarantees in Haskell :(

by tumdum_ 11y ago

unsafePerformIO invalidates any guarantees in Haskell :(

Less than you might think, in practice. I see unsafePerformIO used three places. First, debugging. While there are sometimes better approaches, this is unobjectionable. Second, I'll sometimes use it in throw-away scripts. Here I am knowingly losing some guarantees, but in a sufficiently constrained portion of the system that it's rarely a problem. Third, where it's known to be safe and necessary. This one is the most worrisome, but the community is pretty at expecting uses to 1) be very rare, and 2) have both safety and necessity justified. Really, the fact that all values are inhabited by bottom is a bigger issue. Still, IME, Haskell provides guarantees that are sufficiently reliable to be tremendously useful.

15155 11y ago
> where it's known to be safe and necessary To give a valid, non-objectionable example: FFI that is known to be pure will often be wrapped with unsafePerformIO to present a clean interface to Haskell code.
- chadaustin 11y ago
  Indeed. Consider https://github.com/chadaustin/buffer-builder/blob/master/src/Data/BufferBuilder.hs#L164 https://github.com/chadaustin/buffer-builder/blob/master/src... The API is pure, but it's implemented with a high-performance effectful monad, and none of the implementation details are exported. A perfect use of unsafe[Dupable]PerformIO.
tumdum_ 11y ago
I think you misunderstood me. I'm not saying it is common to use unsafe functions in Haskell for 'bad things'. All I'm saying is that due to existence unsafe functions it is possible to lie about your real side effects and memory safety. Which considering that op article was about guarantees seems to be critical issue. If I give you only the signature of function, You can't be sure what exactly it's doing, just like in C - http://lpaste.net/5209148331879563264 http://lpaste.net/5209148331879563264

kpmah 11y ago

I deliberately ignore that :) I don't think escape hatches added as a practical concern should count against the language, as long as they're used appropriately by the community. You can defeat Rust's guarantees by using an `unsafe` block, and you can defeat Python's memory safety by adding a C extension. Like I say at the start, if I were going to be strict about this it would be a very short blog post!

nickpsecurity 11y ago

There's methods for handling that safely even down to assembler language or gates. Quite a few. FLINT was first I saw. There's also SPARK with integrity checks that assume hardware or something else might goof. Chlipala's Bedrock can emulate some of it. Microsoft came up with one, Vx86, for their VCC verification system that they applied to Hyper-V. They also did CoqASM and used TAL in VerveOS. So, all kinds of methods of getting some guarantees out of unsafe code that can be paired with safe HLL's like Haskell.