问题标签 [system-f]

在“什么是欣德利·米尔纳”下，它指出：

Hindley-Milner 是System F的一个限制，它允许更多类型但需要程序员注释。

我的问题是，什么是 System F 中可用的类型的示例，但在 Hindley Milner 中不可用（类型推断）？

（假设系统 F 类型的推断已被证明是不可判定的）

我一直在阅读各种类型系统和 lambda 演算，我发现 lambda 立方体中的所有类型化 lambda 演算都在强归一化，而不是图灵等价物。这包括 System F，简单类型的 lambda 演算和多态性。

这使我想到了以下问题，我一直无法找到任何可以理解的答案：

• （例如）Haskell 的形式主义与它表面上基于的微积分有何不同？
• Haskell 中的哪些语言特性不属于 System F 形式主义？
• 允许图灵完成计算所需的最小更改是多少？

非常感谢任何帮助我理解这一点的人。

我不明白为什么这个程序不可输入：

我使用-XRankNTypesGHC 选项。

我有以下错误：

有人可以帮我吗？

如何系统地计算系统 F 中给定类型的居民数量？

假设有以下限制：

• 所有居民都终止，即没有底部。
• 所有居民都没有副作用。

例如（使用 Haskell 语法）：

• Bool有两个居民。
• (Bool, Bool)有四个居民。
• Bool -> (Bool, Bool)有十六个居民。
• forall a. a -> a有一个居民。
• forall a. (a, a) -> (a, a)有四个居民。
• forall a b. a -> b -> a有一个居民。
• forall a. a居民为零。

为前三个实现算法是微不足道的，但我不知道如何为其他算法做。

在 System F 中，多态类型的类型是*（因为这是 System F 中唯一的类型......），例如对于以下封闭类型：

我想在 Agda 中表示 System F，因为一切都在 中*，我想我会将类型（如上）解释为 Agda Sets; 所以像

但是，Agda 没有多态类型，因此在 Agda 中，上述类型需要是（大！）Π 类型：

这意味着它不在 Set₀ 中：

有没有办法解决这个问题，或者 System F 在这个意义上不能嵌入到 Agda 中？

我正在尝试在 Haskell 中实现 System-F 风格的数据结构。

我将使用A <B>to 表示将术语A应用于类型B只是为了使其明确（也使用大写字母表示类型）。

假设Tree <T>是具有 type 值的二叉树的类型T。我们想找到一种可以充当Tree <T>. 构造函数有以下三种：

因此，我认为，由于 Girard 的一些聪明才智，我们可以使用以下

从中

我在 Haskell 中发现了这些东西所需的指令，我认为我没有遗漏任何指令。所以在 Haskell 中：

到目前为止，所有这些都可以编译并且似乎可以工作。当我尝试Show为我的T t类型创建一个实例时，问题就出现了。我添加了更多指令：

和打印树的功能

有适当的助手displayEmpty :: String和displayFork :: String -> String -> String. 这也可以编译和工作（直到漂亮）。现在，如果我尝试实例T t化为Show

尝试编译时出现以下错误：

我（想我）理解它们存在的必要性TypeSynonymInstances和FlexibleInstances实用性原因，但我不明白为什么我的类型T t 仍然不能被声明为Show. 有没有办法做到这一点，什么属性T t意味着这在我的代码中目前存在问题？

我有一个我不太了解的 System F 多态性示例：

如果我要删除它会保留的类型： \f.\af (fa) 这没有任何意义。

你能帮我解决这个问题吗？谢谢！

在 System F 中，以下 3 种类型有什么区别：

在此处以文本形式转载：

第二个比第一个更通用吗？

我需要知道 Haskell 绑定类型 (>>=) 运算符的 System F 类型是什么。

到目前为止，我是这样写的：

这样对吗？如果正确，我如何找到最终结果？

谢谢！

Matt Might谈到在7 行 Scheme中实现Lambda Calculus解释器：

现在这不是简单类型的 Lambda 演算。在Haskell 的核心中，有一种与System F非常相似的中间语言。一些人（包括Simon Peyton Jones）称其为简单类型 Lambda 演算的实现。

我的问题是：扩展无类型 Lambda 演算实现以涵盖简单类型 Lambda 演算需要什么？