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

В 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 и не нашел ни одной библиотеки, соответствующей моему описанию (размер индексированные изменяемые массивы).

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

 type Array n a = IORef (Vec n a)

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


arrays haskell dependent-type
person Rodrigo Ribeiro    schedule 10.01.2016    source источник

Ответы (1)


arrow_upward
7
arrow_downward

Такой тип существует в Hackage. .

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

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

import qualified Data.Vector.Unboxed.Mutable as VUM

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

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

person leftaroundabout    schedule 10.01.2016
comment
Извините за шум... Я пропустил эту библиотеку. Спасибо за внимание. - person Rodrigo Ribeiro; 11.01.2016