haskell / haskell/primitive

Safe use of unsafeFreeze in arbitrary PrimMonad

Open
#431 0 comments 3 reactions 0 assignees View on GitHub
documentation
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.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.