Я только начинаю изучать Идрис и решил, что для начала неплохо было бы реализовать конечные последовательности в виде деревьев на 2-3 пальца. Каждый внутренний узел в дереве необходимо аннотировать во время выполнения с указанием общего количества элементов, хранящихся под ним, для поддержки быстрого разделения и индексации. Этой информацией о размере также необходимо управлять во время компиляции, чтобы (в конечном итоге) доказать, что разделение с соответствующими индексами и сжатие последовательности с другой последовательностью являются общими операциями.
Я могу придумать два способа справиться с этим:
То, что я сейчас делаю, написав крошечную долю от общего необходимого кода: полностью обрабатываю размеры в типах, а затем использую что-то вроде
proof {intros; exact s;}, чтобы добраться до них. Я не знаю, какие ужасные последствия для эффективности это может иметь, если таковые имеются. Среди потенциальных возможностей в моей голове: а) Излишнее сохранение размера с каждым листовым узлом. б) Я думаю, что это маловероятно, но было бы очень плохо, если бы он настаивал на вычислении размеров снизу вверх, а не лениво сверху вниз.Включите явное поле размера в каждый конструктор узла вместе с доказательством того, что число в поле размера соответствует размеру, необходимому для системы типов. Такой подход кажется крайне неудобным. С другой стороны, я должен быть уверен в том, что номера уровня типа и доказательства равенства будут стерты, оставив только одно число на каждый внутренний узел во время выполнения.
Какой из них, если таковой существует, является правильным?
Текущий код
Не стесняйтесь давать советы по стилю и, возможно, объяснять, как встроить код размера. Я мог только понять, что делать в интерактивном режиме, но мне кажется немного странным иметь внизу доказательства таких простых вещей.
data Tree23 : Nat -> Nat -> Type -> Type where
Elem : a -> Tree23 0 1 a
Node2 : Lazy (Tree23 d s1 a) -> Lazy (Tree23 d s2 a) ->
Tree23 (S d) (s1 + s2) a
Node3 : Lazy (Tree23 d s1 a) -> Lazy (Tree23 d s2 a) -> Lazy (Tree23 d s3 a) ->
Tree23 (S d) (s1 + s2 + s3) a
size23 : Tree23 d s a -> Nat
size23 t = ?size23RHS
data Digit : Nat -> Nat -> Type -> Type where
One : Lazy (Tree23 d s a) -> Digit d s a
Two : Lazy (Tree23 d s1 a) -> Lazy (Tree23 d s2 a) -> Digit d (s1+s2) a
Three : Lazy (Tree23 d s1 a) -> Lazy (Tree23 d s2 a) ->
Lazy (Tree23 d s3 a) -> Digit d (s1+s2+s3) a
Four : Lazy (Tree23 d s1 a) -> Lazy (Tree23 d s2 a) ->
Lazy (Tree23 d s3 a) -> Lazy (Tree23 d s4 a) -> Digit d (s1+s2+s3+s4) a
sizeDig : Digit d s a -> Nat
sizeDig t = ?sizeDigRHS
data FingerTree : Nat -> Nat -> Type -> Type where
Empty : FingerTree d 0 a
Single : Tree23 d s a -> FingerTree d s a
Deep : Digit d spr a -> Lazy (FingerTree (S d) sm a) -> Digit d ssf a ->
FingerTree d (spr + sm + ssf) a
data Seq' : Nat -> Type -> Type where
MkSeq' : FingerTree 0 n a -> Seq' n a
Seq : Type -> Type
Seq a = (n ** Seq' n a)
---------- Proofs ----------
try.sizeDigRHS = proof
intros
exact s
try.size23RHS = proof
intros
exact s
Редактировать
Другой вариант, который я немного изучил, - это попытаться отделить структуру данных от ее достоверности. Это приводит к следующему:
data Tree23 : Nat -> Type -> Type where
Elem : a -> Tree23 0 a
Node2 : Nat -> Lazy (Tree23 d a) -> Lazy (Tree23 d a) ->
Tree23 (S d) a
Node3 : Nat -> Lazy (Tree23 d a) -> Lazy (Tree23 d a) -> Lazy (Tree23 d a) ->
Tree23 (S d) a
size23 : Tree23 d a -> Nat
size23 (Elem x) = 1
size23 (Node2 s _ _) = s
size23 (Node3 s _ _ _) = s
data Valid23 : Tree23 d a -> Type where
ElemValid : Valid23 (Elem x)
Node2Valid : Valid23 x -> Valid23 y -> Valid23 (Node2 (size23 x + size23 y) x y)
Node3Valid : Valid23 x -> Valid23 y -> Valid23 z
-> Valid23 (Node3 (size23 x + size23 y + size23 z) x y z)
data Digit : Nat -> Type -> Type where
One : Lazy (Tree23 d a) -> Digit d a
Two : Lazy (Tree23 d a) -> Lazy (Tree23 d a) -> Digit d a
Three : Lazy (Tree23 d a) -> Lazy (Tree23 d a) ->
Lazy (Tree23 d a) -> Digit d a
Four : Lazy (Tree23 d a) -> Lazy (Tree23 d a) ->
Lazy (Tree23 d a) -> Lazy (Tree23 d a) -> Digit d a
data ValidDig : Digit d a -> Type where
OneValid : Valid23 x -> ValidDig (One x)
TwoValid : Valid23 x -> Valid23 y -> ValidDig (Two x y)
ThreeValid : Valid23 x -> Valid23 y -> Valid23 z -> ValidDig (Three x y z)
FourValid : Valid23 x -> Valid23 y -> Valid23 z -> Valid23 w -> ValidDig (Four x y z w)
sizeDig : Digit d a -> Nat
sizeDig (One x) = size23 x
sizeDig (Two x y) = size23 x + size23 y
sizeDig (Three x y z) = size23 x + size23 y + size23 z
sizeDig (Four x y z w) = (size23 x + size23 y) + (size23 z + size23 w)
data FingerTree : Nat -> Type -> Type where
Empty : FingerTree d a
Single : Tree23 d a -> FingerTree d a
Deep : Nat -> Digit d a -> Lazy (FingerTree (S d) a) -> Digit d a ->
FingerTree d a
sizeFT : FingerTree d a -> Nat
sizeFT Empty = 0
sizeFT (Single x) = size23 x
sizeFT (Deep k x y z) = k
data ValidFT : FingerTree d a -> Type where
ValidEmpty : ValidFT Empty
ValidSingle : Valid23 x -> ValidFT (Single x)
ValidDeep : ValidDig pr -> ValidFT m -> ValidDig sf ->
ValidFT (Deep (sizeDig pr + sizeFT m + sizeDig sf) pr m sf)
record Seq : Type -> Type where
MkSeq : FingerTree 0 a -> Seq a
data ValidSeq : Seq a -> Type where
MkValidSeq : ValidFT t -> ValidSeq (MkSeq t)
Затем каждая функция сопровождается (отдельным) доказательством ее справедливости.
Мне нравится, как этот подход отделяет код от доказательств, но я столкнулся с парой проблем:
В то время как код становится проще, доказательства, кажется, становится все труднее строить. Я полагаю, что большая часть этого, вероятно, связана с тем, что я не знаком с системой.
На самом деле я еще не подошел к моменту, когда я напишу этот код, но все функции индексации, разделения и архивирования должны будут настаивать на получении доказательства действительности своих входных данных. . Кажется немного странным, что одни функции работают только с последовательностями, а другие настаивают на доказательствах, но, возможно, это только я.
