问题标签 [existential-type]

我收到如下错误消息：

实际类型似乎比预期类型更通用。那么这种错误消息的可能原因是什么？该消息是否具有误导性或我是否阅读不正确？

我想做的是传递一个存在量化的函数runSubstT，它的类型是：

我还将对 GHC 编译器如何对存在量化类型执行类型匹配进行一些很好的描述。

我对类型的存在量化是什么以及可以在哪里使用有一个大致的了解。然而，根据我迄今为止的经验，为了有效地使用这个概念，需要理解很多警告。

问题：是否有任何好的资源来解释 GHC 中如何实施存在量化？IE

• 存在类型的统一是如何工作的——什么是统一的，什么不是？
• 对类型的后续操作以什么顺序执行？

我的目标是更好地理解 GHC 向我抛出的错误信息。消息通常会说一些类似的东西"this type using forall and this other type don't match"，但是他们没有解释为什么会这样。

例如，List[T] forSome { type T }等价于List[_]，但对于每种可能的用法是否都是如此，forSome或者是否存在forSome不能被第二种语法的等价物替换的情况？

给定一个元组，其元素的类型A和另一种类型在 中参数化A：

和一个使用站点：

为什么使用元组的提取器可以按预期工作：

但以下失败：

带有错误信息

我可以修复第二种形式 ( test2) 以正确编译吗？

编辑

与 Owen 的想法不同，我尝试了是否可以在完全没有模式匹配的情况下使其工作（这是我首先想要的）。这里还有两个奇怪的案例，一个有效，另一个无效：

对我来说还是很模糊...

许多静态类型语言具有参数多态性。例如在 C# 中可以定义：

在呼叫站点中，您可以执行以下操作：

这些类型有时也写成这样：

我听说有人说“forall 就像类型级别的 lambda 抽象”。所以 Foo 是一个函数，它接受一个类型（例如 int）并产生一个值（例如一个 int -> int 类型的函数）。许多语言推断类型参数，以便您可以编写Foo(3)而不是Foo<int>(3).

假设我们有一个f类型为 的对象forall T. T -> T。我们可以对这个对象做的首先是Q通过写给它一个类型f<Q>。然后我们返回一个 type 的值Q -> Q。但是，某些f' 是无效的。例如这个f：

因此，如果我们“调用” f<int>，那么我们会返回一个带有 type 的值，int -> int一般来说，如果我们“调用” f<Q>，那么我们会返回一个带有 type 的值Q -> Q，所以这很好。但是，通常认为这f不是 type 的有效事物，因为根据您传递的类型forall T. T -> T，它会做不同的事情。forall 的想法是明确不允许这样做。另外，如果 forall 是类型级别的 lambda，那么存在什么？（即存在量化）。由于这些原因，似乎 forall 和 exists 并不是真正的“类型级别的 lambda”。但那它们是什么？我意识到这个问题相当模糊，但有人可以帮我解决这个问题吗？

一个可能的解释如下：

如果我们看逻辑，量词和 lambda 是两个不同的东西。量化表达式的一个例子是：

所以有两部分要考虑：一个用于量化的集合（例如整数）和一个谓词（例如 P）。Forall 可以看作是一个高阶函数：

带类型：

Exists 具有相同的类型。Forall 就像一个无限合取，其中 S[n] 是集合 S 的第 n 个元素：

Exists 就像一个无限析取：

如果我们对类型进行类比，我们可以说∧的类型类比是计算交集类型∩，∨的类比类型是计算并集类型∪。然后我们可以定义 forall 和存在于类型上，如下所示：

所以forall是一个无限的交集，exists是一个无限的并集。他们的类型是：

例如多态恒等函数的类型。这Types是所有类型的集合，->是函数的类型构造函数，=>是 lambda 抽象：

现在类型的东西forall T:Type. T -> T是一个值，而不是从类型到值的函数。它是一个值，其类型是所有类型 T -> T 的交​​集，其中 T 涵盖所有类型。当我们使用这样的值时，我们不必将其应用于类型。相反，我们使用子类型判断：

这向下转换id为有 type int -> int。这是有效的，因为int -> int也出现在无限交集。

我认为这很好用，它清楚地解释了 forall 是什么以及它与 lambda 的不同之处，但这个模型与我在 ML、F#、C# 等语言中看到的不兼容。例如在 F# 中你id<int>可以获取整数上的标识函数，这在此模型中没有意义：id 是值上的函数，而不是返回值上的函数的类型上的函数。

有类型理论知识的人可以解释一下到底什么是 forall 和存在的吗？“forall 在类型级别上是 lambda”在多大程度上是真的？

当使用 Existential 类型时，我们必须使用模式匹配语法来提取foralled 值。我们不能将普通的记录选择器用作函数。GHC 报告错误并建议使用以下定义的模式匹配yALL：

我的一些数据包含超过 5 个元素。如果我使用模式匹配，很难维护代码：

有没有一种好方法可以使这样的代码可维护或将其包装起来以便我可以使用某种选择器？

考虑以下类定义：

我想要一个学生和教授的名单：

但这无法编译并出现以下错误：

感谢 Daniel C. Sobral 对我之前的相关问题How to define case classes with members with unbound type parameters?的回答。我知道存在类型会在这里解决问题。这编译：

<: Person[T]问题是由类 Person 的声明的类型参数中的上限引起的。删除上限可以让编译器推断列表的类型参数，使其编译：List[Person[Person[Person[Any]]]]据我所知。

问题

1. 为什么编译器不能推断出可以编译的列表的任何类型？
2. 存在类型是最不冗长的，而且可能更棘手（参见丹尼尔对我上面链接的上一个问题的回答）：是否有替代显式存在类型来创建学生和教授列表？

假设我有一个函数，它采用函数列表对的列表，并将每对中的函数映射到对中的列表上，例如：

有没有办法实现 myFunction 以便我上面提供的代码无需任何修改就可以正常工作？

我的问题是我不知道如何实现 myFunction 因为每个子列表的类型可能不同（在我的示例中，我有一个字符串列表 ["DAY", ONE"] 和一个数字列表：[ 1,2]). 我知道列表中的每个函数都会将其列表转换为字符串列表（因此最终列表将具有 [[Char]] 类型），但我不知道如何在 Haskell 中表达这一点.

我需要一个可以包含任意值的映射，只要它们的类型属于相同的类型类。我的第一个天真的方法是这样的：

但它似乎不起作用：以下代码给出了编译错误：

我以为我需要特殊的异构集合，但奇怪的是我在谷歌中找不到任何东西，但这个库似乎有点邋遢和陈旧。正确执行此操作的方法是什么（希望没有其他库，仅使用 GHC 扩展）？

Haskell Wiki很好地解释了如何使用存在类型，但我不太了解它们背​​后的理论。

考虑这个存在类型的例子：

为我们可以转换为String. wiki 提到我们真正想要定义的类型是

即一个真正的“存在”类型——我松散地认为这是在说“数据构造函数S采用任何存在Show实例的类型并包装它”。实际上，您可能可以编写如下 GADT：

我没有尝试编译它，但它似乎应该可以工作。对我来说，GADT 显然等同于我们想要编写的代码 (2)。

但是，我完全不明白为什么（1）等于（2）。为什么将数据构造函数移到外面会forall变成一个exists？

我能想到的最接近的是逻辑中的德摩根定律，其中交换否定和量词的顺序将存在量词变成全称量词，反之亦然：

但数据构造函数似乎与否定运算符完全不同。

forall使用而不是不存在来定义存在类型的能力背后的理论是什么exists？