haskell - 证明 Haskell 中名义类型角色需要的最简单示例

Question

我试图了解是什么决定了类型参数是否必须是标称的。

虽然 GADT 和类型家族在某种意义上看起来不同，但它们不是“简单容器”，因为它们的实例定义可以“查看”它们的参数，但简单类型是否可以明显需要名义参数，例如 Set？

Answer 1

你应该可以强制吗？

 coerce :: Coercible a b => F a -> F b

如果不是，那么 F 的参数应该是名义上的。

在 Set 的情况下它的第一个角色是名义上的

type role Set nominal

因为我们不想

coerce :: Set Int -> Set ReversedInt

因为 newtype ReversedInt = RevInt Int deriving (Eq, Ord) via Data.Ord.Down Int有一个完全不同的 Ord比 Int以及 Set的内部结构取决于其元素的顺序。 Map 相同

type role Map nominal representational

对于像这样的 GADT

data F :: Type -> Type where
  FInt :: F Int

我们只有一个居民，所以我们不想让

coerce :: F Int -> F ReversedInt

所以，GHC 推断 type role F nominal .