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

Если я проверю kind из Maybe, я получу следующее:

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

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

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

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


person Sibi    schedule 08.04.2015    source источник


Ответы (2)


В отличие от 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.

person AJF    schedule 08.04.2015

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
person chi    schedule 08.04.2015