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 <ezy...@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 > > _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs