Haskell中Nothing的类型是什么？答案

【问题标题】：What is the type of Nothing in Haskell?Haskell中Nothing的类型是什么？
【发布时间】：2014-02-27 10:16:13
【问题描述】：

我在“Learn You a Haskell for Great Good!”一书的118 页上！

上面写着：

ghci> :t Nothing 
Nothing :: Maybe a

这是我的问题：

如果我理解正确，Nothing 是一个值，只有具体类型可以有值，但Maybe a 不是具体类型。那怎么会有Nothing这个值呢？

书上还说：

注意 Nothing 的类型是 Maybe a。它的类型是多态的。

多态类型是什么意思？我该如何理解这一点？这与只有具体类型才能有值的规则不矛盾吗？

编辑：

来自本书的PDF版本：

如果一个类型不带任何类型参数，我们就说它是具体的完全没有（如 Int 或 Bool），或者如果它采用类型参数并且它们是都填满了（比如Maybe Char）。如果你有一些价值，它的类型是总是一个具体的类型。

【问题讨论】：

很有趣的问题。 Nothing 不是值，而是构造函数。构造函数是一个函数（嗯，不完全是），它是 certain 类型的值。
函数是某种类型的值？我该如何理解这一点？您能否更详细地解释一下您的意思？
Maybe 不是具体类型，不能有值。 Maybe a 是任何 a 的具体类型。 Nothing 是任何 a 的 Maybe a 的值。
本书将“具体类型”定义为“完全应用的类型构造函数”，或者更正式地说，类型为*。这似乎是造成所有混乱的原因。根据本书的定义，Maybe a 是具体的，而单独的Maybe 不是。所以Nothing 是Maybe a 类型绝对没有问题。话虽这么说，“具体”绝不是一个官方术语，每个人都以不同的方式使用它。
这有点微妙，在这方面我远不是最有知识的人，但我相信在 Haskell 底层语言（lambda 演算的一种变体）中，Nothing 是真的是/\a. Maybe a 类型，这意味着如果你给它一个具体类型a 你会得到一个具体类型Maybe a 的值。但是，a 类型的这种传递在 Haskell 中是隐含的。

标签： haskell types

【解决方案1】：

这并不矛盾。 Nothing 是一个值，它的具体类型可以是Maybe a 的任何可能的实例化。

否则，Maybe a 类型的值继续具有具体类型 Maybe Int、Maybe String、Maybe Whatever，特别是 Nothing 可以由它们中的每一个键入，具体取决于上下文.这是因为它的构造函数（又称为Nothing :: Maybe a）不带任何参数，因此可以按原样调用它以生成Maybe a 类型的值。如果您愿意，我们将为每种具体类型提供一个。

如果没有上下文，ghci 当然会给你它可以推断出Nothing 的最一般的类型，即Maybe a，但它不是它的具体类型。这将取决于您将在 Nothing 中使用的各个表达式。例如：

ghci> Nothing
Nothing
it :: Maybe a

这可能是您键入的内容，或者类似的内容。没有进一步的上下文，因此Nothing 不会被输入具体类型。

ghci> Nothing :: Maybe Int
Nothing
it :: Maybe Int

这里我强制它采用具体类型Maybe Int。

ghci> 1 + fromMaybe 2 Nothing
3
it :: Integer

如果我将它与整数之和混合（fromMaybe :: a -> Maybe a -> a 采用默认值和 Maybe a 并返回 Just 中的值或带有 Nothing 的默认值），那么 Nothing 将得到由系统键入为Maybe Integer，因为您希望从中提取一个整数。没有，所以在这种情况下，我们将 1 与默认值 2 相加。

ghci> 1 + fromMaybe 2 (Nothing :: Maybe Integer)
3
it :: Integer

这里也一样，请仔细检查。我们强制 Nothing 在同一个表达式中使用我们之前假设的具体类型。

ghci> 1 + fromMaybe 2 (Nothing :: Maybe Char)

<interactive>:1:15:
    No instance for (Num Char)
      arising from the literal `2'
    Possible fix: add an instance declaration for (Num Char)
    In the first argument of `fromMaybe', namely `2'
    In the second argument of `(+)', namely
      `fromMaybe 2 (Nothing :: Maybe Char)'
    In the expression: 1 + fromMaybe 2 (Nothing :: Maybe Char)

