Unsafe Haskell (2015) | Hacker News Reader

Unsafe Haskell (2015)

seas.upenn.edu

54 pointsCieplak13 comments

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.

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.

> 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.

There's even work to address that with linking types:

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-ful...

Previously, others made the assembly languages themselves type-safe. Example:

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?

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

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/71c4b438c675aa3...

https://github.com/haskell/bytestring/commit/210c656390ae617...

https://ghc.haskell.org/trac/ghc/ticket/3486

https://ghc.haskell.org/trac/ghc/ticket/3487

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...

EDIT: For anyone confused, accursedUnutterablePerformIO is the new name for inlinePerformIO

This is the reason Safe Haskell exists

https://downloads.haskell.org/~ghc/7.8.4/docs/html/users_gui...

Also lambdabot.

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/...

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.

Learning Haskell definitely affected the way I write and read code in other languages.

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

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?"

Reply on news.ycombinator.com