Violating memory safety with Haskell's value restriction

Links
1
21 Likes
2

Thanks! Very clear, well-written and interesting article. Does that mean that this definition from linear-base is unsafe?

I attempted to use your same trick to derive something unsafe, but I couldn’t get it to work. It don’t know whether it doesn’t work because of some issue with linear lets, or Ur, or something else, and whether the “issue” is intended (and is a theoretical means of preventing unsafety) or it’s unintended and can be worked around.

Not working linear example 
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE ImportQualifiedPost #-}

import System.IO.Linear
import Control.Functor.Linear qualified as L
import Control.Functor.Linear hiding (state)
import Prelude hiding (IO, (<$>), (>>=), pure, Monad)
import GHC.Exts
import System.IO.Linear
import Data.IORef (IORef)
import Data.Unrestricted.Linear

class (Monad m) => MonadGen m where
    generalize :: forall f. (forall a. m (f a)) -> m (forall a. f a)

data BoxedState s = BoxedState {state :: State# s}

liftState :: (# State# s, b #) %1 -> (BoxedState s, b)
liftState (# s, b #) = (BoxedState s, b)

myGeneralize :: forall f. (forall a. IO (f a)) -> IO (forall a. f a)
myGeneralize m = do
        let (IO f) = m
        IO \s -> do
            let (!boxedState, !result) = liftState (f s)
            let BoxedState{state} = boxedState
            (# state, result #)

instance MonadGen IO where
    generalize = myGeneralize

newtype MaybeRef a = MaybeRef (IORef (Maybe a))

unsafeCoerceIO :: forall a b. a -> IO b
unsafeCoerceIO x = L.do
    maybeRef <- generalize (newIORef Nothing)
    let MaybeRef ref = maybeRef
    writeIORef ref (Just x)
    readIORef ref >>= \case
        Ur (Just y) -> pure y
        Ur Nothing -> error "unreachable"
1 Like
3

That was entertaining to read.

The crux of it is that GHC represents IO actions as effectful functions State# -> (# State#, a #). In a language like OCaml, where all functions are effectful, there is a value restriction (= a special rule in the type system) to enable type safety. In GHC, these effectful functions are an implementation detail, and type safety is ensured by hiding those details.

3 Likes
4

Yes, I think, in a sense, IO is a “reification” of the value restriction.

5

I suspect that we are saved by the fact that only monomorphic mutable references are duplicable.

unsafeCoerceIO relies on writing to IORef a and reading from IORef b, so we need to duplicate a polymorphic reference so it can be instantiated at different types:

type UrIORef = forall a. Ur (IORef a)
_ :: UrIORef 1% -> (UrIORef, UrIORef)  -- unimplementable

But duplication is done by dup2 from the Dupable class. (Or equivalently by pattern-matching on Ur.) It requires a monomorphic IORef:

dup2 :: Ur (IORef a) 1% -> (Ur (IORef a), Ur (IORef a))
5 Likes