问题标签 [hindley-milner]

考虑从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'是它的主要类型。

我正在研究算法 W。据我了解，算法 W 以 (Γ,expr) 作为输入，其中 Γ 是上下文，而 expr 是表达式。输出是一个替代σ。然后我可以使用替换 σ 将另一个 (Γ,expr) 作为 σ(Γ,expr)。

让我困惑的是接下来要做什么。由于 expr 可以有以下情况：变量、抽象、应用程序、条件、定点表达式和 let 表达式。

有不同的 expr 案例的目的是什么？下一步我应该做什么？

我目前正在构建一个程序来使用以下 AST 在 F# 中进行类型推理：

类型推断算法如下：

我想解释一下为什么当我启动程序并在 shell 中写入以下行时：

let test = fun x -> x;;

类型推断返回的类型是'b ->'b而不是'a ->' a。

这可能是因为在类型推断的过程中，函数 generate_fresh_variable () 被调用了两次，分别为 Lamba 和 var，但我想了解如何让它以'a ->' a类型出现？

显然我接受关于如何改进代码以及如何更好地实现算法的建议，我为我缺乏经验而道歉，但这是我第一次看 F# 和类型推断。