Что такое ограничение в натуральной подписи

Question

Если я проверю kind из Maybe Я получаю это:

λ> :k Maybe
Maybe :: * -> *

Теперь, если я проверю вид Monad Я получаю это:

λ> :k Monad
Monad :: (* -> *) -> Constraint

Что такое Constraint там и зачем это нужно? Почему не только это * -> *?

Answer 1

В отличие от Maybe , Monad не тип; это класс типов.

То же самое относится и к другим классам типов:

Num :: * -> Constraint
Functor :: (* -> *) -> Constraint
Bifunctor :: (* -> * -> *) -> Constraint

куда * представляет конкретные типы (такие как Bool или же Int), -> представляют более родственные типы (такие как Maybe), а также Constraint представляет идею ограничения типа. Вот почему:

---

Как мы знаем, мы не можем сделать такую ​​подпись:

return :: a -> Monad a -- This is nonsense!

Так как Monad следует использовать в качестве ограничения, чтобы сказать, что "это должна быть монада для работы":

return :: (Monad m) => a -> m a

Мы делаем это, потому что мы знаем, что return не может работать на любом старом типе m поэтому мы определяем поведение return для разных типов под именем Monad, Другими словами, нет единственной вещи, которую можно назвать монадой, а есть только поведение, которое можно назвать монадической.

По этой причине мы создали это ограничение типа, сказав, что мы должны заранее определить что-то как монаду, чтобы использовать эту функцию. Вот почему вид Monad является (* -> *) -> Constraint - это само по себе не тип!

---

Maybe это пример Monad, Это означает, что где-то кто-то написал:

instance Monad Maybe where
  (>>=) = ... -- etc

... и определил как Maybe должен вести себя как монада. Вот почему мы можем использовать Maybe с функциями или типами, которые имеют ограничение префикса Monad m => ..., По сути, именно здесь определяется ограничение, применяемое Monad,

Answer 2

Constraint это, например, вид Show Int, Monad Maybe, а также Monoid [a], Грубо говоря, это вид всего, что может произойти на левой стороне => в аннотации типа.

Сейчас с

Show Int :: Constraint

а также Int это тип, т.е.

Int :: *

мы можем назначить функциональный вид Show следующее

Show :: * -> Constraint
             ^-- the result kind
        ^-- the kind of Int

В вашем случае просто так получается, что Monad принимает аргумент как Maybe, так

Maybe Int :: *
Maybe :: * -> *
Monad :: (* -> *) -> Constraint
                     ^-- the result kind
         ^-- the kind of Maybe