Размер индексированных изменяемых массивов в Haskell

Question

В Haskell можно писать функции над индексированным списком размера, гарантирующим, что мы никогда не выходим за пределы. Возможная реализация:

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      

Конечно, это очень хорошо для неизменен размера индексированных списков (он же Vec).

Но как насчет изменчивых? Можно определить (или есть библиотека для) измененных размеров индексированных массивов в Haskell? Если такой библиотеки нет, как ее можно реализовать?

Редактировать 1: Я искал Hackage и не нашел библиотеку, соответствующую моему описанию (размер индексированных изменяемых массивов).

Edit 2: Я хотел бы отметить, что я думал, что использование IORef «с, чтобы получить желаемую переменчивость:

type Array n a = IORef (Vec n a) 

, но мне интересно, если есть лучше (более эффективный, более элегантные) опция ...

Answer 1

такой тип does exist on Hackage.

Я бы избегал чего-то вроде type Array n a = IORef (Vec n a). Многочисленные массивы - все об эффективности. Если вам не нужно бегать быстро/с низким объемом памяти, тогда их не так много смысла - даже «изменчивые алгоритмы», как правило, легче выразить в Haskell, используя функциональный стиль, возможно, с государственной монадой, но без истинных разрушительных изменяемое состояние.
Но если эффективность имеет значение, то вы также нуждаетесь в жестком кэшировании. Unboxed vectors являются идеальными. OTOH, Vec находится на уровне данных во время выполнения, отличном от обычных списков, которые, конечно же, не столь велики с точки зрения согласованности кеша. Даже если бы вы определили их, чтобы на самом деле переплетить изменчивость в списке позвоночника, это было бы не лучше, чем использование неизменяемого Vec s в чисто функциональном стиле.

Итак, если бы мне пришлось написать что-то вроде этого простого, я бы предпочел бы обернуть (небезопасный, длинный) unboxed изменяемый arrox в индексе с индексированным по длине индексом.

import qualified Data.Vector.Unboxed.Mutable as VUM 

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

Затем можно определить интерфейс, который делает все государственные операции типа проверена длиной безопасной, сохраняя при этом профиле производительности MVector.