Что такое полиморфные / поликиндированные кортежи?

Question

Пока я вопросы задавалhaskell-exrcises . Я видел следующий код, который создает агрегат, применяя каждый тип к конструктору ограничений. В GHC кажется, что глубоко вложенные кортежи s по-прежнему являются своего рода 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) было принято в первую очередь (учитывая тип семьи возвращаемый вид был)?

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

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

ОБНОВИТЬ

Как уже упоминал @Daniel Wagner под (,) используемый здесь рассматривается как Type -> Type -> Type и параметр вида r создается для Type во втором уравнении выше ( All' c (x ': xs) = (c x, All' c xs)). Фактически, если бы мы использовали '(,), он правильно вернул бы ошибку типа. Я смог дополнительно подтвердить это, используя методику, описанную в этом сообщении в блоге, а именно:

      λ> :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. Одинарная галочка ' устраняет неоднозначность между первыми двумя и последним.