Haskell 中的参数化类型

Posted 2023-03-15

【中文标题】Haskell 中的参数化类型

【英文标题】：Parameterized Types in Haskell

【发布时间】：2021-12-17 23:11:34

【问题描述】：

为什么 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)

【问题讨论】：

在您的示例中，Just True 和 Just 42 的类型是否相同？如果是这样，您是否看到任何可能导致的问题？如果不是，您认为会有什么不同？

不是更“强”的类型；它的不同类型。 data Maybe = ... 定义了类似 Type 的东西，而 data Maybe a = ... 定义了类似 Type -> Type 的东西。以不同的方式编写不同的东西会更简单，而不是必须推断出两种不同的东西中的哪一种。

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

考虑类似data Either = Left a | Right b。 Either String Int 和 Either Int String 是否相同？如果是这样，Left 3 和 Left "foo" 之间有什么区别？如果不是，是Left 3 正确还是Left "foo" 正确？

您最后添加的示例仅显示创建这样的值。但@JosephSible-ReinstateMonica 问题的第二部分同样重要：然后你将如何使用该值？

【参考方案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

【讨论】：

需要哪些扩展才能使这些示例正常工作？我假设它需要一些重要的。

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

【参考方案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 扩展来定义类似的类型。但在这些情况下，您使用这些数据类型的方式非常有限，因为您无法知道它们包含什么。

【参考方案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

【讨论】：

感谢您的示例，现在它很有意义。现在@JosephSible-ReinstateMonica cmets 也有意义。