Skip to content

Safe use of unsafeFreeze in arbitrary PrimMonad #431

@Shimuuar

Description

@Shimuuar

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:

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:

{-# 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

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions