类型构造函数和存在类型

Posted 2023-03-28

【中文标题】类型构造函数和存在类型

【英文标题】：Types constructors and existential types

【发布时间】：2017-04-20 11:21:38

【问题描述】：

只有多态函数可以应用于存在类型的值。 这些属性可以通过相应的表达式量词来表达，并通过自然变换来表征。

同样，当我们定义一个类型构造函数时

data List a = Nil | Cons a (List a)

此类型构造函数适用于所有a，而类型族允许具有非统一类型构造函数

type family TRes i o
type instance TRes Bool = String
type instance TRes String  = Bool

在类型级别上，这种“统一性”概念的确切特征是什么自然转换？

是否存在类似于我们在价值级别使用 rank-n 类型的强制自然性的等价物？

ApplyNat :: (forall a. a -> F a) -> b -> F b

【参考方案1】：

我认为您在这里混淆了几个不同的想法。

此类型构造函数适用于所有a。

这是整体。给定a 类型* 的任何参数，List :: * -> * 生成类型* 的有效类型。 Haskell 98 数据类型总是总数，但是，正如您所指出的，在现代 Haskell 中，您可以编写不涵盖所有可能情况的类型系列。 TRes Int 不是“真正的”类型，因为它不包含任何值，它不归约为任何其他类型，并且不等于 TRes Int 以外的任何类型。

Haskell 在值级别或类型级别没有整体检查器（除了关于不可判定实例的规则，这是一种钝器），因此，正如无法排除 undefined 值一样，有无法排除像TRes Int 这样的“卡住”类型的家庭。 （有关“卡住”类型家族的更多信息，请参阅TypeInType 的设计师 Richard Eisenberg 的this blog post。）

自然是一个完全不同的概念。在值级别的 Haskell 中，f 和 g 之间的自然转换是一个多态函数，将 f x 类型的值映射到 g x 类型的值，而无需了解任何关于 x 的信息。

type f ~> g = forall x. f x -> g x

在 GHC 8 和 TypeInType 中，我们可以使用我们用来讨论类型的相同语言来讨论种类，因为种类是类型。类型表达式forall x. f x -> g x 具有类型* ((~>) :: forall k. (k -> *) -> (k -> *) -> *)，因此它也是一个完全有效的类型分类器。具有这种类型的类型是多态类型函数，将类型 f x 映射到类型 g x。

在现实世界中，您会将类型级别的自然转换用于什么目的？我不知道。你可能不会。

【讨论】：

我应该明确“为所有人统一工作”。这是我想知道的自然概念。显然，在价值和类型级别上属于不同的类别。

强制自然对于确保树的进度很有用。 [11] Hasuo, I., Jacobs, B., Uustalu, T.：关于树计算的分类观点。

patrick bahr itu.dk/people/paba/pubs/files/bahr12mpc-paper.pdf在价值层面有一个很好的实现@