问题

为什么在 Haskell（以及FP通用）中，像 Maybe 这样的函子被定义为

data Maybe a = Nothing | Just a

而不是简单地

data Maybe a = Nothing | a

第二个选项仍然可以是函子，因为 Maybe 函子将类型 a 映射到类型 Nothing + a。我漏掉了什么？

data Maybe a = Nothing | Just a

data Maybe a = Nothing | a

答案1

得分: 13

这被称为“非歧视性联合”，与“歧视性联合”相对立 - Just 是“鉴别器”的事物。一些编程语言中有它们，例如 TypeScript。

但它们也带来了自己的困难。考虑类型推断：如果我写 let x = "foo"，x 的类型是什么？是 String 还是 Maybe String？

不过，最终这只是语言设计者所做的选择。在实践中，歧视性联合通常比非歧视性联合更有用，因此 Haskell 采用了它们。

答案2

得分: 5

一个data定义的右侧必须定义数据构造函数。一个单独的a只是一个类型变量。

data Maybe a = Nothing | Just a

Nothing是一个无参数的数据构造函数，其类型为Maybe a。Just是一个带有一个参数的数据构造函数，其类型为a -> Maybe a。与函数类似，它接受类型为a的参数，生成类型为Maybe a的值。（与函数不同，您可以将其用于模式匹配。）

> :t Nothing
Nothing :: Maybe a
> :t Just
Just :: a -> Maybe a
> :t Just 'c'
Just 'c' :: Maybe Char
> :t Just 3
Just 3 :: Num a => Maybe a

data Maybe a = Nothing | Just a

   > :t Nothing
   Nothing :: Maybe a
   > :t Just
   Just :: a -> Maybe a
   > :t Just 'c'
   Just 'c' :: Maybe Char
   > :t Just 3
   Just 3 :: Num a => Maybe a

答案3

得分: 5

让我们从一些基本的东西开始：你可以对 Maybe a 进行模式匹配。这意味着 在运行时，求值器需要能够查看内存中的 Maybe a 类型的值，并确定在以下代码中应该选择哪个分支：

case (mx :: Maybe a) of
  Nothing -> ...
  Just x -> ...

求值器需要能够在不知道类型 a 的情况下做出这种区分。因此，在内存中表示 mx :: Maybe a 的结构必须包含足够的信息来进行这种区分。Nothing 很容易，因为它只是一个常量，不包含其他值，所以它可以是一个已知的固定值；举例来说，我们决定它应该是一个所有位都是 0 的机器字。然后，当模式匹配查看 mx 时，如果找到一个全零字，我们就选择 Nothing 分支，如果找到非零的值，我们就选择 Just 分支。简单明了，对吗？

为了使这个工作，我们假设 Just x 值与 Nothing 值不同，无论 x 是什么。但这必须在不知道类型 a 的情况下工作，所以 x 可以是任何类型的任何值，而我们无法控制这些值在内存中的表示方式。如果我们只是将我们的 Just x 值表示为 x 的内存结构而没有其他包装，那么每当 x 的表示恰好是（或以）全零字开始时，我们就会认为我们有 Nothing，而实际情况并非如此。

特别是类型 a 可能是 Maybe b，这意味着我们的 Just x 可能是 Just Nothing；内部的值 可能是 Nothing，因此根据定义，有一些 x 值具有与 Nothing 相同的内存表示。但嵌套的 Maybe 并不是唯一可能出现内存表示冲突的情况，所以不要认为这只是一个晦涩的问题；False 也是一个空构造，没有理由分配与 Nothing 相同的位模式的算法不会分配给它；对于 LT :: Ordering 或 任何 枚举类型的第一个值可能也是同样的情况。原始数值和字符类型也没有避免这特定位模式的理由（无论它是全零还是我们选择其他值）。

你只有两种方法可以使这个工作。

