问题标签 [system-f]

System F是在编写原型时简单地推理类型的好方法。除了自己实现之外，我还想使用现有的实现。

在寻找实现时，似乎没有任何实现——我不知道为什么。

我的问题是：系统 F 的规范实现是什么？

我正在阅读一篇关于 F _ω的论文，无法理解这句话背后的原因：

类型 (∀γ:*.F γ → β) 的类型项表明 F 是一个始终返回 β 的常数函数。

我猜“F γ → β”是类型项，即箭头类型。这个箭头类型是一个函数的类型，它接受一个由类型应用程序“F γ”计算的类型的参数，并返回一个类型为 β 的值。

如果是这种情况，为什么 F 应该是一个总是返回 β 的常量（类型）函数？它不能是任意类型的函数，比如返回 α 并且仍然满足类型检查器的函数吗？

谢谢你的时间。

我很想得到以下示例进行类型检查：

我知道可能无法推断和检查gs 类型（即使在这种特定情况下很明显，因为它只是一个部分应用程序）：Secret不是单射的，也无法告诉编译器Functor它应该期望哪个实例。因此，它失败并显示以下错误消息：

所以需要程序员的一些指导，如果我可以这样写，它会很容易被接受g：

System Fw 的大 lambda 的假设语法在哪里\\，即类型抽象。我可以用丑陋Proxy的 s 来模拟它，但是还有其他 GHC Haskell 功能可以让我写这样的东西吗？

所以我正在尝试以最终的无标签风格做 system f omega。我已经成功地对系统 f 进行了编码，如下代码（还给出了一些示例）（另外，请忽略推理不起作用并且示例非常丑陋的事实，我将在单独的问题中询问它们）：

但我在做 F omega 时遇到了麻烦。

所以我的问题是，如何解决它？似乎我可以在 lambda 类型上显式添加 beta 相等性（如 Idris Eq），并让用户使用它来重写 beta 缩减。

但是，我希望它自动完成。我的选择是什么？

在 System F 中，类型exists a. P可以被编码为forall b. (forall a. P -> b) -> b任何使用存在的 System F 术语都可以用这种编码来表示，这种编码尊重类型和归约规则。

在“类型和编程语言”中，出现了以下练习：

我们可以根据存在类型对通用类型进行编码吗？

我的直觉说这是不可能的，因为在某种程度上，“存在包装”机制根本不如“类型抽象”机制强大。我如何正式展示这一点？

我什至不确定我需要证明什么才能正式展示这个结果。

让我们定义列表类型

例如在哪里

我正在尝试定义zip类型的函数

直观地做到了

请注意，它会截断较长的列表以适应较短的列表。

我在这里遇到的主要问题是我不能一次“迭代”两个列表。如何在系统F中实现这样的功能？甚至可能吗？

我想使用 Agda 作为我的类型检查器和评估器来测试系统 F 中的一些定义。

我第一次尝试介绍 Church 自然数是通过写作

这将像常规类型别名一样使用：

然而，定义Num不输入（种类？）检查。使其工作并尽可能接近系统 F 表示法的最合适方法是什么？

考虑从a's 到成对的b's 和c's,的函数类型a -> (b, c)。（我将使用 Haskell 表示法来表示类型和函数，但这不是关于 Haskell 本身的问题。）有许多这样的函数，包括那些同时、一个或不(b, c)依赖于输出的函数a。

假设，特别是，第一个输出取决于a，但第二个不依赖（例如在 中\a -> (a, ())）。是否可以在多态 lambda 演算或 Hindley-Milner 中编写一个类型来表征所有且仅此类函数 - 换句话说，其子空间与a -> (b, c)同构(a -> b, c)？换句话说，我们是否可以定义一个f :: d（对于某些类型d）使得f (\a -> (a, ())), f (\a -> (a, 1)), ... 都是正确类型的，但是f (\a -> (a, a)), f (\a -> (a, snd a)), ... 都不是？

或者，有什么方法可以静态地确保 的元素a -> (b, c)具有此属性？

下面是几个简单的函数：

所有f1、f2和f3都能够接受()作为输入。另一方面，当然f4不能接受()；f4 ()是类型错误。

是否有可能从类型理论上描述f1、f2和f3的共同点？具体来说，是否可以定义一个acceptsUnit函数，使得acceptsUnit f1、acceptsUnit f2和acceptsUnit f3是类型良好的，但是acceptsUnit f4是类型错误——并且没有其他影响？

以下内容完成了部分工作，但将其输入单态化（在 Haskell 中，我在 Hindley-Milner 中收集），因此其效果不仅仅是断言其输入可以接受()：

当然，同样的单态化也发生在下面。在这种情况下，注解的类型acceptsUnit'是它的主要类型。