Прочитав 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. Введение" говорит: "Например, мы могли бы обеспечить [во время компиляции], чтобы предполагаемое красно-черное дерево действительно обладало красно-черным свойством".
"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.
Nat может быть, например, используется для построения числовых векторов, которые могут быть добавлены только в том случае, если они имеют одинаковую длину, проверенные в время компиляции.