什么是约束实物签名

Question

如果我检查kind的Maybe,我得到这样的:

?> :k Maybe
Maybe :: * -> *

现在,如果我检查一下,Monad我得到这个:

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

有什么Constraint需要以及为什么需要它？为什么不* -> *呢？

Answer 1

不像Maybe,Monad不是一种类型 ; 它是一个类型类.

其他类型类也是如此:

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

Where *表示具体类型(例如Boolor Int),->表示更高级的类型(例如Maybe),并Constraint表示类型约束的概念.这就是为什么:

我们知道我们不能像这样签名:

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

因为Monad应该用作约束,要说'这必须是一个单独的工作':

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

我们这样做是因为我们知道它return不能用于任何旧类型m,所以我们return在名称下定义不同类型的行为Monad.换句话说,没有一件事可以被称为Monad,但只有一种行为可以被称为Monadic.

出于这个原因,我们已经创建了这种类型约束,说我们必须预先定义一些东西作为Monad来使用这个函数.这就是为什么样的Monad是(* -> *) -> Constraint-它本身不是一个类型!

Maybe是一个实例Monad.这意味着在某个地方,有人写道:

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

......并定义了Maybe应该如何表现为Monad.这就是我们可以使用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