[Haskell-cafe] Safe Haskell?

[Bertram Felgenhauer]

Hi again,

I wrote:
> So I'd be sad to see SafeHaskell go away.

I've slept on this. The above is still true, but only because I happen
to have a use case that fits SafeHaskell pretty much perfectly. The
bigger picture is bleaker, and SafeHaskell may well be holding back
safe Haskell from reaching its full potential. Its main drawbacks are:

1) SafeHaskell imposes a single notion of safety upon the whole world.
First, safety is expressed through language pragmas, which are
Booleans attached to source code; basically whatever interpretation
the base library gives to safety is the one that everyone has to
use. On top of that, library maintainers are supposed to do the work
of declaring safety of their code, even if they do not care about
SafeHaskell at all. Secondly, the mechanism for inferring safety is
baked into the compiler, but different notions of safety may require
different inference mechanisms.

Unless the use case for which SafeHaskell was designed is common
(and the replies here indicate that it's not), this is hard to
justify.

2) Since SafeHaskell is integrated in GHC, it's hard to improve, and
SafeHaskell is lacking in some regards. For example, safety is
declared at the module level, rather than the level of exported
symbols. This is unfortunate, because the real cost is not in adding
annotations to files, but in reviewing individual definitions; the
more definitions can be inferred as safe the better, and a finer
granularity would help there.


In principle, most of SafeHaskell's functionality could be covered by
external tools, including managing lists of safe/trusted/unsafe
modules (or exports) and tracking safety dependencies for inferred
safety or unsafety. There could be a standard file format for such
lists, so they can be shared easily. (The information could even be
expressed in source code pragmas and be extracted from there, so there
doesn't need to be any loss compared to the existing SafeHaskell.)

The parts that require compiler support are inference of safety, and
checking language extensions and imports against a whitelist. For
these things, compiler plugins should work [*]. Maybe a set of utility
functions or even an abstraction layer from the GHC API can be found
to support these tasks.

Ideally, we could have a nice suite of tools for code auditing (define
a desired property, chase it through a code base) that supports
checking functions automatically through compiler plugins. And if
enough people care about a particular property and trust each other's
analysis, results could be shared.

And of course, the original SafeHaskell use case ala lambdabot would
still be covered, since it boils down to only allowing code whose
safety can be inferred automatically.

There would inevitably be a mess of different safety notions. But that
is already the case now. The difference is that currently, only one
notion is blessed and supported by GHC and all the others are not.

Cheers,

Bertram

[*] I'm a bit worried that I'm being too naive there. Why is
SafeHaskell such a burden within GHC? Is it because it touches many
parts, from language pragmas to interface files to actually checking
imports? Or am I forgetting something about SafeHaskell that requires
deep integration, say, into the type checker?