一种是放弃 Maybe 类型作为一个像其他 ADT 一样工作的组合类型的想法。相反，你将它作为一种特殊情况，其中每种类型都有一个“可空”版本，但它不会嵌套。通过使用一些 全局 可识别的东西（比如空指针）来表示空情况，而不是使用所有其他值都使用的内存布局来表示。这是一些改进“null 安全性”的命令式语言采取的方法，但这不是 Haskell 采取的方法。Maybe 是一个完全普通的 ADT，不需要嵌入到编译器中，它可以嵌套和组合，不会对学习者强加任何额外的必须记住的规则。

第二种方法是不尝试用与 x 相同的内存结构表示 Just x。必须有一个用于 Just 数据构造函数本身的内存记录，至少有一个位用于区分它与 Nothing，并且有空间可以 包含 x（而不仅仅是 成为 x）。现在我们可以依赖于区分 Nothing 和 Just，一旦我们知道我们得到了 Just，我们就知道无论类型如何，我们都可以在哪里查找 x 部分。这就是 Haskell 所做的。

（有第三种可以想象的策略，那就是放弃独立决定类型表示的策略。语言实现将不得不安排一个全局注册表，以便无论涉及的类型如何，永远不会有两个值由相同的内存结构表示；实际上跟踪全程序中所有模块的全局“已分配”的位模式。但即使你可以实现它，这条规则 本身 也指示我们不能让 Just x :: Maybe a 与 x :: a 表示相同，因此它仍然需要一个包装器来包裹 x）。

所以基本上 Just 构造函数将存在于运行时系统中。在你可以避免它之前，你必须对 Haskell 的工作方式进行相当大的更改。即使定义 Maybe 的语言语法允许 data Maybe a = Nothing | a，第二种情况仍然会有一个包装构造函数存在，只是我们在表面语法中没有为它命名。

鉴于它必须存在于语言以使其按预期工作，将数据构造函数始终具有显式名称 实际上极大地简化了语言的语法。例如，在模式匹配中，编译器可以通过查看构造函数来判断程序员打算匹配哪个。否则，在这段代码中，你怎么知道哪个 Nothing 分支是哪个：

-- 你提议的语法
case (mmx :: Maybe (Maybe Int)) of


<details>
<summary>英文:</summary>

Let&#39;s start from something fundamental: you can pattern match on a `Maybe a`. That means that **at runtime** the evaluator needs to be able to look at a value of type `Maybe a` in memory and tell which branch to take in the following code:

case (mx :: Maybe a) of
Nothing -> ...
Just x -> ...

And the evaluator needs to be able to make that distinction without knowing anything about the type `a`. So at runtime the structure in memory that represents `mx :: Maybe a` has to have enough information in it to make this distinction. `Nothing` is easy, since it's just a constant and contains no other values, so it can just be a known fixed thing; for example's sake let's say we decide it should be a machine word with all 0 bits. Then when pattern matching is looking at `mx` if it finds an all-zero word we take the `Nothing` branch and if we find something non-zero we take the `Just` branch. Easy, right?

For that to work we've assumed that a `Just x` value will be different from the `Nothing` value **no matter what `x` is**. But this has to work without knowing the type `a`, so `x` could be any value of any type, and we have no way to control how those are represented in memory. If we just represent our `Just x` value as the memory structure for `x` with no additional wrapping, then any time the representation for `x` happens to be (or start with) an all-zero word we'll think we had `Nothing` when that's actually not the case.

