Deprecating Safe Haskell, or heavily investing in it?

#64

I have always wanted Haskell, and GHC in particular, to serve as a laboratory for trying out ideas, and seeing which ones flourish and which do not. Ideas always start with particular, passionate individuals, and Safe Haskell is no exception: the driving forces were David Terei and David Mazieres at Stanford.

Successful ideas outlive their creators; they attract others who maintain, refine, and develop them. GADTs is an example of a wildly successful idea; GADTs are now deeply embedded in GHC. Template Haskell is another – Tim Sheard was the original inspiration, but TH is no longer dependent on Tim, while lots and lots of libraries are dependent on TH.

Linear Haskell is at an earlier stage. It still has its original enthusiasts deeply engaged (Arnaud, Krzysztof, and others), and we have yet to see how broadly it is used. But I love that GHC can be a petri dish for an experiment like this.

Safe Haskell is arguably an idea that hasn’t taken root. It remains a pretty good idea. As the paper says “Haskell comes tantalisingly close to providing a means for confining malicious code”. But somehow Safe Haskell hasn’t caught fire, gained users, grown enthusiasts who love and develop it. So, without any implied criticism of David and David (and I was a co-author on the original paper too) I think it would be plausible to lay it to rest.

Incidentally, while thinking about the petri dish, Backpack is another experiment whose outcome is (to me) uncertain. Backpack is a “big feature”; it fills a really important hole in Haskell’s story, namely large scale modularity. And yet it hasn’t attracted either the enthusisats or the real-world usage that I was hoping for. I would love for someone, or a group, to take up the mantle of being the Backpack enthusiasts and maintainers.

16 Likes
#65

Thanks for bringing some clarity into this. Just a side comment…

I think we need to approach things much more from the end user POV.

Backpack is great, but it has always been a primarily technically based discussion for the advanced. Many people don’t even know what it’s really for.

We need to market and demonstrate use cases in a digestible way for regular users, so they will go “oh, that’s neat, I want it”. This will also allow us to reason about the proposed in terms of usability and how it fits into workflows, which I think has largely been neglected.

2 Likes
#66

At my work, we have strongly wanted Backpack on more than one occasion. Our resistance has always come down to ease-of-use and HLS integration.

The same worries for ease-of-use haunt us with linear types, which we have actually tried to use, but the cost of use was slightly too high (known bugs such as linearity inference at the time through let bindings and case statements).

I’m not sure if these concerns are totally real, but I’ve seen the bug reports on HLS, and it’s enough to make me feel uncomfortable to make my company to rely on Backpack.

#67

I figure many people who ever used OCaml modules and functors would like to have such functionality in Haskell. I do, for one. I actually played around with Backpack a while ago for a very suitable use-case, but ran into too many showstoppers (one of them being Stack not supporting it) to pursue further. See xinU, a Haskell Experiment » nicolast.be

2 Likes
#68

Incidentally, while thinking about the petri dish, Backpack is another experiment whose outcome is (to me) uncertain. Backpack is a “big feature”; it fills a really important hole in Haskell’s story, namely large scale modularity. And yet it hasn’t attracted either the enthusisats or the real-world usage that I was hoping for. I would love for someone, or a group, to take up the mantle of being the Backpack enthusiasts and maintainers.

Backpack is very important for the incremental compilation, the best version of splitting base, and making Hackage type safe — by which I mean version solving is sound and complete and we don’t need to spend O(2^n) compute resources verifying this. So I remain confident its time will come!

#69

Let’s discuss Backpack in a separate thread please.

6 Likes
#70

In my opinion, almost everyone does that, or should at least think of it that way, since it’s wrong to see trust as a binary of either full trust or no trust whatsoever. Every time I use a library from hackage, I’m running somewhat untrusted code. I’m fairly confident that it’s not malicious, but I have far from 100% confidence in that, at least unless I do a thorough inspection of the code, but not even then.

So for me, the most value Safe Haskell could give is to decrease the level of trust needed when using third party libraries, at least in the cases where those doesn’t need to have IO access, and thus decreasing the attack surface for supply chain attacks.

1 Like
#71

One of the big practical challenges, in my experience, is confining Trustworthy code to small modules that can be audited easily.

1 Like
#72

…and now that it’s been coughed regurgitated brought up yet again in the context of language editions:

Deprecating Safe Haskell

So what was the intended purpose of Safe Haskell?

So if it really is time for Safe Haskell and its ecosystem to be dismantled, such “loophole” language features (old and new) as well as their associated ecosystems should also be included in said dismantling to avoid regressing (in this case) all the way back to Haskell 2010:

Renovating Safe Haskell

Haskell is (meant to be) a declarative language. So a module written in ordinary, boring un-extended Haskell ought to be safe by default - there ought to be no need at all to explicitly label that module as being Safe. Instead, any module which uses unsafe language features should be be labelled “unsafe” in some way.

Since unsafe has already be reserved for a technical purpose in the FFI, and based on this post, a future Safe Haskell could use feign as an annotation for both unsafe modules:

module feign MotleyBits (...) where

and their imports:

import feign MotleyBits (...)

Note:

  • there should be no way to “override” the absence of either annotation if Safe Haskell is enabled - if users don’t want to see the resulting warnings (or errors if need be) they must add the annotations.

  • there should be no transitivity - if module A imports from module B, and B imports from an unsafe module C, then only B requires the annotated (feign) imports.

  • If there was some way to “deem” the likes of runIO and the various PerformIOs as being foreign to Haskell, reusing the existing reserved word foreign could be an alternative to introducing feign.

So instead of everyone else having to label their modules as “safe”, the few who use unsafe Haskell features in the sources for their modules would need to label those modules or their imports accordingly. This places the focus on unsafe modules and how to have less (or none) of them.

