为什么"forall(a::j)(b::k)"的工作方式与"for all(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)

我可以使用两个类型变量在对上定义一个标识，并将其在GHC8.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等式也成立(w.r.t.观察等价(。

Answer 2

p可能是⊥的问题吗？

或多或少。不幸的是，所有种类的人都居住在空虚型家庭中。

type family Any :: k

这让任何允许你尝试做什么的理论都感到沮丧。我认为它真的需要修正；然而，我不确定是否有这样做的计划。