Повышение качества данных для зависимых лиц

Прочитав ghc 7.4. заметки перед выпуском и документ Предоставление Haskell a Promotion, я все еще смущен тем, что вы на самом деле делаете с продвинутыми типами. Например, в руководстве GHC приводятся следующие примеры продвинутых типов данных:

data Nat = Ze | Su Nat

data List a = Nil | Cons a (List a)

data Pair a b = Pair a b

data Sum a b = L a | R b

Какие виды использования имеют такие виды? Можете ли вы привести примеры (код)?

Ответы

Ответ 1

В самой статье есть как минимум два примера:

"1. Введение" говорит: "Например, мы могли бы обеспечить [во время компиляции], чтобы предполагаемое красно-черное дерево действительно обладало красно-черным свойством".

"2.1 Продвижение типов данных" обсуждает векторы с индексом длины (то есть векторы с ошибками "индекс за пределами границ" ).

Вы также можете взглянуть на более раннюю работу в этом направлении, например. HList для гетерогенных списков типов и расширяемых коллекций. Олег Киселев имеет много связанных работ. Вы также можете читать работы по программированию с зависимыми типами. http://www.seas.upenn.edu/~sweirich/ssgip/main.pdf содержит вводные примеры для вычислений на уровне типа в Agda, но они также могут применяться к Haskell.

Грубо говоря, идея состоит в том, что head для списков задан более точный тип. Вместо

head :: List a -> a

это

head :: NotEmptyList a -> a

Последняя функция главы более типична, чем fomer: она никогда не может быть применена к пустым спискам, потому что это вызовет ошибки компилятора.

Вам нужны вычисления на уровне типов для выражения типов, таких как NotEmptyList. Классы типов с функциональными зависимостями, семейства GAGT и (индексированные) уже предоставляют слабые формы вычислений на уровне типа для haskell. Работа, о которой вы упомянули, еще раз уточняет в этом направлении.

См. http://www.haskell.org/haskellwiki/Non-empty_list для реализации, используя только классы классов Haskell98.

Ответ 2

Nat может быть, например, используется для построения числовых векторов, которые могут быть добавлены только в том случае, если они имеют одинаковую длину, проверенные в время компиляции.