haskell - 类型族和部分新类型之间的区别？ (和部分数据？)

Question

我不得不连接两个库，其中元数据在一个库中表示为类型参数，在另一个库中表示为记录字段。我使用 GADT 编写了一个适配器。这是一个精简版:

{-# LANGUAGE GADTs #-}

newtype TFId  a = MkId   a
data    TFDup a = MkDup !a !a

data GADT tf where
  ConstructorId  :: GADT TFId
  ConstructorDup :: GADT TFDup

main = do
  f ConstructorId
  f ConstructorDup

f :: GADT tf -> IO ()
f = _

这行得通。 (可能并不完美；欢迎评论，但这不是问题所在。)

我花了一些时间才达到这种工作状态。我最初的直觉是为 TFId 使用一个类型族，计算:“GADT 有种类 (* -> *) -> *；在 ConstructorDup TFDup 中有种类 * -> *；所以对于 ConstructorId 我可以使用以下 * -> * 类型系列:”

{-# LANGUAGE TypeFamilies #-}
type family TFId a where TFId a = a

类型构造函数确实有相同类型的 * -> *，但 GHC 显然不会将它放在同一个地方:

error: …

• The type family ‘TFId’ should have 1 argument, but has been given none
• In the definition of data constructor ‘ConstructorId’ In the data type declaration for ‘GADT’

好吧，如果它这么说......

我不确定我是否理解为什么它会产生如此大的不同。不应用它们就不能使用类型族词干吗？这是怎么回事？还有其他(更好的)方法吗？

Answer 1

单射性。

type family F :: * -> *
type instance F Int  = Bool
type instance F Char = Bool

此处 F Int ~ F Char。然而，

data G (a :: *) = ...

永远不会导致 G Int ~ G Char。这些保证是不同的类型。

在像这样的通用量化中

foo :: forall f a. f a -> a

f 允许是 G(单射)但不允许是 F(非单射)。

这是为了进行推理。 foo (...::G Int) 可以推断为 Int 类型。 foo (...::F Int) 等同于 foo (...::Bool) 可能具有 Int 类型，或者类型 Char -- 这是一个不明确的类型。

还要考虑 foo True。我们不能期望 GHC 为我们选择 f ~ F, a ~ Int (or Char)。这将涉及查看所有 类型族并查看Bool 是否可以由它们中的任何一个生成——本质上，我们需要反转所有类型族。即使这是可行的，它也会产生大量可能的解决方案，因此它会是模棱两可的。