Haskell 中的参数化类型

Question

为什么在Haskell中类型必须在类型构造器参数中显式地进行参数化？

例如：

data Maybe a = Nothing | Just a  

a必须在类型中进行指定。为什么不能只在构造函数中指定？

data Maybe = Nothing | Just a 

从设计角度来看，为什么他们做出这个选择？一个比另一个更好吗？

我确实理解第一个比第二个更强类型，但没有第二个选项。

编辑:

示例函数

data Maybe = Just a | Nothing

div :: (Int -> Int -> Maybe)
div a b
  | b == 0    = Nothing
  | otherwise = Just (a / b)

- Caelan Miron

---

在你的例子中，“Just True”和“Just 42”的类型是否相同？如果是，你认为会有什么问题吗？如果不是，你认为它们之间的区别是什么？ - Joseph Sible-Reinstate Monica

它并不是更加“强类型”，而是不同的类型。data Maybe = ...定义了一种Type类型的东西，而data Maybe a = ...定义了一种Type -> Type类型的东西。以不同的方式写不同的事情要简单得多，而不必推断一个语法应该意味着两个不同事物中的哪一个。 - chepner

特别是使用ExistentialQuantification和RankNTypes扩展，您可以编写data EMaybe = ENothing | forall a. EJust a和data R2Maybe = R2Nothing | R2Just (forall a. a)，GHC将接受它们。这样做然后尝试一些基本的适应于它们的Maybe示例并查看发生了什么可能会很有启发性。 - Joseph Sible-Reinstate Monica

考虑类似于 data Either = Left a | Right b 的东西。Either String Int 和 Either Int String 是相同的吗？如果是，那么 Left 3 和 Left "foo" 之间有什么区别？如果不是，那么 Left 3 正确还是 Left "foo" 正确？ - chepner

你在最后添加的示例只展示了如何创建这样的值。但是@JosephSible-ReinstateMonica问题的第二部分同样重要：那么你将如何使用该值？ - Fyodor Soikin

Answer 1

为了使事情更加清晰，最好使用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

- leftaroundabout

---

谢谢提供示例，现在我明白了。现在JosephSible-ReinstateMonica的评论也有意义了。 - Caelan Miron

Answer 2

如果一个变量在返回类型中没有反映出来，那就被认为是存在性的。可以使用 data ExMaybe = ExNothing | forall a. ExJust a 来定义，但是 ExJust 的参数完全没有用处。从类型系统的角度来看，ExJust True 和 ExJust () 都具有类型 ExMaybe，并且无法区分它们。

以下是原始的 Maybe 和存在性的 ExMaybe 的 GADT 语法。

{-# Language GADTs                    #-}
{-# Language LambdaCase               #-}
{-# Language PolyKinds                #-}
{-# Language ScopedTypeVariables      #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications         #-}

import Data.Kind (Type)
import Prelude hiding (Maybe(..))

type Maybe :: Type -> Type
data Maybe a where
  Nothing ::      Maybe a
  Just    :: a -> Maybe a

type ExMaybe :: Type
data ExMaybe where
  ExNothing ::      ExMaybe
  ExJust    :: a -> ExMaybe

你的问题就像是在问为什么一个函数 f x = .. 需要指定它的参数，虽然可以将类型参数设置为不可见，但这非常奇怪，即使不可见，参数仍然存在。

-- >> :t JUST
-- JUST :: a -> MAYBE
-- >> :t JUST 'a'
-- JUST 'a' :: MAYBE
type MAYBE :: forall (a :: Type). Type
data MAYBE where
  NOTHING ::      MAYBE @a
  JUST    :: a -> MAYBE @a

mAYBE :: b -> (a -> b) -> MAYBE @a -> b
mAYBE nOTHING jUST = \case
  NOTHING -> nOTHING
  JUST a  -> jUST a

- Iceland_jack

---

需要哪些扩展程序才能使这些示例正常工作？我认为它可能需要一些非平凡的扩展程序。 - pedrofurla

我添加了必要的扩展，StandaloneKindSignatures 和 GADTs/GADTSyntax 是理解更复杂的数据类型的好组合。它们通过“类型形成规则”（:kind 输出）和“项引入规则”（:type 输出）来定义类型。 - Iceland_jack

Answer 3

有明确的类型参数会使其更加具有表现力。没有它，你会失去很多信息。例如，你如何编写map的类型？或者一般的函子（functors）呢？

map :: (a -> b) -> [a] -> [b]

这个版本几乎没有说明正在发生什么。

map :: (a -> b) -> [] -> []

甚至更糟的是，head标签：

head ::  [] -> a

现在我们突然拥有了不安全的coerce和零类型安全性。

unsafeCoerce :: a -> b
unsafeCoerce x = head [x]

但是我们不仅失去了安全性，还失去了某些功能。例如，如果我们想将某些内容读取到列表或Maybe中，我们就无法指定所需列表的类型。

read :: Read a => a

example :: [Int] -> String

main = do
  xs <- getLine
  putStringLine (example xs)

如果列表没有显式类型参数，那么这个程序是不可能编写的。(或者说，read 无法为不同的列表类型实现不同的实现，因为内容类型现在是不透明的)

---

然而，正如其他人所提到的，仍然可以通过使用 ExistentialQuantification 扩展来定义类似的类型。但在这些情况下，您在使用这些数据类型时非常受限制，因为您无法知道它们包含什么。

- Hjulle