Safe use of unsafeFreeze in arbitrary PrimMonad
- Dominant language
- Haskell
- Stars
- 123
- Forks
- 60
- PR merge metrics
- No merged PRs in 30d
Description
As it turns out use of `unsafeFreeze` (for whatever array library) together with polymorphic `PrimMonad` allows to violate referential transparency using seemingly reasonable code. Let consider following pseudocode:
```haskell
do v <- newArray 2
write v 0 =<< action0
write v 1 =<< action1
unsafeFreeze v
```
It looks perfectly safe and it is safe for some monads like IO,ST, transfomers like Writer/Reader/State. Yet for monads which allow backtracking it allows to break referential transparency. Here's examples using `ListT` from `list-t` and `ContT` monads and vector package:
```haskell
{-# LANGUAGE TypeFamilies #-}
module Q where
import Control.Applicative
import Control.DeepSeq
import Control.Monad.Primitive
import Control.Monad.Trans.Class
import Control.Monad.Trans.Cont
import Data.Vector.Unboxed qualified as VU
import Data.Vector.Unboxed.Mutable qualified as VUM
import ListT (ListT(..), toList)
instance PrimMonad m => PrimMonad (ListT m) where
type PrimState (ListT m) = PrimState m
primitive = lift . primitive
horror :: IO [([Int], VU.Vector Int)]
horror = ListT.toList $ do
mv <- VUM.replicateM 2 $ pure 0 <|> pure 1
v <- VU.unsafeFreeze mv
let !i = force $ VU.toList v
pure (i,v)
liftList :: Monad m => [a] -> ContT [r] m a
liftList xs = ContT $ \cnt -> concat <$> traverse cnt xs
continuedHorror :: IO [([Int], VU.Vector Int)]
continuedHorror = flip runContT (pure . pure) $ do
mv <- VUM.replicateM 2 $ liftList [0, 1]
v <- VU.unsafeFreeze mv
let !i = force $ VU.toList v
pure (i,v)
```
both functions return
```
([0,0],[1,1])
([0,1],[1,1])
([1,0],[1,1])
([1,1],[1,1])
```
It's not surprising since we have 4 vectors sharing same buffer.
But this pattern is clearly useful. So it would be nice to have type class with laws which tell that such use of `unsafeFreeze` is safe. Informally it's clear: no backtracking but I would like to have law with firmer footing.
This issue was brought up during discussions about implementation of `unstreamM` variant which writes directly to vector. See haskell/vector#416 and haskell/vector#544 for discussion
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.