Каковы точные критерии для типа, подлежащего сохранению? - PullRequest
Новая
       73

Каковы точные критерии для типа, подлежащего сохранению?

1 голос
/ 07 октября 2019

Я давно реализовал тип данных для симметричных групп (и циклических групп): 

newtype Cyclic (n :: Nat) = Cyclic {cIndex :: Integer}

data Symmetric (n :: Nat) where
    S1 :: Symmetric 1
    (:.) :: Cyclic n -> Symmetric (n-1) -> Symmetric n

Это неоднородный контейнер, , но я не уверен, является ли это массивом илисписок. Как поясняют комментарии, это не проблема.

Если это массив, можно было бы реализовать instance Storable (Symmetric n). Почему именно это можно сделать?

1 Ответ

1 голос
/ 07 октября 2019

Storable призвано вызвать идею C struct s. Как struct, любой тип Storable имеет ограниченный размер. Storable (Symmetric n) возможно, потому что Symmetric n на самом деле ограниченного размера. (Предполагая, что Cyclic n s эквивалентны по модулю n,). Он имеет значения n!, которые являются конечными, и поэтому вам не нужно неограниченное пространство. В частности, достаточно log2(n!) битов. Обратите внимание, что я говорю о Symmetric n для некоторого конкретного n. Для разных Nat с n, m и т. Д. Symmetric n, Symmetric m и т. Д. Имеют разные типы, и поэтому они могут иметь разные размеры. Для одного n :: Nat, Symmetric n имеет фиксированный размер.

Реальная проблема заключается в выборе кодировки. Для простоты реализации вы можете использовать рекурсивное кодирование, где Storable n состоит из ceil(log2(n) / 8) байтов для хранения первого числа, за которым следует Storable (n - 1). Тогда Symmetric 1 будет 0 байтов, Symmetric 2 будет 1 байтом (используется только один бит), Symmetric 3 будет 2 байта, ..., Symmetric 256 будет 255 байтов, Symmetric 257будет 257 байтов (потому что первое число имеет 257 вариантов выбора и поэтому требует двух байтов). Это, конечно, неэффективно, но вы можете ясно видеть, что для каждого Symmetric n есть четко определенный размер. Если вы хотите перейти к пределу log2(n!) битов (на самом деле, ceil(log2(n!)/8) байт), вам придется сделать некоторую ~~ фанк-математику ~~ (с которой я не знаком), но вы можете сделатьэто.

Вам нужны одиночные, чтобы сделать эту работу;можно написать 

instance KnownNat n => Storable (Symmetric n)

, но не 

instance Storable (Symmetric n)

Типы стираются, поэтому второй instance не сообщается, что такое n, и, следовательно, ничего не может прочитать (или внедрить sizeof и т. д.). Он может писать, потому что Symmetric является GADT и, таким образом, содержит информацию о том, что такое n.

Примечание: не должно ли Symmetric 0 быть непустым? 

data Symmetric (n :: Nat) where
    S0 :: Symmetric 0
    (:.) :: Cyclic n -> Symmetric (n - 1) -> Symmetric n

Symmetric 0 - это набор биекций из пустого набора в себя, и в нем есть только одна функция (пустой набор)комплект.

...