Продвижение типа данных для зависимых - PullRequest
Новая
       37

Продвижение типа данных для зависимых

36 голосов
/ 22 декабря 2011

После прочтения ghc 7.4.перед выпуском заметок и бумагой Giving Haskell 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

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

Ответы [ 2 ]

8 голосов
/ 22 декабря 2011

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

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

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

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

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

head :: List a -> a

это 

head :: NotEmptyList a -> a

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

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

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

2 голосов
/ 22 декабря 2011

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

...