为啥 `forall (a :: j) (b:: k)` 与 `forall (p :: (j,k))` 的工作方式不同？

Posted 2023-03-28

【中文标题】为啥 `forall (a :: j) (b:: k)` 与 `forall (p :: (j,k))` 的工作方式不同？

【英文标题】：Why does `forall (a :: j) (b:: k)` work differently than `forall (p :: (j,k))`?为什么 `forall (a :: j) (b:: k)` 与 `forall (p :: (j,k))` 的工作方式不同？

【发布时间】：2018-12-14 15:43:21

【问题描述】：

我试图了解使用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 可能是⊥ 的问题吗？

【参考方案1】：

原因很简单，类型级别上没有 eta 转换检查。首先，没有机制可以将 data 定义与可能具有 eta 定律的单构造函数记录/产品区分开来。我不认为p 可能是⊥ 是这样做的正当理由。即使在部分惰性语言中，对的 eta 等式也成立（w.r.t. 观察等价）。

【参考方案2】：

p 可能是⊥ 的问题吗？

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

type family Any :: k

这会挫败任何允​​许您尝试做的事情的理论。我认为它确实需要修复；不过，我不确定是否有这样做的计划。

【讨论】：

Any 应该不是问题。如果 GHC 将类型级别记录上的匹配转换为原始投影，如在 Agda/Coq 中，那么 Any 将与 (Fst Any, Snd Any) 无法区分，从而验证 eta 规则。

@AndrásKovács，啊，我明白你的意思了。我认为Any 仍然是相关的，因为它给副产品带来了问题——或者例如。如果 (,) 在 Agda 中被定义为 data 类型，而不是 record。

是的，我的意思是在这种情况下这不是问题，但我认为这对于副产品来说也不是问题，因为尽管Any 使副产品 eta 无效，但类型检查器几乎从不检查副产品 eta反正。 （但我也认为摆脱 Any 会很好）。

@AndrásKovács，是的，但是在 Agda 中，没有类型级别的底部（或任何底部），至少有可能进行模式匹配，以便您可以说服您的定义通过。在 Haskell 中并非如此。但我们谈论的越多，我的评论似乎与这个精确问题的相关性就越低，这只是我的普遍不满。 :-p