4 ms·

Unsafe Haskell (2015)

54 points by Cieplak 8y ago

jejones3141 8y ago
Is there a point to this other than calling unsafe functions is unsafe?
- JadeNB 8y ago
  Presumably, answering the question "Why does Haskell have all these (seemingly) unnecessary restrictions on things that I can do when doing them (seemingly) won't cause problems?"
habitue 8y ago
This is the reason Safe Haskell exists https://downloads.haskell.org/~ghc/7.8.4/docs/html/users_guide/safe-haskell.html https://downloads.haskell.org/~ghc/7.8.4/docs/html/users_gui...
- dmead 8y ago
  Also lambdabot.
justinjlynn 8y ago
So, essentially the Haskell compiler allows you to say "don't worry I've got this, it'll be fine -- it's pure and semantically correct, I promise!" because the developers of the compiler know that they can't think of everything and want you to be able to do some really nasty hacks if you have to do so. It's easy to check up that the authors of the libraries you're using aren't using these escape hatches. Of course, if they or you are using these escape hatches, and it's not correct -- and it blows up -- you've only yourself to blame for subverting the compiler.
- Drup 8y ago
  Most strongly typed languages have such escape hatches ("Unsafe" in haskell, "Obj" in OCaml, "trustme" in Idris,....) . It's something you always need at some point when the typing is not sufficient to properly account for what you are doing. For instance, Coq code can be extracted to OCaml code. OCaml type system is less powerful than Coq's, so Coq needs to cheat, and the emitted code is full of "unsafe" features. But the program was typechecked with Coq's type system, and is thus perfectly safe. Of course, the goal of the language designer is to minimize its usage. That's something the Rust people understood very well, and the unsafe blocks are an extremely good solution to this problem.
  - pdpi 8y ago
    > It's something you always need at some point when the typing is not sufficient to properly account for what you are doing. E.g. FFI becomes horrendously impractical without something of this kind.
    - nickpsecurity 8y ago
      There's even work to address that with linking types: https://dbp.io/pubs/2017/linking-types-snapl.pdf https://dbp.io/pubs/2017/linking-types-snapl.pdf If the component is externally type-checked, the integration can be type checked against the language including it. They're also working on verifying compilers that do that: https://dbp.io/essays/2018-04-19-how-to-prove-a-compiler-fully-abstract.html https://dbp.io/essays/2018-04-19-how-to-prove-a-compiler-ful... Previously, others made the assembly languages themselves type-safe. Example: https://www.cs.cornell.edu/talc/papers/talx86-wcsss.pdf https://www.cs.cornell.edu/talc/papers/talx86-wcsss.pdf We might eventually be able to drop a caveat or three when talking about where type/memory safety ends. Cool stuff, eh?
- dontchooseanick 8y ago
  And most of the time it DOES warn you, google "haskell" + "If you enjoy sharing an address space with a malevolent agent of chaos" to find why unsafeCoerce and unsafePerformIO are only for FFI writers who know-what-they-do
  - gizmo686 8y ago
    In fairness, that comment refers to using the function accursedUnutterablePerformIO The comment for accursedUnutterablePerformIO: This "function" has a superficial similarity to 'unsafePerformIO' but it is in fact a malevolent agent of chaos. It unpicks the seams of reality (and the 'IO' monad) so that the normal rules no longer apply. It lulls you into thinking it is reasonable, but when you are not looking it stabs you in the back and aliases all of your mutable buffers. The carcass of many a seasoned Haskell programmer lie strewn at its feet. Witness the trail of destruction: https://github.com/haskell/bytestring/commit/71c4b438c675aa360c79d79acc9a491e7bbc26e7 https://github.com/haskell/bytestring/commit/71c4b438c675aa3... https://github.com/haskell/bytestring/commit/210c656390ae617d9ee3b8bcff5c88dd17cef8da https://github.com/haskell/bytestring/commit/210c656390ae617... https://ghc.haskell.org/trac/ghc/ticket/3486 https://ghc.haskell.org/trac/ghc/ticket/3486 https://ghc.haskell.org/trac/ghc/ticket/3487 https://ghc.haskell.org/trac/ghc/ticket/3487 https://ghc.haskell.org/trac/ghc/ticket/7270 https://ghc.haskell.org/trac/ghc/ticket/7270 Do not talk about "safe"! You do not know what is safe! Yield not to its blasphemous call! Flee traveller! Flee or you will be corrupted and devoured! https://hackage.haskell.org/package/bytestring-0.10.8.1/docs/src/Data-ByteString-Internal.html#accursedUnutterablePerformIO https://hackage.haskell.org/package/bytestring-0.10.8.1/docs... EDIT: For anyone confused, accursedUnutterablePerformIO is the new name for inlinePerformIO
saintPirelli 8y ago
Haskell is my guilty pleasure language. I have no idea what I personally would ever use it for, but I admire it so much that learning it is higher up on my bucket list than many other (arguably more useful) things.
- nine_k 8y ago
  Learning Haskell definitely affected the way I write and read code in other languages.
FrozenVoid 8y ago
Author calls the unsafe version x7 slower, yet such imperative, impure code wins Haskell benchmarks Perhaps he didn't optimize it well? https://benchmarksgame-team.pages.debian.net/benchmarksgame/faster/haskell.html https://benchmarksgame-team.pages.debian.net/benchmarksgame/...

