Gregory Collins | 17 Jul 2012 19:57
Gravatar

Re: Safe Haskell and Haskell Platform: near-term tactics

Re-adding haskell-platform <at> , which I assume you left off by accident?

On Tue, Jul 17, 2012 at 7:05 PM, Yitzchak Gale <gale <at> sefer.org> wrote:
Gregory Collins wrote:
> This slightly underestimates the amount of work required. Each package's api
> must be carefully audited for unsafe functions, you can't just slap a
> "trustworthy" on everything and call it a day. If any legitimately unsafe
> functions are found, the APIs need to be separated out into safe and unsafe
> modules, and the old modules must go through a deprecation cycle.

No, it's really simple. Did you read Simon's paper,
and his emails in this and related threads?

I emphasize that I am *not* advocating requiring
platform packages to have best possible support
for Safe Haskell. That can come later after we
get more experience and see how it is used
in practice, as Mark says. That will take time.

I am only advocating *recommending* that
packages provide at least *minimal* support -
namely, a simple Trustworthy pragma, which
is almost always possible. That is in order to
help bootstrap the process, to make adoption of
Safe Haskell possible. Then we'll see if it
really happens. (After reading Simon's paper,
I believe there is a good chance it will if
we do this.)

From the paper:

"A module that is declared to be Trustworthy is claimed by the
author to expose a safe interface, even though its implementation
might make use of unsafe features."

Putting a Trustworthy on the top of a module means that "I, the module author, assert that any uses of unsafePerformIO and friends in this module are safe and using the functions herein will not violate safety." You can't just slap a Trustworthy on everything and go home, every module in the platform needs to be audited.

If a module does export a legitimately unsafe function (like the ones we've already identified), then the unsafe bits will need to be moved into a new module so that the package can export modules that *can* be either safe-inferred or marked trustworthy. This is all I'm saying.

Happily, from what I can see, the only legitimately unsafe module in the platform outside of the core libs (which I understand someone -- Simon? -- has already audited) is Data.Text.Array, so this is indeed probably just hullabaloo about nothing on my part. Still: I just did a quick grep, someone (or several someones) has to do a careful audit.

I really don't get what all the noise is about. We're talking
about a single language pragma at the top of each module.

Again: no, we aren't :). It's likely that in almost every case putting the pragma in will be the end result, but: the work is in the audit! We can't just gloss over that.
 
> regex-posix has lots of "unsafePerformIO"

Re-exported to the user? I doubt it. There is
no problem with unsafePerformIO if it is
used internally and the author believes that
the usage is safe.

Right. Those need Trustworthy pragmas.
 
> network looks like it needs some work

All exposed pointer-poking functions are in
IO. So after Simon's comment, it looks like
we can mark everything Trustworthy without
change, even Internal. Correct me if I'm
wrong.

There are several unsafePerformIOs in there also. The use is also almost certainly fine, but again, a human needs to audit before the pragma can be applied.

G
--
Gregory Collins <greg-Ul5JJHalTl8GkDYIr3kye6xOck334EZe@public.gmane.org>
_______________________________________________
Haskell-platform mailing list
Haskell-platform@...
http://projects.haskell.org/cgi-bin/mailman/listinfo/haskell-platform
Yitzchak Gale | 17 Jul 2012 20:51

Re: Safe Haskell and Haskell Platform: near-term tactics

Gregory Collins wrote:
> From the paper:
>
> "A module that is declared to be Trustworthy is claimed by the
> author to expose a safe interface, even though its implementation
> might make use of unsafe features."
>
> Putting a Trustworthy on the top of a module means that "I, the module
> author, assert that any uses of unsafePerformIO and friends in this module
> are safe and using the functions herein will not violate safety." You can't
> just slap a Trustworthy on everything and go home, every module in the
> platform needs to be audited.

So I guess we disagree about how to interpret
Simon's use of the word "claim".

From the tone of the rest of the paper, I understood
that no "audit" or formal proof of any sort is needed.
Just that the author believes that any use of a
potentially unsafe feature is OK.

So by my reading, it is enough just to look over the
API to make sure nothing apparently unsafe is
exported, plus include in our email to the package
maintainer a request to contact the list before adding
the pragma if there is a suspicion that something
unsafe might be going on.

Anyway, in real life, most of us are pretty familiar
with most of the packages in the platform.
We've identified a few that need some thought.
If there are any other problems, I hope someone
here will let us know.

Thanks,
Yitz
Gregory Collins | 17 Jul 2012 21:09
Gravatar

Re: Safe Haskell and Haskell Platform: near-term tactics

On Tue, Jul 17, 2012 at 8:51 PM, Yitzchak Gale <gale-qokrdK/Rc/HYtjvyW6yDsg@public.gmane.org> wrote:
So by my reading, it is enough just to look over the
API to make sure nothing apparently unsafe is
exported

That's an audit :). I'm just saying that it ought to be done quite carefully. If we care about Safe Haskell being useful at all, we need to at least get it right for the platform packages! It's already been noted that Data.Binary.Builder.Internal, for example, which was marked Trustworthy, exports an ostensibly pure function that could be used to violate type safety:

writeN :: Int -> (Ptr Word8 -> IO ()) -> Builder

You need Foreign.Ptr in scope to make that happen, but that's marked Trustworthy also. Put the two together and you can scribble on arbitrary memory locations from a pure function.

G
--
Gregory Collins <greg-Ul5JJHalTl8GkDYIr3kye6xOck334EZe@public.gmane.org>
_______________________________________________
Haskell-platform mailing list
Haskell-platform@...
http://projects.haskell.org/cgi-bin/mailman/listinfo/haskell-platform

Gmane