Is Safe Haskell intended to allow segfaults?

[Edward Kmett]

What about consuming Storable Vectors carefully, or simply working
parameterized over vector type, where Storable vectors are one of the
options?

-Edward

On Fri, Aug 12, 2016 at 12:58 PM, Ryan Newton <rrnewton at gmail.com> wrote:

> 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/5f05c0de/attachment.html>