<div dir="ltr">Hi Ed,<div><br></div><div>Thanks, I went back to the paper and read those sections.</div><div><br></div><div>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 <i>spirit</i> of the type safety guarantee mentioned in the paper:</div><div>
<div title="Page 3">
<div>
<div>
<p><span style="font-size:8pt;font-family:CMSY8;vertical-align:1pt"></span><span style="font-size:9pt;font-family:NimbusRomNo9L;font-style:italic">"Type safety. </span><span style="font-size:9pt;font-family:NimbusRomNo9L">In Milner’s famous phrase, well-typed programs do
not go wrong. "</span></p></div></div></div></div><div>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. </div><div><br></div><div>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 <i>in the IO monad</i>. I think it's quite <b>reasonable to expect Safe Haskell to be as safe as Java! </b> 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.</div><div><br></div><div>One question I have for people is which of the following they would favor:</div><div><ol><li>Redefine -XSafe to guarantee something about IO and its memory safety (and even its memory model)</li><li>Add a fourth safety level, "SafeExceptIO", that corresponds to the current guarantees, while extending "Safe" to say something about IO. </li><li>Leave safe Haskell as it is.</li></ol></div><div>(2) sounds a bit clunky to me, and I favor (1) most of all.</div><div><br></div><div>Best,</div><div> -Ryan</div><div><br></div><div>[1] 17M lines on hackage total, hard to count how much is in an IO monad or related monad.</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Aug 8, 2016 at 2:05 PM, Edward Z. Yang <span dir="ltr"><<a href="mailto:ezyang@mit.edu" target="_blank">ezyang@mit.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello Ryan,<br>
<br>
The guarantee that Safe Haskell gives with regards to IO is a little<br>
subtle and is mentioned in Section 3.1 of the paper, and detailed<br>
in Section 5.1. Essentially, to use Safe Haskell, you are responsible<br>
for defining the type at which untrusted code is to be called.<br>
Using an untrusted value at type IO a in main imposes no safety<br>
restrictions by design--it's up to the user of Safe Haskell to<br>
decide what kind of security properties it needs out of user code.<br>
<br>
Edward<br>
<br>
Excerpts from Ryan Newton's message of 2016-08-08 13:27:16 -0400:<br>
<span class="">> We're trying to spend some cycles pushing on Safe Haskell within the<br>
> stackage packages. (It's looking like a slog.)<br>
><br>
> But we're running up against some basic questions regarding the core<br>
> packages and Safe Haskell guarantees. The manual currently says:<br>
</span>> <<a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/safe_haskell.html#safe-language" rel="noreferrer" target="_blank">https://downloads.haskell.<wbr>org/~ghc/latest/docs/html/<wbr>users_guide/safe_haskell.html#<wbr>safe-language</a>><br>
><br>
><br>
> *Functions in the IO monad are still allowed and behave as usual. *<br>
<div class="HOEnZb"><div class="h5">> As usual? So it is ok to segfault GHC? Elsewhere it says "in the safe<br>
> language you can trust the types", and I'd always assumed that meant Safe<br>
> Haskell is a type safe language, even in the IO fragment.<br>
><br>
> Was there an explicit decision to allow segfaults and memory corruption?<br>
> This can happen not just with FFI calls but with uses of Ptrs within<br>
> Haskell, for example the following:<br>
><br>
><br>
> ```<br>
><br>
> {-# LANGUAGE Safe #-}<br>
><br>
> module Main where<br>
><br>
> import Foreign.Marshal.Alloc<br>
><br>
> import Foreign.Storable<br>
><br>
> import Foreign.Ptr<br>
><br>
> import System.Random<br>
><br>
><br>
> fn :: Ptr Int -> IO ()<br>
><br>
> fn p = do<br>
><br>
> -- This is kosher:<br>
><br>
> poke p 3<br>
><br>
> print =<< peek p<br>
><br>
> -- This should crash the system:<br>
><br>
> ix <- randomIO<br>
><br>
> pokeElemOff p ix 0xcc<br>
><br>
><br>
><br>
> main = alloca fn<br>
><br>
> ```<br>
><br>
><br>
> -Ryan<br>
</div></div></blockquote></div><br></div>