polymorphic/polykinded 元组是什么样的？

Question

当我正在回答 haskell-excercises 问题时。我看到以下代码通过将每种类型应用于 Constraint 构造函数来创建聚合 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) 首先被接受（考虑到类型族 return kind 是 r）？

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

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

更新

正如@Daniel Wagner 已经在下面提到的，这里使用的 (,) 被认为是 Type -> Type -> Type 并且 kind 参数 r 在上面的第二个等式中被实例化为 Type (All' c (x ': xs) = (c x, All' c xs))。事实上，如果我们使用 '(,)，它会正确地 returned 一个类型错误。我能够使用以下技术 described in this blog post 进一步确认它（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)

请注意，none 这些类型与任何其他类型统一。此外，第二个有点谎言。如果 x :: Constraint 和 y :: Constraint，则 (x, y) :: Constraint，但逗号不能像 (,) x y.

那样作为前缀

当试图消除前两个歧义时，GHC 假定您正在使用 (,) :: Type -> Type -> Type 除非您在语法上不能使用它的地方（例如 => 的左侧）或者您有给定 :: Constraint 的明确种类注释。单勾 ' 消除了前两个和最后一个之间的歧义。

polymorphic/polykinded 元组是什么样的？

What is the kind of polymorphic/polykinded tuples?

haskell

type-families

polykinds