Почему `forall (a:: j) (b:: k)` работает иначе, чем `forall (p:: (j,k))`?

Question

Я пытаюсь понять разницу между использованием forall количественно определить переменные двух типов и используя forall количественно определить переменную одного типа типа кортежа.

Например, даны следующие семейства типов:

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

type family Fst (p :: (a,b)) :: a where
  Fst '(a,_) = a
type family Snd (p :: (a,b)) :: b where
  Snd '(_,b) = b
type family Pair (p :: (Type,Type)) :: Type where
  Pair '(a,b) = (a,b)

Я могу определить тождество для пар, используя переменные двух типов, и заставить его скомпилировать в GHC 8.0.1:

ex0 :: forall (a :: Type) (b :: Type). Pair '(a,b) -> (Fst '(a,b), Snd '(a,b))
ex0 = id

Однако это же определение не компилируется, если я использую переменную одного типа типа кортежа:

ex1 :: forall (p :: (Type,Type)). Pair p -> (Fst p, Snd p)
ex1 = id
-- Ex.hs:20:7: error:
--     • Couldn't match type ‘Pair p’ with ‘(Fst p, Snd p)’
--       Expected type: Pair p -> (Fst p, Snd p)
--         Actual type: (Fst p, Snd p) -> (Fst p, Snd p)
--     • In the expression: id
--       In an equation for ‘ex1’: ex1 = id
--     • Relevant bindings include
--         ex1 :: Pair p -> (Fst p, Snd p) (bound at Ex.hs:20:1)

Проблема в том, что p возможно ⊥?

Answer 1

Причина в том, что на уровне типов нет проверки eta-преобразования. Начнем с того, что нет механизма для различения data определения из записей / продуктов с одним конструктором, которые, возможно, имеют законы ETA. Я не думаю p возможно быть ⊥ является уважительной причиной для этого. Даже в частично ленивых языках выполняется равенство eta для пар (в отношении наблюдательной эквивалентности).

Answer 2

Проблема в том, что p возможно ⊥?

Более менее. К сожалению, все виды населены пустой семьей типов.

type family Any :: k

Что расстраивает любую теорию, которая позволила бы то, что вы пытаетесь сделать. Я думаю, что это действительно нужно исправить; Однако я не уверен, есть ли планы сделать это.