Haskell中的部分应用类型 [英] Partially Applied Types in Haskell

问题描述

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

  data Promise ab = Pending（a  - > b）|已解决b | Broken 
 
实例Functor（Promise x）其中
 fmap f（Pending g）= Pending（f。g）
  

---

IF

  g :: a  - > b 
  

then

 待定g ::承诺ab 
  

还有

  f :: b  - > c 
  

因为存在 f。 g 。

表示

  Pending（f。g）:: Promise ac`。 
  

结束

  fmap ::（b  - > c） - >承诺b  - > Promise ac 
  

---

现在 fmap 单独拥有这个签名（适用于上述）

  fmap :: Functor f => （b→c）→> f b  - > fc 
  

如果您认为 f = Promise a 。虽然最终产品似乎是合理的，但您如何解释 f 的类型或等价地是部分应用的承诺的类型 Promise a 几乎 - 哈斯克尔 - 。特别是，您可以将类型视为具有构造函数并且可以部分应用。

为了更加严格地查看这个，我们引入类型的类型种。例如，类型构造函数 Int 具有类型

  Int ::: * 
  

其中我写（:::）阅读has kind，尽管这不是有效的Haskell语法。现在我们还有部分应用类型构造函数，比如

 也许::: *  - > * 
  

它的函数类型就像您期望的值级别一样。

---

类型的概念有一个非常重要的概念 - 只有类型 * 。或者，例如，不存在类型可能

  x ::也许
x =  -  ....什么！ 
  

事实上，甚至不可能表达除之外的其他类型的类型， * 我们期望该类型描述一个值的任何地方。

这会导致某种在Haskell中我们不能只是普遍地传递未应用的类型构造函数，因为它们并不总是很有意义。相反，整个系统的设计使得只有合理的类型才能被构造出来。

但是允许表达这些更高级别的类型的一个地方是类型类如果我们启用 KindSignatures ，那么我们可以编写这样的定义：

---

我们的类型直接。显示的一个地方是类定义。这是显示

  class Show（a :: *）其中
 show :: a  - >字符串
 ... 
  

这是非常自然的，因为<$ c

$ p> Show 方法的签名中的$ c> a 是有价值的。 >但是，正如你在这里指出的那样， Functor 是不同的。如果我们写出它的类型签名，我们可以看到为什么

  class Functor（f :: *  - > *）其中
 fmap ::（a  - > b） - > f a  - > fb 
  

这是一种非常新颖的多态性，高度多态的多态性，所以需要一分钟把你的头围绕在它周围。然而，需要注意的是， f 只出现在应用 Functor 的方法中到其他类型 a 和 b 。特别是像这样的类会被拒绝。

$ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ b nope :: f - >字符串

因为我们告诉系统 f 虽然它可以实例化值，就好像它是 * KindSignatures 。



---

因为Haskell可以直接推断签名。例如，我们可以（并且实际上）编写

  class Functor f其中
 fmap ::（a  - > b） - > f a  - > fb 
  

和Haskell推断出 f 必须是（* - > *），因为它看起来适用于 a 和 b 。同样，如果我们写了一些不一致的东西，我们可能会因为类型检查失败而导致类型检查失败。例如

  class NopeNope f其中
 fmap :: f  - > f a  - > a 
  

意味着 f 有kind * 和 （* - > *）不一致。

Based on this question, in this code

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

instance Functor (Promise x) where
    fmap f (Pending g) = Pending (f . g)

---

IF

g :: a -> b

then

Pending g :: Promise a b

also

f :: b -> c

because of the existence of f . g.

That means

Pending (f . g) :: Promise a c`.

Wrapping up

fmap :: (b -> c) -> Promise a b -> Promise a c

---

Now fmap alone has this signature (adapted to the above)

fmap :: Functor f => (b -> c) -> f b -> f c

This only conforms if you assume that f = Promise a. While the end product seems reasonable, how do you interpret the type of f or equivalently what it the type of a partially applied promise Promise a?

解决方案

At the type level you have another programming language, almost-Haskell. In particular, you can view types as having constructors and being able to be partially applied.

To view this a bit more rigorously, we introduce "types of types" called "kinds". For instance, the type constructor Int has kind

Int ::: *

where I write (:::) to read "has kind", though this isn't valid Haskell syntax. Now we also have "partially applied type constructors" like

Maybe ::: * -> *

which has a function type just like you'd expect at the value level.

---

There's one really important concept to the notion of kinds—values may instantiate types only if they are kind *. Or, for example, there exist no values of type Maybe

x :: Maybe
x = -- .... what!

In fact, it's not possible to even express a type of kind other than * anywhere where we'd expect that type to be describing a value.

This leads to a certain kind of restriction in the power of "type level functions" in Haskell in that we can't just universally pass around "unapplied type constructors" since they don't always make much sense. Instead, the whole system is designed such that only sensible types can ever be constructed.

But one place where these "higher kinded types" are allowed to be expressed is in typeclass definitions.

---

If we enable KindSignatures then we can write the kinds of our types directly. One place this shows up is in class definitions. Here's Show

class Show (a :: *) where
  show :: a -> String
  ...

This is totally natural as the occurrences of the type a in the signatures of the methods of Show are of values.

But of course, as you've noted here, Functor is different. If we write out its kind signature we see why

class Functor (f :: * -> *) where
  fmap :: (a -> b) -> f a -> f b

This is a really novel kind of polymorphism, higher-kinded polymorphism, so it takes a minute to get your head all the way around it. What's important to note however is that f only appears in the methods of Functor being applied to some other types a and b. In particular, a class like this would be rejected

class Nope (f :: * -> *) where
  nope :: f -> String

because we told the system that f has kind (* -> *) but we used it as though it could instantiate values, as though it were kind *.

---

Normally, we don't have to use KindSignatures because Haskell can infer the signatures directly. For instance, we could (and in fact do) write

class Functor f where
  fmap :: (a -> b) -> f a -> f b

and Haskell infers that the kind of f must be (* -> *) because it appears applied to a and b. Likewise, we can fail "kind checking" in the same was as we fail type checking if we write something inconsistent. For instance

class NopeNope f where
  fmap :: f -> f a -> a

implies that f has kind * and (* -> *) which is inconsistent.

这篇关于Haskell中的部分应用类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！