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

使用 GADT 表示法可能会解决问题，因为标准表示法将类型级和值级语言混合在一起。

\n

标准Maybe类型因此看起来像 GADT：

\n

{-# LANGUAGE GADTs #-}\n\ndata Maybe a where\n  Nothing :: Maybe a\n  Just :: a -> Maybe a\n

\n

\xe2\x80\x9cun 参数化\xe2\x80\x9d 版本也是可能的：

\n

data EMaybe where\n  ENothing :: EMaybe\n  EJust :: a -> EMaybe\n

\n

（正如 Joseph Sible 评论的那样，这被称为存在主义类型）。现在你可以定义

\n

foo :: Maybe Int\nfoo = Just 37\n\nfoo' :: EMaybe\nfoo' = EJust 37\n

\n

太好了，那我们为什么不直接使用EMaybealways呢？

\n

好吧，问题是当你想使用这样的值时。有了Maybe它，您就可以完全控制所包含的类型：

\n

bhrar :: Maybe Int -> String\nbhrar Nothing = "No number "\nbhrar (Just i)\n | i<0        = "Negative "\n | otherwise  = replicate i ''\n

\n

但是你能用 type 的值做什么呢EMaybe？事实证明，并不多，因为包含某种未知类型EJust的值。因此，无论您尝试使用该值做什么，都将是类型错误，因为编译器无法确认它实际上是正确的类型。

\n

bhrar :: EMaybe -> String\nbhrar' (EJust i) = replicate i ''\n  =====> Error couldn't match expected type Int with a\n

\n

Answer 2

如果一个变量没有反映在返回类型中，那么它被认为是存在的。这是可以定义的data ExMaybe = ExNothing | forall a. ExJust a，但其论证ExJust是完全没有用的。ExJust True并且ExJust ()两者都有类型ExMaybe并且从类型系统的角度来看是无法区分的。

Maybe这是原始语法和存在语法的 GADT 语法ExMaybe

{-# 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