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

Я видел это '[] а также ': синтаксис в нескольких местах, особенно в гетерогенных списках пакетов, таких как 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 ответа

Решение

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"

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

Источник

Книга

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

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

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

Источник
Другие вопросы по тегам