In particular the type `a` could be `Maybe b`, which means our `Just x` could be `Just Nothing`; the value inside **could be** `Nothing` so automatically by definition there are some `x` values that have the same representation in memory as `Nothing`. But nested maybes are by no means the only case where the nested value might have a memory representation that collides with that of `Nothing`, so don't think it's just this one obscure case that's a problem; `False` is also an empty constructor and there's no reason the algorithms assigning memory representations wouldn't assign it the same bit pattern as `Nothing`; the same probably goes for `LT :: Ordering`, or the first value of *any* enum type. There's no reason primitive number and character types would avoid that specific bit pattern either (whether it's all-zero or we pick something else).

There are only 2 ways you can make this work, really.

One is to give up on the `Maybe` type being a compositional type that works like every other ADT. Instead you make it a special case thing where every type has a "nullable" version, but it doesn't nest. And you represent the null case by something *globally* identifiable (like a null pointer) rather than using memory layout used by all other values. This is the approach taken by a number of imperative languages that have approached this from the direction of improving "null safety", but it's not the approach Haskell takes. `Maybe` is a perfectly ordinary ADT that doesn't need to be baked into the compiler, it is nestable and compositional, doesn't impose any extra rules that have to be memorised by learners.

The second is to not try to represent `Just x` with the same memory structure as `x`. There needs to be a memory record for the `Just` data constructor itself, with at least one bit distinguishing it from `Nothing`, and room for it to **contain** `x` (rather than simply *being* `x`). Now we can rely on being able to distinguish `Nothing` from `Just`, and once we know we've got a `Just` we know where to look for the `x` part regardless of what type it is. This is what Haskell does.

(There is a third imaginable strategy, which is to give up on the representations of types being decided independently. The language implementation would instead have to arrange for some global registry so that no two values are ever represented by the same structure in memory, regardless of the types involved; effectively keeping track of which bit patterns are "already assigned" globally across all modules in the program. But even if you could implement it, that rule *itself* dictates that we can't have `Just x :: Maybe a` represented the same as `x :: a`, so it still requires a wrapper around the `x`).

---

So basically the `Just` constructor is going to exist in the runtime system. You have to make quite dramatic changes to how Haskell works before you can avoid that. Even if the language syntax for defining `Maybe` allowed `data Maybe a = Nothing | a`, the second case would still have a wrapper constructor there, we just wouldn't have a name for it in the surface syntax.

And given that it has to be there for the language to work the way it does, it **dramatically** simplifies the syntax of the language to always have an explicit name for the data constructor, even when it only contains one value. For example, in a pattern match, the compiler can tell what the programmer intended to match by looking at the constructors. Otherwise how do you tell which `Nothing` branch is which in this code:

-- Your proposed syntax
case (mmx :: Maybe (Maybe Int)) of
Nothing -> ...
Nothing -> ...
x -> ...

-- Standard Haskell sytax
case (mmx :: Maybe (Maybe Int)) of
Nothing -> ...
Just Nothing -> ...
Just (Just x) -> ...

For that matter how do I know that final `x` branch is supposed intended to be matching the `Int` that might be contained in the nested maybe? It's a bare variable, so it's a valid pattern at any of the levels? If I saw that pattern match without the explicit `Maybe (Maybe Int)` type annotation, how would I even know how many levels there are supposed to be? The `x` could just as validly be matching the `Int` contained in a `Maybe (Maybe (Maybe (Maybe (Maybe Int))))` (with all the other levels of `Nothing` being left to error out as failed pattern matches).

And if a bare value without an explicit constructor is a valid option for a normal data declaration for `Maybe`, it would have to be for any other type. A number of packages define a type that looks something like `data Result a = OK a | Error String`; why wouldn't they be defined as `data Result = a | String`? Now if I pass a value `"hello"` to a function that requires a `Result a`, am I giving it the error case? Or am I giving it the success case when `a` is `String`? Or am I giving it the success case when `a` is `Maybe (Identity (SomeOtherTypeWithABareStringCase))`? They would all look the same.

Or even worse, why shouldn't `data Either a b = Left a | Right b` be written as `data Either a b = a | b`? Now **any expression** could be interpreted as any path through any number of nestings of `Either`. It would be impossible for anyone (or the compiler) to tell anything about the type of any code by looking at it.

Obviously nobody would design the language allowing all of my dumb examples above. Either there would be a lot of extra restrictions on when you could use this feature, or there would be extra syntactic markers added to disambiguate all of the difficult cases (or both).

But remember again that the constructors still need to really exist in the system at runtime. So this feature of not having to write `Just` doesn't gain the system any *capabilities*. It **only** saves us a few key-presses writing the code. And in return we either have to *lose* capabilities (if the compiler restricts us to avoiding situations that would create an impossible ambiguous mess), or we have to write markers all over the place (which is basically equivalent to going back to explicit constructors anyway).

The closest I can see working is for this to only be allowed for a few built in types (not syntax that can be used in user-defined types), and add some special rules for those types to disambiguate common cases. Basically a somewhat less restricted version of the "nullable types" idea, so that a `Maybe a` is still a "normal" enough type to allow instances of user-defined classes and such, even though `Maybe a` wouldn't be definable by users.

But I don't want that. Haskell's beauty and power comes from having simple and consistent building blocks that are designed to be compositional. I don't *want* weird special cases to save a few key-presses. An ADT is a set of constructors, each of which has a list of fields. You build or pattern match values of an ADT by writing the constructor names. That fundamental language feature already works to cover all of the functionality gained by a nullable type feature so we don't need such a feature at all. Just a perfectly ordinary ADT called `Maybe`.

(I **do** want to save a few key-presses because Haskellers are just as lazy as programmers in any other language! But I want to do so via a feature that can work generally across the whole language, not a special-case hack just for `Maybe`. If you can't make this "bare value with no constructor" work as a general feature of ADTs I don't want it at all.)

</details>



# 答案4
**得分**: 1

&gt; 我漏掉了什么？

那个&lt;code&gt;&lt;i&gt;x&lt;/i&gt; | &lt;i&gt;y&lt;/i&gt;&lt;/code&gt;不是一种类型。

它只是`data`定义中的简写语法的一部分。你可以用GADT语法写出完整的定义，而不使用它。

垂直线旨在说明有效值的语法，就像在BNF中一样，以及它们的类型规则：

- 对于任何`a :: Type`，如果`n = Nothing`，则`n :: Maybe a`

- 对于任何`a :: Type`，如果`j = Just x`，且`x :: a`，则`j :: Maybe a`

类型系统对看似微小的更改非常敏感。如果你将`data Maybe a = Nothing | a`解释为与上述相同，它会说：

- 对于任何`a :: Type`，如果`x :: a`，则`x :: Maybe a`

这将极大地改变意义：

- 每种类型`t`都是`Maybe t`的_子类型_
- `|`表示_未标记_联合（上界/合并）
- `Maybe (Maybe t)`等同于`Maybe t`（并集是幂等的）
- `Maybe t`意味着“_可空_的`t`”

<details>
<summary>英文:</summary>

&gt; What am I missing?

That &lt;code&gt;&lt;i&gt;x&lt;/i&gt; | &lt;i&gt;y&lt;/i&gt;&lt;/code&gt; isn’t a type.

It’s just part of the short syntax of `data` definitions. You can write out the full definition in GADT syntax without it.

data Maybe a = Nothing | Just a

data Maybe (a0 :: Type) :: Type where
Nothing :: forall (a1 :: Type). Maybe a1
Just :: forall (a2 :: Type). a2 -> Maybe a2

The vertical bar is meant to illustrate the syntax of valid values, like in BNF, and their typing rules:

* For any `a :: Type`, if `n = Nothing`, then `n :: Maybe a`

* For any `a :: Type`, if `j = Just x`, and `x :: a`, then `j :: Maybe a`

Type systems are extremely sensitive to seemingly small changes. If you interpret `data Maybe a = Nothing | a` in the same way as above, it says:

* For any `a :: Type`, if `x :: a`, then `x :: Maybe a`

And that would drastically change the meaning:

* Every type `t` is a _subtype_ of `Maybe t`
* `|` denotes _untagged_ union (upper bound / join)
* `Maybe (Maybe t)` is _equivalent_ to `Maybe t` (union is idempotent)
* `Maybe t` means “_nullable_ `t`”


</details>