Right - Safe Haskell provides the minimum that you need to be able to safely run untrusted code: the ability to trust the type system and the module system. Definining a safe subset of IO is usually an application-specific decision, e.g. do you want to allow access to the filesystem but without allowing openFile "/dev/mem"? It's a minefield.
Ryan, if you want to give an operational semantics for memory in IO, why not start from the subset of IO that you can accurately model - the basic IO structure together with a set of primitives - and define the semantics for that? That's typically what we do when we're talking about something in the IO monad. Cheers Simon On 10 August 2016 at 04:58, Edward Kmett <ekm...@gmail.com> wrote: > I see three major stories here: > > 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'd have to cut up too many APIs into too many > fine-grained pieces. This would considerably reduce the utility of Safe > Haskell to me. Many of them expose a few combinators here and there that > happen to live in IO and I can view offering Safe or Trustworthy to users > as a 'the pure stuff looks really pure' guarantee. For the most part it > 'just works' and Trustworthy annotations can be put in when I know the > semantics of the hacks I'm using under the hood. > > 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. At least then you could say what you are safe > with respect to. That all seems to be rather a big mess, roughly equivalent > to modeling an effect system for IO operations, and then retroactively > categorizing everything, putting a big burden on maintainers and requiring > a lot of community buy-in, sight unseen. > > 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. then pull a couple of Trustworthy modules > around it for embedding the effects they want to permit and build this > today without any compiler support, they'd just have to make a final > application-specific Trustworthy wrapper to run whatever effects they want > to permit into their program. It is more invasive to the code in question, > but it requires zero community organizing and we've already got all the > compiler mojo we need. The downside is the Trustworthy wrappers at the > bottom of the heap and that it doesn't interoperate with basically anything > already written. > > -Edward > > On Tue, Aug 9, 2016 at 10:45 PM, Ryan Newton <rrnew...@gmail.com> wrote: > >> I'm hearing that Safe Haskell is great for pure use cases (lambda bot). >> But that doesn't depend on being able to write arbitrary IO code inside the >> Safe bubble, does it? In fact *all* of IO could be outside the safe >> boundary for this use case, could it not? Are there any existing cases >> where it is important to be able to build up unsafe IO values inside -XSafe >> code? >> >> Edward, why does it seem like a losing proposition? Are there further >> problems that come to mind? ezyang mentioned the subprocess problem. I >> don't have a strong opinion on that one. But I tend to think the safe IO >> language *should* allow subprocess calls, and its a matter of >> configuring your OS to not allow ptrace in that situation. This would be >> part of a set of requirements for how to compile and launch a complete >> "Safe Haskell" *program* in order to get a guarantee. >> >> My primary interest is actually not segfault-freedom, per-se, but being >> able to define a memory model for Safe Haskell (for which I'd suggest >> sequential consistency). FFI undermines that, and peek/poke seems like it >> should cluster with FFI as an unsafe feature. I'm not inclined to give a >> memory model to peek or FFI -- at that level you get what the architecture >> gives you -- but I do want a memory model for IORefs, IOVectors, etc. >> >> We're poking at the Stackage package set now to figure out what pressure >> point to push on to increase the percentage of Stackage that is Safe. I'll >> be able to say more when we have more data on dependencies and problem >> points. Across all of hackage, Safe Haskell has modest use: of the ~100K >> modules on Hackage, ~636 are marked Safe, ~874 trustworthy, and ~118 >> Unsafe. It should be easy to check if any of this Safe code is currently >> importing "Foreign.*" or using FFI. >> >> My general plea is that we not give the imperative partition of Haskell >> too much the short end of the stick [1]. There is oodles of code in IO (or >> MonadIO), and probably relatively little in "RIO". To my knowledge, we >> don't have great ways to coin "RIO" newtypes without having to wrap and >> reexport rather a lot of IO functions. Maybe if APIs like MVars or files >> were overloaded in a class then GND could do some of the work... >> >> -Ryan >> >> [1] In safety guarantees, in optimizations, primops, whatever... For >> instance, I find in microbenchmarks that IO code still runs 2X slower than >> pure code, even if no IO effects are performed. >> >> >> >> On Tue, Aug 9, 2016 at 5:13 PM, Edward Kmett <ekm...@gmail.com> wrote: >> >>> I've always treated Safe Haskell as "Safe until you allow IO" -- in that >>> all 'evil' things get tainted by an IO type that you can't get rid of by >>> the usual means. So if you go to run pure Safe Haskell code in say, >>> lambdabot, which doesn't give the user a means to execute IO, it can't >>> segfault if all of the Trustworthy modules you depend upon actually are >>> trustworthy. >>> >>> Trying to shore up segfault safety under Safe in IO seems like a losing >>> proposition. >>> >>> -Edward >>> >>> On Mon, Aug 8, 2016 at 1:27 PM, Ryan Newton <rrnew...@gmail.com> wrote: >>> >>>> 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 >>>> >>>> >>> >> > > _______________________________________________ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
