在函数式编程中,为什么Maybe函子没有定义为data Maybe a = Nothing | a?

5

我在想为什么在Haskell(和FP一般)中,像Maybe这样的函子被定义为

data Maybe a = Nothing | Just a

不要只是简单地

data Maybe a = Nothing | a

第二个选项仍然是函子的,因为 Maybe 函子将类型 a 映射到类型 Nothing + a。我错过了什么?

第二个选项不是有效的语法。 - sepp2k
3
aa有什么区别?(提示:其中一个是Maybe,你能分辨出哪个吗?) - cafce25
1
密切相关:为什么我们需要求和类型? - duplode
这个语法在 Haskell 中是无效的,但在“函数式编程普遍”中没有共同规则。你可以自由发明一种语言,在那样的语法下工作。 - n. m.
1
@duplode 为什么 Maybe/Optional 类型使用 Just/Some 类型而不是实际类型? 从那个问题中链接过来,看起来更相关。 - amalloy
@amalloy确实——这已经足够接近可以算作是重复了,不过到目前为止我喜欢这里给出的简短而甜美的答案。 - duplode
4个回答

13
这就是所谓的“非歧视性联合”,与“歧视性联合”相反 - Just 是“鉴别器”。 一些语言确实有它们 - 例如 TypeScript。
但它们带来了自己的难点。考虑类型推断:如果我写let x =“foo”,那么x的类型是什么?是String还是Maybe String
不过,最终,这只是语言设计者所做的选择。实际上,歧视性联合比非歧视性联合更有用,因此 Haskell 也有它们。

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

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只是其中一个嵌套值可能具有与Nothing冲突的内存表示的案例,并且不要认为它只是这个晦涩的案例有问题; False也是一个空的构造函数,算法分配内存表示形式不会给它分配与Nothing相同的位模式;对于LT :: Ordering或任何枚举类型的第一个值,情况也可能如此。原始数字和字符类型没有理由避免特定的位模式(无论是全零还是我们选择其他东西)。
实际上只有两种方法可以使其工作。

一种方法是放弃 Maybe 类型作为一个像其他任何 ADT 一样工作的组合类型。取而代之,使它成为每种类型都有一个“可为空”的版本的特殊情况,但它不嵌套。您可以通过一些全局可识别的方式(如空指针)来表示空值,而不是使用所有其他值使用的内存布局。这是一些从改进“空安全性”角度出发的命令式语言采用的方法,但这并不是 Haskell 采用的方法。 Maybe 是一个完全普通的 ADT,不需要被编译器嵌入,它是可嵌套和组合的,不会对学习者施加任何额外的规则。

第二个是不要试图用与x相同的内存结构来表示Just x。需要有一个内存记录来存储Just数据构造函数本身,至少有一位区分它和Nothing,并且有空间来包含x(而不仅仅是成为x)。现在我们可以依赖于能够区分NothingJust,一旦我们知道我们有了一个Just,无论它是什么类型,我们都知道在哪里寻找x部分。这就是Haskell所做的事情。

有第三种可能的策略,就是放弃类型表示独立决定。语言实现将需要安排一些全局注册表,以便无论涉及哪种类型,都不会通过相同的内存结构表示两个值;有效地跟踪已经在程序的所有模块中“分配”的位模式。但即使您可以实现它,该规则本身也说明我们不能将Just x :: Maybe a表示为与x :: a相同,因此仍需要在x周围包装。


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

鉴于它必须存在于语言中以使其正常工作,即使它只包含一个值,在语言的语法中始终具有数据构造器的显式名称也大大简化了语言的语法。例如,在模式匹配中,编译器可以通过查看构造器来判断程序员想要匹配的内容。否则,在以下代码中,你如何区分哪个Nothing分支是哪个:

-- 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) -> ...

就这个问题而言,我怎么知道最终的x分支应该匹配嵌套的Maybe中可能包含的Int?它是一个裸变量,所以在任何级别上都是有效的模式吗?如果我看到那个模式匹配没有明确的Maybe (Maybe Int)类型注释,我怎么知道应该有多少级别?x同样可以匹配Maybe (Maybe (Maybe (Maybe (Maybe Int))))中包含的Int(所有其他级别的Nothing都被留给错误的模式匹配失败)。

如果一个没有显式构造函数的裸值对于Maybe的普通数据声明是一个有效的选项,那么它也必须适用于任何其他类型。许多软件包定义了类似data Result a = OK a | Error String的类型; 为什么它们不能被定义为data Result = a | String呢?现在,如果我向需要Result a的函数传递一个"hello"值,我是给它错误情况吗?还是当aString时我给它成功的情况?或者当aMaybe(Identity(SomeOtherTypeWithABareStringCase))时我给了它成功的情况?它们看起来都一样。
或者更糟糕的是,为什么不应该将data Either a b = Left a | Right b写成data Either a b = a | b?现在,任何表达式都可以被解释为通过Either的任意嵌套路径。任何人(或编译器)通过查看代码都无法确定任何代码的类型。
很明显,没有人会设计一种语言允许我上面那些愚蠢的例子。要么在使用此功能时会有很多额外的限制,要么会添加额外的语法标记来消除所有困难的情况(或者两者都有)。
但是请记住,构造函数仍然需要在运行时真正存在于系统中。因此,不需要编写Just这样的特性并不为系统带来任何能力。它只是帮我们省下了一些编写代码的按键操作。而作为回报,我们要么必须丧失一些能力(如果编译器限制我们避免创建不可能的混乱歧义的情况),要么必须在各个地方写上标记(这基本上等同于重新回到显式构造函数的方式)。
我能看到的最接近可行的方法是只允许在一些内置类型中使用(不能在用户定义的类型中使用的语法),并对这些类型添加一些特殊规则以消除常见情况的歧义。基本上是“可为空类型”思想的一种略为限制较少的版本,这样Maybe a仍然是足够“常规”的类型,可以允许用户定义类的实例等,尽管用户无法定义Maybe a

但我不想要那个。Haskell的美和力量来自于具有简单和一致的构建块,这些构建块被设计成可组合的。我不希望为了节省几个按键而使用奇怪的特殊情况。ADT是一组构造函数,每个构造函数都有一个字段列表。通过编写构造函数名称,您可以构建或模式匹配ADT的值。这种基本语言功能已经可以覆盖由可空类型功能获得的所有功能,因此我们根本不需要这样的功能。只需要一个完全普通的ADT,称为Maybe

(我确实想要节省几个按键,因为Haskellers和其他任何语言的程序员一样懒!但我希望通过一个可以在整个语言中通用的功能来实现,而不是仅针对Maybe的特殊情况。如果您无法将这个“裸值没有构造函数”的功能作为ADT的通用功能工作,那么我根本不想要它。)


1
我错过了什么? x | y 不是一种类型,而只是 data 定义的简短语法的一部分。你可以在 GADT 语法中写出完整的定义。
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

竖线用于说明有效值的语法,就像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

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文,
原文链接