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)

Answer 1

如果一个变量没有反映在返回类型中，它被认为是存在的。这可以定义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

Answer 2

具有显式类型参数使其更具表现力。没有它，你会丢失很多信息。例如，map 的类型你会怎么写？还是一般的函子？

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

这个版本几乎没有说明发生了什么

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

或者更糟糕的是，head:

head ::  [] -> a

现在我们突然可以使用不安全的强制和零类型安全了。

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

但我们不仅会失去安全感，还会失去做一些事情的能力。例如，如果我们想将read 某个东西放入一个列表或Maybe，我们就不能再指定我们想要什么样的列表。

read :: Read a => a

example :: [Int] -> String

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

如果没有具有显式类型参数的列表，则无法编写此程序。 （或者更确切地说，read 将无法为不同的列表类型提供不同的实现，因为内容类型现在是不透明的）

---

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

Answer 3

使用 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