Что такое «[] и»: в Хаскеле? - PullRequest
Новая
       40

Что такое «[] и»: в Хаскеле?

0 голосов
/ 03 января 2019

Я видел этот синтаксис '[] и ': в нескольких местах, особенно в пакетах разнородных списков, таких как HList или HVect .

Например, гетерогенный вектор HVect определяется как 

data HVect (ts :: [*]) where
    HNil :: HVect '[]
    (:&:) :: !t -> !(HVect ts) -> HVect (t ': ts)

В GHCi с расширением TemplateHaskell или DataKinds я получаю это 

> :t '[]
'[] :: template-haskell-2.13.0.0:Language.Haskell.TH.Syntax.Name
> :t '(:)
'(:) :: template-haskell-2.13.0.0:Language.Haskell.TH.Syntax.Name

У меня сложилось впечатлениечто это связано с зависимыми типами и видами и т. д., а не с шаблоном haskell.

Поисковые системы, а также hoogle и hayoo обрабатывают запросы с помощью'[] или ': довольно плохо, поэтому возникает вопрос: Как называются эти '[] и ': вещи? Указатели на документацию или учебные пособия были бы весьма желательны.

Ответы [ 2 ]

0 голосов
/ 04 января 2019

Книга

Мышление с типами Сэнди Магуайр (http://thinkingwithtypes.com)

может быть хорошим ресурсом по теме уровня типапрограммирование на Haskell в целом. Глава «Снятие ограничений» имеет дело с DataKinds и повышенными конструкторами.

(Отказ от ответственности: Нет присоединения.)

0 голосов
/ 03 января 2019

DataKinds позволяет использовать конструкторы уровня терминов на уровне типов.

После 

data T = A | B | C

можно писать типы, проиндексированные значением T

data U (t :: T) = ...
foo :: U A -> U B -> ...

Здесь, однако, A и B используются как типы, а не как значения.Следовательно, они должны быть "продвинуты", используя цитату: 

data U (t :: T) = ...
foo :: U 'A -> U 'B -> ...

То же самое происходит со знакомым синтаксисом списка.'[] - пустой список, повышенный на уровне типа.'[a,b,c] - это то же самое, что и a ': b ': c ': '[], список, продвигаемый на уровне типа. 

type           :: kind
'[]            :: [k]   -- polykinded! works for any kind k
'[ 'A, 'B, 'C] :: [T]   -- mind the spaces, we do not want the char '['
'A ': '[]      :: [T]
'[ Int, Bool ] :: [*]   -- a list of types
'[ Int ]       :: [*]   -- a list of types with only one element
[Int]          :: *     -- a type "list of Int"

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

...