Is Safe Haskell intended to allow segfaults?

[Ryan Newton]

Yes, it is peek and poke that are dangerous.  It was Foreign.Storable that
I wanted to mark as Unsafe.

But we do sometimes run into examples where there's an A and a B, and if
you import both, you can make A+B which blows up.  So preventing access to
A+B may mean arbitrarily marking one or the other (or both) as Unsafe.

What I was hoping for examples of are modules you have that are Safe and
import Foreign.Storable.




On Fri, Aug 12, 2016 at 9:49 AM, Edward Kmett <ekmett at gmail.com> wrote:

> As for a sample list of modules, let's just start with your very first
> example, Foreign.Ptr:
>
> In and of itself nothing in Foreign.Ptr is unsafe! It allows a bit of
> arithmetic on a type you can't actually use with anything, and provides an
> IO action mixed into an otherwise pure module that happens to create a
> FunPtr slot from a haskell function. In fact this module is a textbook
> example of an otherwise perfectly cromulent Trustworthy module today that
> happens to have a single IO action in it.
>
> I can grab Ptr from it, use its Storable instance to make a default
> signature for other safe code and still be perfectly safe.
>
> It gives no tools for manipulating the contents of the Ptr. It is no more
> dangerous than an Int with a phantom type argument.
>
> You could randomly declare that this module is Unsafe because it combines
> badly with APIs that would be safe if you could rely on any Ptr T actually
> pointing to a T, and that users could then be granted the power to ferry
> them around, but we don't trust a user to be able to do that today.
>
> It's the combinators that read/write to a Ptr are the dangerous bits, not
> pure math.
>
> -Edward
>
>
> On Wed, Aug 10, 2016 at 10:23 AM, Ryan Newton <rrnewton at gmail.com> wrote:
>
>> Hi Edward,
>>
>> On Tue, Aug 9, 2016 at 11:58 PM, Edward Kmett <ekmett at gmail.com> wrote:
>>>
>>> 1.) If you remove IO from being able to be compiled inside Safe code _at
>>> all_ most packages I have that bother to expose Safe information will have
>>> to stop bothering.
>>>
>>
>> I definitely wouldn't argue for removing it entirely.  But it's good to
>> know that there are instances where IO functions get mixed up in safe
>> modules.  I'll try to systematically find all of these on hackage, but in
>> the meantime do you have a sample list of modules?
>>
>> My modest starting proposal is marking certain Foreign.* modules as
>> Unsafe rather than Trustworthy.  We'll find all the modules affected.  But,
>> again, are there any modules you know of offhand that are affected?  They
>> should fall into two categories:
>>
>>    1. Safe modules that must become Trustworthy (if they import Foreign
>>    bits, but don't expose the ability to corrupt memory to the clients of
>>    their APIs).
>>    2. Safe modules that must become Unsafe or be split further into
>>    smaller modules.
>>
>> Obviously (2) is the biggest source of potential disruption.
>>
>> I wouldn't ask anyone to accept a patch on GHC until we'd explored these
>> impacts pretty thoroughly.
>>
>> I'd have to cut up too many APIs into too many fine-grained pieces.
>>>
>>
>> Yeah, the module-level business is pretty annoying.  "vector' removed
>> ".Safe" modules and no one has gotten around to adding the ".Unsafe".
>>
>>
>>> 2.) Assuming instead that you're talking about a stronger-than-Safe
>>> additional language extension, say ReallySafe or SafeIO, it all comes down
>>> to what the user is allowed to do in IO, doesn't it? What effects are users
>>> granted access to? We don't have a very fine-grained system for IO-effect
>>> management, and it seems pretty much any choice you pick for what to put in
>>> the sandbox will be wrong for some users, so you'd need some sort of pragma
>>> for each IO operation saying what bins it falls into and to track that
>>> while type checking, etc.
>>>
>>
>> Well, *maybe* it is a slippery slope that leads to a full effect
>> system.  But I'd like to see these issues enumerated.  Does memory safety
>> as a goal really involve so many different effects?  Do you think there
>> will be 1, 3, 10, or 100 things beyond Foreign.Ptr to worry about?
>>
>> 3.) On the other hand, someone could _build_ an effect system in Haskell
>>> that happens to sit on top of IO, holding effects in an HList, undischarged
>>> nullary class constraint, etc.
>>>
>>
>> Well, sure, I hope we will continue to aim for this as well.  This is
>> effectively what we do with our "LVish" Par monad, where we use Safe
>> Haskell to ensure users cannot break the effect system in -XSafe code.
>>
>> Best,
>>  -Ryan
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160812/0defa233/attachment.html>