CODEWITHSUNDEEP
arrayshaskelldependent-type
Rodrigo Ribeiro
Rodrigo Ribeiro

Reputation: 3218

Size indexed mutable arrays in Haskell

In Haskell is possible to write functions over a size indexed list that ensure that we never get out of bounds. A possible implementation is:

data Nat = Zero | Succ Nat deriving (Eq, Ord, Show)

infixr 5 :-

data Vec (n :: Nat) a where
    Nil  :: Vec 'Zero a
    (:-) :: a -> Vec n a -> Vec ('Succ n) a       

data Fin (n :: Nat) where
    FZ :: Fin ('Succ n)
    FS :: Fin n -> Fin ('Succ n)                       

vLookup :: Vec n a -> Fin n -> a
vLookup Nil _ = undefined           
vLookup (x :- _) FZ = x
vLookup (_ :- xs) (FS i) = vLookup xs i

Of course, this is just fine for immutable size indexed lists (aka Vec).

But how about mutable ones? Is possible to define (or is there a library for) mutable size indexed arrays in Haskell? If there's no such library, how it could be implemented?

Edit 1: I searched Hackage and didn't found any library matching my description (size indexed mutable arrays).

Edit 2: I would like to mention that I have thought use IORef's to get the desired mutability:

 type Array n a = IORef (Vec n a)

but I'm wondering if there's a better (more efficient, more elegant) option...

Upvotes: 2

Views: 191

Answers (1)

leftaroundabout
leftaroundabout

Reputation: 120711

Such a type does exist on Hackage.

I would avoid something like type Array n a = IORef (Vec n a). Mutable arrays are all about efficiency. If you don't need it to run fast / with low memory footprint, then there's not much point in using them – even “mutable algorithms” are generally easier to express in Haskell using functional style, perhaps with a state monad but no true destructive mutable state.
But if efficiency matters, then you also want tight cache-efficient storage. Unboxed vectors are ideal. OTOH, Vec is on the runtime data level no different from ordinary lists, which are of course not so great in terms of cache coherence. Even if you defined them to actually interweave mutability into the list spine, it wouldn't be really better in any way than using immutable Vecs in a pure-functional style.

So, if I had to write something like that simple, I'd rather wrap an (unsafe, length-wise) unboxed mutable arrox in a length-indexed newtype.

import qualified Data.Vector.Unboxed.Mutable as VUM

newtype MVec (s :: *) (n :: Nat) (a :: *)
        = MVec { getMVector :: VUM.MVector s a }

You can then define an interface that makes all public operations type-checked length-safe, while still retaining the performance profile of MVector.

Upvotes: 7

Related Questions