什么是多态/多类元组?

Question

当我在做haskell练习题的时候。我看到下面的代码通过将每种类型应用于约束构造函数来创建聚合Constraint。在GHC中，Constraint的深嵌套元组似乎仍然是Constraint类型的(可能是扁平的?)。

{-# LANGUAGE DataKinds     #-}
{-# LANGUAGE PolyKinds     #-}
{-# LANGUAGE TypeFamilies  #-}
{-# LANGUAGE TypeOperators #-}

type family All (c :: Type -> Constraint) (xs :: [Type]) :: Constraint where
All c '[] = ()
All c (x ': xs) = (c x, All c xs)
-- >>> :kind! All
-- All :: (* -> Constraint) -> [*] -> Constraint
-- = All
-- >>> :kind! All Eq '[Int, Double, Float]
-- All Eq '[Int, Double, Float] :: Constraint
-- = (Eq Int, (Eq Double, (Eq Float, () :: Constraint)))

我尝试使用PolyKinds扩展来推广它，如下所示。

{-# LANGUAGE DataKinds     #-}
{-# LANGUAGE PolyKinds     #-}
{-# LANGUAGE TypeFamilies  #-}
{-# LANGUAGE TypeOperators #-}

type family All' (c :: k -> r) (xs :: [k]) :: r where
All' c '[] = ()
All' c (x ': xs) = (c x, All' c xs)
-- >>> :kind! All'
-- All' :: (k -> r) -> [k] -> r
-- = All'
--- This one works. Tuples of Types is a Type.
-- >>> :kind! All' Maybe '[Int, Double, Float]
-- All' Maybe '[Int, Double, Float] :: *
-- = (Maybe Int, (Maybe Double, (Maybe Float, ())))
--- However this one gets stuck.
-- >>> :kind! All' Eq '[Int, Double, Float]
-- All' Eq '[Int, Double, Float] :: Constraint
-- = All' Eq '[Int, Double, Float]

是'(,) (a :: k) (b :: k)的种类也是k的种类。从下面看似乎不是这样，所以我想知道为什么类型族定义All' c (x ': xs) = (c x, All' c xs)首先被接受(考虑到类型族返回类型是r)?

λ> :kind! '(,)
'(,) :: a -> b -> (a, b)
= '(,)
λ> :kind! '(,) ('True :: Bool) ('False :: Bool)
'(,) ('True :: Bool) ('False :: Bool) :: (Bool, Bool)
= '( 'True, 'False)

正如@Daniel Wagner已经在下面提到的，这里使用的(,)被认为是Type -> Type -> Type，而在上面的第二个方程(All' c (x ': xs) = (c x, All' c xs))中，类型参数r被实例化为Type。事实上，如果我们使用'(,)，它将正确地返回类型错误。我能够使用下面这篇博文中描述的技术进一步确认它(All'用k和*类型实例化):

λ> :set -fprint-explicit-kinds
λ> :info All'
type All' :: forall k r. (k -> r) -> [k] -> r
type family All' @k @r c xs where
forall k (c :: k -> *). All' @k @(*) c ('[] @k) = ()
forall k (c :: k -> *) (x :: k) (xs :: [k]).
All' @k @(*) c ((':) @k x xs) = (c x, All' @k @(*) c xs)

Answer 1

这里有一个句法双关。实际上有几种不同类型的逗号:

(,) :: Type -> Type -> Type
(,) :: Constraint -> Constraint -> Constraint -- ...ish
'(,) :: a -> b -> (a, b)

请注意，这些类型中没有一种是统一的。另外，第二个有点像谎言;如果是x :: Constraint和y :: Constraint，则是(x, y) :: Constraint，但逗号不能像(,) x y那样放在前面。

当试图消除前两个歧义时，GHC假设您正在使用(,) :: Type -> Type -> Type，除非您在语法上不能使用它的地方(例如在=>的左侧)或者您已经给出了:: Constraint的显式注释。单引号'消除了前两个和最后一个之间的歧义。