为了使事情更加清晰,最好使用GADT符号表示法,因为标准符号将类型和值级语言混合在一起。
标准的Maybe
类型在GADT中如下所示:
{-# LANGUAGE GADTs #-}
data Maybe a where
Nothing :: Maybe a
Just :: a -> Maybe a
“未参数化”版本也是可行的:
data EMaybe where
ENothing :: EMaybe
EJust :: a -> EMaybe
(正如Joseph Sible所评论的那样,这被称为存在类型)。现在您可以定义。
foo :: Maybe Int
foo = Just 37
foo' :: EMaybe
foo' = EJust 37
好的,那么为什么我们不总是使用 EMaybe
呢?
问题在于当您想要 使用 这样的值时。使用 Maybe
没有问题,您可以完全控制所包含的类型:
bhrar :: Maybe Int -> String
bhrar Nothing = "No number "
bhrar (Just i)
| i<0 = "Negative "
| otherwise = replicate i ''
但是,如果你有一个EMaybe
类型的值,你能做什么呢?其实没什么用处,因为EJust
包含了一个某种未知类型的值。所以无论你尝试将该值用于任何操作,都会导致类型错误,因为编译器无法确认它是否为正确的类型。
bhrar :: EMaybe -> String
bhrar' (EJust i) = replicate i ''
=====> Error couldn't match expected type Int with a
data Maybe = ...
定义了一种Type
类型的东西,而data Maybe a = ...
定义了一种Type -> Type
类型的东西。以不同的方式写不同的事情要简单得多,而不必推断一个语法应该意味着两个不同事物中的哪一个。 - chepnerExistentialQuantification
和RankNTypes
扩展,您可以编写data EMaybe = ENothing | forall a. EJust a
和data R2Maybe = R2Nothing | R2Just (forall a. a)
,GHC将接受它们。这样做然后尝试一些基本的适应于它们的Maybe
示例并查看发生了什么可能会很有启发性。 - Joseph Sible-Reinstate Monicadata Either = Left a | Right b
的东西。Either String Int
和Either Int String
是相同的吗?如果是,那么Left 3
和Left "foo"
之间有什么区别?如果不是,那么Left 3
正确还是Left "foo"
正确? - chepner