我在想为什么在Haskell(和FP一般)中,像Maybe
这样的函子被定义为
data Maybe a = Nothing | Just a
不要只是简单地
data Maybe a = Nothing | a
第二个选项仍然是函子的,因为
Maybe
函子将类型 a
映射到类型 Nothing + a
。我错过了什么?我在想为什么在Haskell(和FP一般)中,像Maybe
这样的函子被定义为
data Maybe a = Nothing | Just a
不要只是简单地
data Maybe a = Nothing | a
Maybe
函子将类型 a
映射到类型 Nothing + a
。我错过了什么?Just
是“鉴别器”。 一些语言确实有它们 - 例如 TypeScript。let x =“foo”
,那么x
的类型是什么?是String
还是Maybe String
?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
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
)。现在我们可以依赖于能够区分Nothing
和Just
,一旦我们知道我们有了一个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"
值,我是给它错误情况吗?还是当a
是String
时我给它成功的情况?或者当a
是Maybe(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的通用功能工作,那么我根本不想要它。)
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
”
a
和a
有什么区别?(提示:其中一个是Maybe
,你能分辨出哪个吗?) - cafce25