问题标签 [type-theory]

我想知道如何在类型推断期间推断强制（又名隐式转换）。我正在使用 Bastiaan Heeren 在Top Quality Type Error Messages中描述的类型推断方案，但我认为在所有 Hindley-Milner-esque 方法中的总体思路可能都是相同的。

似乎强制可以被视为一种重载形式，但本文中描述的重载方法没有考虑（至少不是以我可以遵循的方式）基于上下文对返回类型的要求的重载，即胁迫的必要条件。我还担心这种方法可能难以优先考虑身份强制，也难以尊重强制的传递闭包。我可以看到将每个可强制表达式（例如e ）添加到 coerce( e )，但是将其添加到 coerce(coerce(coerce(... coerce( e) ...))) 对于等于强制嵌套的最大嵌套的某些深度似乎很愚蠢，并且还将强制关系限制为具有有限传递闭包的东西，其深度与上下文无关，这似乎（不必要？）限制。

The Wikipedia article on Effect system is currently just a short stub and I've been wondering for a while as to what is an effect system.

• Are there any languages that have an effect system in addition to a type system?
• What would a possible (hypothetical) notation in a mainstream language, that you're familiar, with look like with effects?

Steve Yegge关于服务器端 Javascript的帖子的评论开始讨论语言中类型系统的优点，该评论描述了：

...来自HM风格系统的示例，您可以在其中获得以下内容：

你能举一个函数定义的例子（或两个？）和一个会产生该错误的函数调用吗？看起来在大型程序中调试可能非常困难。

另外，我可能在Miranda看到过类似的错误吗？（我已经 15 年没用过了，所以我对它的记忆很模糊）

是否有任何编程语言（或类型系统）可以在其中以静态类型和类型安全的方式表达以下 Python 函数（无需使用强制转换、运行时检查等）？

#1：

#2：

我正在上一门编程语言课程，“什么时候一个函数是另一个函数的子类型”的答案对我来说非常违反直觉。

澄清一下：假设我们有以下类型关系：

为什么函数是 )(real->bool)的子类型(int->bool？不应该反过来吗？

我希望子类型函数的标准是：f1 是 f2 的子类型，如果 f2 可以采用 f1 可以采用的任何参数，并且 f1 只返回 f2 返回的值。显然 f1 可以采用某些值，但 f2 不能。

在 Beyond Java（第 2.2.9 节）中，Brute Tate 声称“类型化模型”是 C++ 的问题之一。这意味着什么？

我试图更好地掌握类型如何在 lambda 演算中发挥作用。诚然，很多类型理论的东西都超出了我的想象。Lisp 是一种动态类型的语言，它会大致对应于无类型的 lambda 演算吗？还是有某种我不知道的“动态类型的 lambda 演算”？

您能否解释一下逻辑编程的基础与类型系统和常规逻辑之间的句法相似现象之间的基本联系是什么？

I am just starting to read about category theory, and would very much appreciate it if someone could explain the connection between CS contravariance/covariance and category theory. What would some example categories be (i.e. what are their objects/morphisms?)? Thanks in advance?

任何一直关注Tony Morris 的博客和 scala 练习的人都会知道这两种类型签名是等价的：

和：

此外，已经声明该类型是单独存在的（即该类型的所有实现都是完全等价的）。我可以猜测证明这两种类型的等价性，但真的不知道从哪里开始单居声明。如何证明这一点？