1 Like
#73

You have to define what you mean by “safe” and this definition must be meaningfully useful.

In my mind compiling a regex expression with libpcre2 and having it return a ForeignPtr Pcre2_code is a safe pure operation, provided I write the code correctly and don’t leave any escape hatches that make the whole thing crash and burn. The compiler will never be able to approve that because it can’t read the documentation for that library.

If your definition of safe is a hard “everything the compiler can approve and not an inch more”, then you will have to solve this topic’s #14, either banning recursion or implementing very complex algorithms that make definitions like let x = x in x impossible.

I would argue the question is the inverse: how much of the ecosystem actively relies on Safe Haskell? Based on the two replies to this comment the answer is very close to none. Moreover the only use real use case seems to be trust, which is something this extension can never solve.

#74

The intention is reuse Safe Haskell’s existing notions of safety (and one reason why the section that quote is from has the name Renovating Safe Haskell ).

Apparently enough to contemplate its replacement - if merely removed, the more pertinent question is:

…and no matter how many extensions are added to GHC’s type system, there will always be some other type it cannot infer or check. But I don’t see angry mobs of Haskellers clamouring for it to be dismantled just because types extensions can never solve that problem.

Typed programming is a “best effort” solution, and so would trusted programming. But for those who like “zero effort” solutions:

# mkdir ./Main
# cat /dev/urandom > ./Main/Main  # ...Ctrl-C!
# chmod u+x .Main/Main
# ./Main/Main

(…after backing up and isolating your system from the Internet ;-)

#75

It doesn’t matter, the ecosystem is already built on abominations like bytestring. There are no greener pastures to go back to and most probably no strong reason to dream of them for too long.

Safe Haskell is by no means the only questionably useful extension, but I imagine it’s quite a standalone one, so dismantling it wouldn’t be hard. Carrying around extensions isn’t free and GHC should be able to shed ones that do not work or are too difficult to maintain.

#76

Iff that is true…forget about Safe Haskell - that’s a reason to avoid all of Haskell and use another language!

…and did ye ol’ "grep it and see" style of safety-checking suddenly get a whole lot easier to use with ever-growing codebases? Because the “loopholes” upon which the abominations rely on means type signatures cannot be trusted at all:

But carrying around types isn’t free either so GHC should be able to shed it too, although that middle initial (“H”) may need to be “reassigned”…

#77

Safe Haskell is comparably bigger burden to maintain in GHC source code than other extensions. Mostly because, for example, a crazy type extension is just a concern of type checker and can be well encapsulated, while Safe Haskell spills out into interface files, implies a bunch of specific errors / warnings / knobs to adjust on package level.

1 Like
#78

As the author and person running the service since 2010, I can comment on TryHaskell’s sandboxing. It uses the hint package which is a thin layer over GHCi’s interpreter, and essentially implements layers of friction that make it hard (not impossible) to do something malicious. It only imports modules which are pure code, and extensions which are unexciting. The evaluator within Haskell uses a timeout, each evaluation of the REPL is a fresh process, which is aggressively nice’d in time and memory, and it runs on an underpowered machine which makes it run into resource limits even quicker. This all makes it quite slow. But also an uninteresting attack victim. It’s not in a VM, apart from the VM I’m renting, of course. It doesn’t let you define definitions anymore because that required state between runs and would make it easier to abuse and needed more parsing to implement a maximum declaration count. Apart from doing too much work I think Haskell is otherwise kind of easy to sandbox.

To run full programs I think CodeWorld made the right choice to compile the program and ship it to the browser and make it someone else’s problem. Redoing tryhaskell today, wasm would be the modern answer. You narrow the scope of your sand boxing problem to making the compile step safe (no naughty imports or FFI or CPP or TH tricks), and nice’d.

4 Likes
#79

…hmm, yes - I should have been more precise:

  • The appearance in interface files would still be needed to check that imports from unsafe modules are labelled accordingly;

  • As for packages…would the current complications be due (in large part) to the need to propagate “safeness” far and wide? If so, what I’m suggesting should remove all of that.

But one possible new difficulty would be a package directly exposing an unsafe module as part of its API - I would like to think that unsafe modules would only be “basement-level” infrastructure (i.e. only used internally, never to be exposed). But that could just be a lack of imagination on my part - there really could be a valid reason for directly exposing unsafe modules in such a manner.

Perhaps a better name for that second section would have been Salvaging Safe Haskell: keeping enough pieces of the old system to make something new (and ideally better)…

#80

Any examples of languages that have useful code safety guarantees? I don’t think anyone uses non-Turing-complete ones (StackExchange), so I imagine you should be able to loop allocations in any of your examples.

Types are nothing more than documentation that the compiler can read and check, and their usefulness far outweighs any potential problems from people violating them. See #60 and above for a long list of other things up the chain of execution that can happily break anything downstream.

Safe Haskell on the other hand does not give me the ability to point at a library with a Safe marking on it and say “yeah, that’s safe to use”, so I don’t see a point in fighting for it.

#81

You mean like not being able to:

…?

No, apparently not. But if you can provide the page numbers where general recursion and heap exhaustion are discussed in the original Safe Haskell paper, that would be appreciated.

Hrm:

freePrize :: Prize
freePrize = unsafePerformIO (stealCreditCardDetails >> randomPrize)

By "safe to use”, do you mean what is specified in the Safe Haskell paper, or your conveniently-expanded definition which also pursues general recursion and heap exhaustion?

#82

Alright you’ve done it, I’m closing this thread.
This is not the debate club, confrontational quips will have to happen elsewhere.

9 Likes
#83