Is Safe Haskell intended to allow segfaults?

[Edward Z. Yang]

I think what you are proposing is reasonable.  I wasn't present
when Safe Haskell's design was originally fleshed out so I don't
know why this route wasn't taken.

Edward

Excerpts from Ryan Newton's message of 2016-08-08 16:00:38 -0400:
> Hi Ed,
> 
> Thanks, I went back to the paper and read those sections.
> 
> It sounds like this design heavily reflects the untrusted-code use case.  I
> believe ceding the entire IO monad is too pessimistic, and it's also
> against the *spirit* of the type safety guarantee mentioned in the paper:
> 
> "Type safety. In Milner’s famous phrase, well-typed programs do not go
> wrong. "
> There's not really very much discussion of this "punting on IO" decision in
> the paper.  The paper mentions not deleting users files as an example of a
> higher level security policy -- and a reason not  to try to lock down IO --
> but that's not really the issue here.
> 
> Sure, there are many use cases that require an RIO newtype, but the memory
> model and memory protection are really internal to the language.  My
> interest is in a type safe language with a memory model *in the IO monad*.
> I think it's quite *reasonable to expect Safe Haskell to be as safe as
> Java! * There are hundreds of thousands or millions of lines of code
> written in the IO monad [1], and a lot of that code could probably be
> memory safe by construction.
> 
> One question I have for people is which of the following they would favor:
> 
>    1. Redefine -XSafe to guarantee something about IO and its memory safety
>    (and even its memory model)
>    2. Add a fourth safety level, "SafeExceptIO", that corresponds to the
>    current guarantees, while extending "Safe" to say something about IO.
>    3. Leave safe Haskell as it is.
> 
> (2) sounds a bit clunky to me, and I favor (1) most of all.
> 
> Best,
>   -Ryan
> 
> [1] 17M lines on hackage total, hard to count how much is in an IO monad or
> related monad.
> 
> On Mon, Aug 8, 2016 at 2:05 PM, Edward Z. Yang <ezyang at mit.edu> wrote:
> 
> > Hello Ryan,
> >
> > The guarantee that Safe Haskell gives with regards to IO is a little
> > subtle and is mentioned in Section 3.1 of the paper, and detailed
> > in Section 5.1. Essentially, to use Safe Haskell, you are responsible
> > for defining the type at which untrusted code is to be called.
> > Using an untrusted value at type IO a in main imposes no safety
> > restrictions by design--it's up to the user of Safe Haskell to
> > decide what kind of security properties it needs out of user code.
> >
> > Edward
> >
> > Excerpts from Ryan Newton's message of 2016-08-08 13:27:16 -0400:
> > > We're trying to spend some cycles pushing on Safe Haskell within the
> > > stackage packages.  (It's looking like a slog.)
> > >
> > > But we're running up against some basic questions regarding the core
> > > packages and Safe Haskell guarantees.  The manual currently says:
> > > <https://downloads.haskell.org/~ghc/latest/docs/html/
> > users_guide/safe_haskell.html#safe-language>
> > >
> > >
> > > *Functions in the IO monad are still allowed and behave as usual. *
> > > As usual?  So it is ok to segfault GHC?  Elsewhere it says "in the safe
> > > language you can trust the types", and I'd always assumed that meant Safe
> > > Haskell is a type safe language, even in the IO fragment.
> > >
> > > Was there an explicit decision to allow segfaults and memory corruption?
> > > This can happen not just with FFI calls but with uses of Ptrs within
> > > Haskell, for example the following:
> > >
> > >
> > > ```
> > >
> > > {-# LANGUAGE Safe #-}
> > >
> > > module Main where
> > >
> > > import Foreign.Marshal.Alloc
> > >
> > > import Foreign.Storable
> > >
> > > import Foreign.Ptr
> > >
> > > import System.Random
> > >
> > >
> > > fn :: Ptr Int -> IO ()
> > >
> > > fn p = do
> > >
> > >   -- This is kosher:
> > >
> > >   poke p 3
> > >
> > >   print =<< peek p
> > >
> > >   -- This should crash the system:
> > >
> > >   ix <- randomIO
> > >
> > >   pokeElemOff p ix 0xcc
> > >
> > >
> > >
> > > main = alloca fn
> > >
> > > ```
> > >
> > >
> > >   -Ryan
> >