Слабые ограничения типа GADT для работы с непредсказуемыми данными - PullRequest
Новая
       11

Слабые ограничения типа GADT для работы с непредсказуемыми данными

0 голосов
/ 23 декабря 2018

Я пытаюсь использовать GADT, чтобы иметь хорошо ограниченные типы, но некоторые зависимости невозможно обработать во время компиляции - например, пользовательский ввод.Давайте рассмотрим следующее определение дерева AVL: 

data Zero
data S a

data AVL depth where
  Nil :: AVL Zero
  LNode :: AVL n -> Int -> AVL (S n) -> AVL (S (S n))
  RNode :: AVL (S n) -> Int -> AVL n -> AVL (S (S n))
  MNode :: AVL n -> Int -> AVL n -> AVL (S n)

Магия GADT гарантирует, что каждое дерево AVL хорошо сбалансировано.Я могу определить некоторые базовые функции, такие как 

singleton :: a -> AVL (S Zero) x
singleton a = MNode Nil a Nil

insert :: a -> AVL n a -> AVL (S n) a
insert = ...

Теперь я хотел бы написать программу, которая будет читать n числа, вставлять их в дерево AVL и возвращать по порядку (при условии, что эти функции определены): 

main = IO ()
main = do
  (n :: Int) <- readInt  -- some IO defined somewhere
  (inp :: [Int]) <- readInts
  let avl = foldl (\tree x -> insert x tree) Nil inp
  print $ toList avl

И, очевидно, я получаю ошибку: 

    • Couldn't match type ‘S Zero’ with ‘Zero’
      Expected type: AVL Zero
        Actual type: AVL (S Zero)

, поскольку тип (глубина) дерева будет меняться вместе с каждым insert.Я понимаю, что здесь происходит, но я не вижу разумного способа использовать этот AVL при обработке ввода «онлайн», то есть без какого-либо знания о том, сколько элементов я собираюсь вставить.

Есть ли какое-либо решение, которое позволило бы мне абстрагировать глубину дерева для этого случая?Даже если AVL является слишком сложным примером, эта проблема применима также к векторам и матрицам размера компиляции.Пока я могу решать только жестко заданные задачи, что делает мои программы совершенно негибкими.

1 Ответ

0 голосов
/ 23 декабря 2018

Вы можете использовать другой GADT, чтобы скрыть глубину дерева.(Это называется экзистенциальным типом.) 

data SomeAVL a where
  SomeAVL :: AVL n a -> SomeAVL a

С упаковщиками для работы на SomeAVL s: 

insert' :: a -> SomeAVL a -> SomeAVL a
insert' a (SomeAVL t) = SomeAVL (insert a t)
...