为什么`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 可能是 ⊥ 吗？

- rampion

Answer 1

原因很简单，类型级别上没有eta-conversion检查机制。首先，没有区分可能具有eta规律的单构造记录/产品和数据定义的机制。我不认为p可能是⊥是这个原因的有效理由。即使在部分惰性语言中，对于成对的eta相等性成立（关于观察等价性）。

- András Kovács

Answer 2

问题在于 p 可能是 ⊥ 吗？

多多少少是的。不幸的是，所有类型都被空类型家族所占据。

type family Any :: k

这会挫败任何试图实现你所尝试做的事情的理论。我认为这真的需要修复；然而，我不确定是否有任何计划来解决这个问题。

- luqui

---

任何问题都不应该成为障碍。如果 GHC 将类型级记录匹配转换为原始投影，就像 Agda/Coq 中一样，那么 Any 将无法与 (Fst Any, Snd Any) 区分开来，从而验证 eta 规则。 - András Kovács

@AndrásKovács，啊，我明白你的意思了。我认为Any仍然是相关的，因为它对于余积来说是一个问题——或者例如如果(,)在Agda中被定义为data类型而不是record。 - luqui

是的，我的意思是在这种情况下这不是一个问题，但我认为对于余积来说也不是真正的问题，因为尽管 Any 使余积 eta 失效，但类型检查器几乎从不检查余积 eta。（但我也认为摆脱 Any 是好的）。 - András Kovács

@AndrásKovács，是的，但在Agda中，没有类型级底部（或任何底部），至少有模式匹配的可能性，以便您可以说服定义通过。在Haskell中则不然。但我们谈得越多，我的评论似乎与这个问题的相关性就越小，它只是我的一般抱怨。:-p - luqui