54 points by Cieplak 8y ago

jejones3141 8y ago

Is there a point to this other than calling unsafe functions is unsafe?

JadeNB 8y ago
Presumably, answering the question "Why does Haskell have all these (seemingly) unnecessary restrictions on things that I can do when doing them (seemingly) won't cause problems?"

habitue 8y ago

This is the reason Safe Haskell exists https://downloads.haskell.org/~ghc/7.8.4/docs/html/users_guide/safe-haskell.html https://downloads.haskell.org/~ghc/7.8.4/docs/html/users_gui...

dmead 8y ago
Also lambdabot.

justinjlynn 8y ago

So, essentially the Haskell compiler allows you to say "don't worry I've got this, it'll be fine -- it's pure and semantically correct, I promise!" because the developers of the compiler know that they can't think of everything and want you to be able to do some really nasty hacks if you have to do so. It's easy to check up that the authors of the libraries you're using aren't using these escape hatches. Of course, if they or you are using these escape hatches, and it's not correct -- and it blows up -- you've only yourself to blame for subverting the compiler.

Drup 8y ago
Most strongly typed languages have such escape hatches ("Unsafe" in haskell, "Obj" in OCaml, "trustme" in Idris,....) . It's something you always need at some point when the typing is not sufficient to properly account for what you are doing. For instance, Coq code can be extracted to OCaml code. OCaml type system is less powerful than Coq's, so Coq needs to cheat, and the emitted code is full of "unsafe" features. But the program was typechecked with Coq's type system, and is thus perfectly safe. Of course, the goal of the language designer is to minimize its usage. That's something the Rust people understood very well, and the unsafe blocks are an extremely good solution to this problem.
- pdpi 8y ago
  > It's something you always need at some point when the typing is not sufficient to properly account for what you are doing. E.g. FFI becomes horrendously impractical without something of this kind.
  - nickpsecurity 8y ago
    There's even work to address that with linking types: https://dbp.io/pubs/2017/linking-types-snapl.pdf https://dbp.io/pubs/2017/linking-types-snapl.pdf If the component is externally type-checked, the integration can be type checked against the language including it. They're also working on verifying compilers that do that: https://dbp.io/essays/2018-04-19-how-to-prove-a-compiler-fully-abstract.html https://dbp.io/essays/2018-04-19-how-to-prove-a-compiler-ful... Previously, others made the assembly languages themselves type-safe. Example: https://www.cs.cornell.edu/talc/papers/talx86-wcsss.pdf https://www.cs.cornell.edu/talc/papers/talx86-wcsss.pdf We might eventually be able to drop a caveat or three when talking about where type/memory safety ends. Cool stuff, eh?
dontchooseanick 8y ago
And most of the time it DOES warn you, google "haskell" + "If you enjoy sharing an address space with a malevolent agent of chaos" to find why unsafeCoerce and unsafePerformIO are only for FFI writers who know-what-they-do
- gizmo686 8y ago
  In fairness, that comment refers to using the function accursedUnutterablePerformIO The comment for accursedUnutterablePerformIO: This "function" has a superficial similarity to 'unsafePerformIO' but it is in fact a malevolent agent of chaos. It unpicks the seams of reality (and the 'IO' monad) so that the normal rules no longer apply. It lulls you into thinking it is reasonable, but when you are not looking it stabs you in the back and aliases all of your mutable buffers. The carcass of many a seasoned Haskell programmer lie strewn at its feet. Witness the trail of destruction: https://github.com/haskell/bytestring/commit/71c4b438c675aa360c79d79acc9a491e7bbc26e7 https://github.com/haskell/bytestring/commit/71c4b438c675aa3... https://github.com/haskell/bytestring/commit/210c656390ae617d9ee3b8bcff5c88dd17cef8da https://github.com/haskell/bytestring/commit/210c656390ae617... https://ghc.haskell.org/trac/ghc/ticket/3486 https://ghc.haskell.org/trac/ghc/ticket/3486 https://ghc.haskell.org/trac/ghc/ticket/3487 https://ghc.haskell.org/trac/ghc/ticket/3487 https://ghc.haskell.org/trac/ghc/ticket/7270 https://ghc.haskell.org/trac/ghc/ticket/7270 Do not talk about "safe"! You do not know what is safe! Yield not to its blasphemous call! Flee traveller! Flee or you will be corrupted and devoured! https://hackage.haskell.org/package/bytestring-0.10.8.1/docs/src/Data-ByteString-Internal.html#accursedUnutterablePerformIO https://hackage.haskell.org/package/bytestring-0.10.8.1/docs... EDIT: For anyone confused, accursedUnutterablePerformIO is the new name for inlinePerformIO

saintPirelli 8y ago

Haskell is my guilty pleasure language. I have no idea what I personally would ever use it for, but I admire it so much that learning it is higher up on my bucket list than many other (arguably more useful) things.

nine_k 8y ago
Learning Haskell definitely affected the way I write and read code in other languages.

FrozenVoid 8y ago

Author calls the unsafe version x7 slower, yet such imperative, impure code wins Haskell benchmarks Perhaps he didn't optimize it well? https://benchmarksgame-team.pages.debian.net/benchmarksgame/faster/haskell.html https://benchmarksgame-team.pages.debian.net/benchmarksgame/...