Добрые подписи - программирование

Я просматриваю книги Haskell wiki GADTS

https://en.wikibooks.org/wiki/Haskell/GADT.

Я хорошо отслеживал, пока не была добавлена подпись Kind, которая обобщает ограниченный тип конструктора Cons.

data Safe
data NotSafe

data MarkedList             ::  * -> * -> * where
  Nil                       ::  MarkedList t NotSafe
  Cons                      ::  a -> MarkedList a b -> MarkedList a c

safeHead                    ::  MarkedList a Safe -> a
safeHead (Cons x _)          =  x


silly 0                      =  Nil
silly 1                      =  Cons () Nil
silly n                      =  Cons () $ silly (n-1)

С помощью Подписи типа я могу использовать конструктор Cons для построения и сопоставления шаблонов как с безопасными, так и с небезопасными MarkedLists. Хотя я понимаю, что происходит, я, к сожалению, испытываю трудности с созданием какой-либо интуиции относительно того, как это допускает Kind Signature. Зачем нужна Подпись? Что такое подпись?

Ответ 1

Точно так же, как подпись типа работает для значений, подтипы типов работают для типов.

f :: Int -> Int -> Bool
f x y = x < y

Здесь f принимает два значения аргумента и выдает значение результата. Эквивалент для типов может быть:

data D a b = D a b

Тип D принимает два типа аргументов и создает тип результата (это * -> * -> *). Например, D Int String - это тип (который имеет вид *). Частичное приложение D Int имеет вид * -> *, точно так же, как частичное приложение f 15 имеет тип Int -> Bool.

Итак, мы могли бы переписать выше, как:

data D :: * -> * -> * where
  D :: a -> b -> D a b

В GHCi вы можете запрашивать типы и виды:

> :type f
f :: Int -> Int -> Bool
> :kind D
D :: * -> * -> *