问题标签 [type-theory]

http://muaddibspace.blogspot.com/2008/01/type-in ​​ference-for-simply-typed-lambda.html 是 Prolog 中简单类型 lambda 演算的简明定义。

看起来不错，但随后他声称将类型分配给 Y 组合器......而在非常真实的意义上，将类型添加到 lambda 演算的全部目的是拒绝为 Y 组合器之类的东西分配类型。

谁能确切地看到他的错误或 - 更有可能 - 我的误解在哪里？

我想学习类型系统理论。我在类型系统理论方面没有任何背景，所以我或多或少是个初学者（除了我读过的关于这个主题的文章，因为使用的符号我觉得很吓人）。有哪些可以让我入门的好书？我在看 Benjamin C. Pierce 的“类型和编程语言”一书。这适合初学者还是太难了？如果太难了，我还能用什么来开始我的学习？

谢谢，

--

干杯，亚历克斯

本文谈到类型和类之间的区别。由于我只使用将两者视为相同的语言，因此请建议可以教会我区别的材料/编程语言。

我记得有一个网页描述了与一些函数式编程任务相关的有趣技术。问题是我不记得那是什么了。

它有一个二叉树节点(Tree left, Tree right, Data d)作为例子，可以描述为Tree*Tree*Data, 或Tree^2*Data。然后，例如通过 推导时Tree，我们得到2*Tree*Data。

你能指点我这是做什么用的吗？

修补其他协变类的典型示例如下：

现在，如果我删除隐式协方差并手动注释类，我会得到：

（快速正确性证明：aStack[A]具有 类型的元素A，因此如果B更宽松，我们总是可以返回 anA来代替B。类似地，给定任何 堆栈A，我们可以使用它来代替B如果 B 可以接受 A 的堆栈。）

但是现在我有点困惑：这里应该有逆变，但这里的所有子类型关系似乎都是一样的。发生了什么？

为了详细说明，我们定义了一个逆变函子F，使得(a -> b) -> (F b -> F a). 特别是，函子F a是a -> r逆变的，就像(a -> b) -> ((b -> r) -> (a -> r))简单地组合函数一样。从形式主义的角度来看，我预计箭头会翻转。因此，从纯粹的句法角度来看，当没有箭头翻转时我会感到困惑（但应该有！）我编写 Scala 的注释方式仅仅是函数逆变的“自然”表示，以至于你甚至没有注意到它？我的抽象类错了吗？第二个演示文稿有什么误导性吗？

本文确定了 System F 中的类型推断（本文中称为“可类型性”）是不可判定的。我从未听说过在其他地方提到的是该论文的第二个结果，即 F 中的“类型检查”也是不可判定的。这里的“类型检查”问题的意思是：给定一个 term t、 typeT和 typing environment A，判断是否A ⊢ t : T可推导？这个问题是不可判定的（并且它等同于可打字性的问题）令我惊讶，因为直觉上它似乎应该是一个更容易回答的问题。

但无论如何，鉴于 Haskell 是基于 System F（甚至是 F-omega），关于类型检查的结果似乎表明存在 Haskell 术语t和类型T，使得编译器无法确定是否t :: T是有效的。如果是这样的话，我很好奇这样的术语和类型是什么......如果不是这样，我误解了什么？

大概理解这篇论文会导致一个建设性的答案，但我有点超出我的深度:)

我读过很多关于类型种类、更高种类的类型等等的有趣的东西。默认情况下，Haskell 支持两种类型：

• 简单类型：*
• 类型构造函数：* → *

最新 GHC 的语言扩展ConstraintKinds增加了一个新种类：

• 类型参数约束：Constraint

同样在阅读此邮件列表后，很明显可能存在另一种类型，但 GHC 不支持（但这种支持在 .NET 中实现）：

• 未装箱类型：#

我已经了解了多态类型，我想我理解这个想法。Haskell 还支持显式类型量化。

所以我的问题是：

• 是否存在任何其他类型的种类？
• 还有其他与种类相关的语言功能吗？
• 是什么subkinding意思？它在哪里实施/有用？
• 上面是否有类型系统kinds，就像kinds上面的类型系统一样types？（只是感兴趣）

我开始深入研究依赖类型编程，发现 Agda 和 Idris 语言最接近 Haskell，所以我从那里开始。

我的问题是：它们之间的主要区别是什么？类型系统在它们中是否同样具有表现力？对收益进行全面的比较和讨论会很棒。

我已经能够发现一些：

• Idris 具有类似于 Haskell 的类型类，而 Agda 具有实例参数
• Idris 包括单子和应用符号
• 它们似乎都有某种可重新绑定的语法，尽管不确定它们是否相同。

编辑：这个问题的 Reddit 页面中有更多答案：http ://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

我很难理解为什么 Scala 编译器对这个函数定义不满意：

这是REPL输出：

目标是传入 Iterable 的任何实现并获得相同类型的回退。这可能吗？

我想详细解释这个问题。在许多具有强类型系统的语言（如 Felix、Ocaml、Haskell）中，您可以通过组合类型构造函数来定义多态列表。这是 Felix 的定义：

在 Ocaml 中：

在 C 中，这是递归的，但既不是多态的也不是组合的：

在 C++ 中，如果 C++ 支持类型递归，它会这样做：

给出了元组（又名对）和变体（但不是 Boost 中使用的损坏的）的合适定义。或者：

考虑到变体的定义略有不同，可能是可以接受的。甚至不可能在 C++ < C++11 中编写它，因为没有模板类型定义，就无法获得多态性，并且没有类型定义的合理语法，就无法获得范围内的目标类型。上面的 using 语法解决了这两个问题，但这并不意味着允许递归。

特别是请注意，允许递归对 ABI 有重大影响，即名称修改（除非名称修改方案允许表示固定点，否则无法完成）。

我的问题：需要在 C++11 中工作吗？[假设扩展不会导致无限大的结构]

编辑：为了清楚起见，要求是一般结构类型。模板正好提供，例如

是匿名（结构上）类型的，并且 pair 显然是多态的。然而，不能说明 C++ < C++11 中的递归，甚至不能用指针说明。在 C++11 中，您可以声明递归，尽管使用模板 typedef（使用新的 using 语法，= 符号的 LHS 上的表达式在 RHS 的范围内）。

具有多态性和递归的结构（匿名）类型是类型系统的最低要求。

任何现代类型系统都必须支持多项式类型函子，否则类型系统太笨拙而无法进行任何高级编程。为此所需的组合子通常由类型理论家陈述，例如：

其中 1 是单元类型，* 是元组形式，+ 是变体形式，fix 是递归。这个想法很简单：

如果 t 是一个类型并且 u 是一个类型，那么 t + u 和 t * u 也是类型

在 C++ 中，struct unit{} 是 1，tuple 是 *，variant 是 +，并且可以使用 using = 语法获得固定点。这不是完全匿名的输入，因为固定点需要模板 typedef。

编辑：只是C中多态类型构造函数的一个例子：

不幸的是，在 C 中，函数值不是组合的，指针的形成受左值约束，类型组合的语法规则本身也不是组合的，但在这里我们可以说：

所以这些类型构造器（组合器）可以递归地应用来获得新类型，而不必创建新的中间类型。在 C++ 中，我们可以轻松解决语法问题：

所以现在你可以写：

语法是组合的，打字也是。