Haskell中的部分应用类型

Cri*_*cia 4 haskell

基于这个问题,在此代码中

data Promise a b =  Pending (a -> b) | Resolved b | Broken

instance Functor (Promise x) where
    fmap f (Pending g) = Pending (f . g)
Run Code Online (Sandbox Code Playgroud)

如果

g :: a -> b
Run Code Online (Sandbox Code Playgroud)

然后

Pending g :: Promise a b
Run Code Online (Sandbox Code Playgroud)

f :: b -> c
Run Code Online (Sandbox Code Playgroud)

因为存在f . g.

这意味着

Pending (f . g) :: Promise a c`.
Run Code Online (Sandbox Code Playgroud)

包起来

fmap :: (b -> c) -> Promise a b -> Promise a c
Run Code Online (Sandbox Code Playgroud)

现在fmap单独有这个签名(适应上述)

fmap :: Functor f => (b -> c) -> f b -> f c
Run Code Online (Sandbox Code Playgroud)

这只有在你假设的情况下才符合f = Promise a.虽然最终产品看似合理,但您如何解释f部分应用承诺的类型或等效类型Promise a

J. *_*son 9

在类型级别,您有另一种编程语言,几乎是 -Haskell.特别是,您可以将类型视为具有构造函数并且可以部分应用.

为了更加严格地看待这一点,我们引入了"类型的类型",称为"种类".例如,类型构造函数Int有类型

Int ::: *
Run Code Online (Sandbox Code Playgroud)

我写的地方(:::)读"有点",虽然这不是有效的Haskell语法.现在我们也有"部分应用类型构造函数"之类的

Maybe ::: * -> *
Run Code Online (Sandbox Code Playgroud)

它的功能类型就像你期望的那样.


对于种类的概念,有一个非常重要的概念 - 值只有在它们是善良的情况下才可以实例化*.或者,例如,不存在类型的值Maybe

x :: Maybe
x = -- .... what!
Run Code Online (Sandbox Code Playgroud)

实际上,除了*我们期望该类型描述一个值的任何地方之外,甚至不可能表达一种类型.

这导致Haskell中"类型级函数"的力量受到某种限制,因为它们不能普遍地传递"未应用的类型构造函数",因为它们并不总是有意义.相反,整个系统的设计使得只能构造合理的类型.

但允许表达这些"更高级别的类型"的一个地方是类型定义.


如果我们启用KindSignatures那么我们可以直接编写我们的类型.这显示的一个地方是类定义.这里的Show

class Show (a :: *) where
  show :: a -> String
  ...
Run Code Online (Sandbox Code Playgroud)

这是完全自然的,因为a方法的签名中的类型的出现Show是有价值的.

但是,正如你在这里指出的那样,当然Functor是不同的.如果我们写出它的亲切签名,我们会明白为什么

class Functor (f :: * -> *) where
  fmap :: (a -> b) -> f a -> f b
Run Code Online (Sandbox Code Playgroud)

这是一种非常新颖的多态性,更高级的多态性,因此需要花一点时间才能完全掌控它.什么是重要的但必须注意的是,f只出现在方法Functor 被应用到其他类型的ab.特别是,这样的课程将被拒绝

class Nope (f :: * -> *) where
  nope :: f -> String
Run Code Online (Sandbox Code Playgroud)

因为我们告诉系统f有种类,(* -> *)但我们使用它就像它可以实例化值一样,好像它是善良的*.


通常,我们不必使用,KindSignatures因为Haskell可以直接推断签名.例如,我们可以(实际上)写

class Functor f where
  fmap :: (a -> b) -> f a -> f b
Run Code Online (Sandbox Code Playgroud)

和Haskell推断出那种f必须是(* -> *)因为它似乎适用于ab.同样地,如果我们写出一些不一致的东西,我们就会失败"类型检查".例如

class NopeNope f where
  fmap :: f -> f a -> a
Run Code Online (Sandbox Code Playgroud)

暗示f有种类* (* -> *)不一致.