三重检查，如果我们强制它假设另一个具体类型，你会看到它的值将完全不同，从而导致类型错误（与 C 不同，在 Haskell 中 Char 不充当数字） .

【讨论】：

GHCI 说 Nothing 的类型是 Maybe a，但什么是 Maybe a ？
根据 user3974，Nothing 不是值，而是构造函数……嗯。
那么Nothing本身就没有具体的类型吗？那么Nothing有什么样的类型呢？这些类型怎么称呼？
...多态 :) 就像Just :: a -> Maybe a 是一个多态构造函数。
我认为“具体”这个词有些疑问。我经常看到“concrete”这个词用来表示“ground type”，即 Kind * 的类型。从这个意义上说，“Maybe a”是完全具体的——它是一种地面类型，只是多态的。在这里，您使用具体来表示单态。我认为 OP 的部分困惑是“具体”一词的这两种不相关的含义。来自 LYAH 的 OP 引用的摘录在“有种类 *”的意义上使用了“具体”。

【解决方案2】：

这与只有具体类型可以有值的规则不矛盾吗？

由于函数是 Haskell 中的一等值，因此这条所谓的规则意味着诸如 map 和 foldr 之类的多态函数将无法实现。

Haskell中其实有很多多态的非函数值，比如

1 :: Num a => a
Nothing :: Maybe a
[] :: [a]
Left 1 :: Num a => Either a b

等等。这些值存在于a（和b）的每个实例化中。

【讨论】：

那么结论是不仅具体类型可以有值吗？所以这本书的陈述（请参阅编辑）是不正确的？所以'Maybe a'是一种多态类型（即不是具体类型），那么我理解正确吗？ “多态类型”是表示“也许是”等概念的正确术语吗？
@jhegedus 看起来这本书指的是完全应用的具体含义。 forall a. Maybe a 是一个完全应用的类型，它绝对可以有值。 Maybe 不是，所以没有价值 v :: Maybe
所以结论是 Nothing 的类型是 Maybe a ?
@jhegedus：是的（正如 GHC 所说）。

【解决方案3】：

从某种意义上说，你是对的。没有forall a.Maybe a 类型的值。您构造的每个 Maybe 值实际上都有一些确定的类型 Maybe tau，其中 tau 可能已知或未知，但它是一些确定的类型。

符号Nothing :: forall a.Maybe a 只是告诉我们，每当我们使用表达式Nothing 时，它将构造一个预期的Maybe 类型的值。

【讨论】：

forall a.Maybe a 是什么？我只在 Haskell 书的第 118 页，所以很遗憾我不是 Haskell 专家。
@jhegedus 我在上面告诉过你：在这种情况下，它的意思是“无论你想要什么具体的 Maybe 类型，这都会适合你”。或者，更正式地说：对于所有你想要的，Nothing 会给你Maybe a。也就是说，如果你想要一个Maybe String，Nothing 会给你一个Maybe String。 Int 或其他的也是如此。
当然，多态类型是有值的。 Nothing 是 forall a. Maybe a 类型的值，就像 \ x -> x 是 forall a. a -> a 类型的值一样。
@kosmikus 好吧，我建议你给我看一些代码，其中一个表达式 Nothing 据称用于 forall a 类型。也许是 a，我会告诉你那个 Nothing 的真实类型，并且它不会是forall a。也许是一个
@Ingo ... 或const False Nothing

【解决方案4】：

Maybe 类型有两个构造函数：Nothing 和 Just a，其中 a 是类型变量。没有什么本身不能确定（约束）类型，但在任何合理的上下文中你会发现类似的东西（我不声称它在语法上是正确的 Haskell，但我会在 10 年前写的东西）：

if (foo == 5)
then Nothing
else Just 5

然后类型推断会告诉你（假设 5 是这段代码 sn-p 'foo' 类型为 Int 的参数）foo 具有类型：

foo :: Int -> Maybe Int

但正如之前的海报所指出的，Maybe a 是一个非常好的类型。您会发现与 [] 相同的非问题，即具有 [] 的列表类型（空列表的构造函数）。

【讨论】：

【解决方案5】：

This 26:00 的谈话回答了这个问题：“[ ] 的类型是什么？”这是与“Nothing 的类型是什么？”相关的问题。

Hudak 的书中也有一段很好的说明：

【讨论】：