我正在研究Scheme编译器Stalin.它既大又复杂.此外,如果我理解正确,作者正计划撰写一系列详细介绍实施方面的论文,但从未接触过这样做.
我感兴趣的斯大林方面是全局类型推断:根据它们在程序中其他地方的用法来推断事物的类型.斯大林确实这样做了吗？如果是,如何以及在其代码库中的位置？它是否使用Hindley-Milner算法的变体/扩展？
在仿射类型系统中，资源最多可以使用一次。
从 Hindley-Milner 类型系统开始，似乎强制关联的一种简单方法是在使用变量的类型规则时简单地从当前类型上下文中删除变量（如LinearML 上的这些幻灯片建议，第 15 页）。
这就是加强亲和力的全部内容吗？或者还有什么更复杂的事情要做？
我希望能够使用定点数据类型和递归方案来制定hindley-milner类型推理算法.忽略除实际递归部分之外的所有细节:
w env term = case term of
Lam n e -> lam (w (modify1 env) e)
App a b -> app (w (modify2 env) a) (w (modify3 env) b)
...
该算法在env递归遍历树直到它到达叶子时构建环境数据结构.然后它再次使用此信息建立结果.
没有这env部分,这可以很容易地实现cata.这个(with env)一般可以使用递归方案吗？
recursion haskell type-inference hindley-milner recursion-schemes
为什么printf "%d\n" 3暧昧而不是show 3？是否printf可以重写模块以提供自动消除歧义？据推测,show必须在较低层次上完成printf......或者是否存在一些重要的区别printf,show这需要消除数字的歧义？
如果printf 可以重写以自动处理数字而不明确消除歧义,那么正在show做什么？如何在show不:: Int消除歧义的情况下将数字转换为字符串printf？
这是show(没有消除歧义)的正确操作以及printf(消除歧义)的正确操作:
$ cat printStrLnShow3
import Text.Printf
main = putStrLn (show 3)
$ runghc printStrLnShow3
3
$ cat printfWithInt3
import Text.Printf
main = printf "%d\n" (3 :: Int)
$ runghc printfWithInt3
3
这里是不明确的变量时,错误printf也没有歧义的数量:
$ cat printfWithAmbiguous3
import Text.Printf
main = …我正在做一项学术练习（为了个人成长）。我想找到一种编程语言，使您可以定义能够接受自身（即，指向自身的指针）作为参数的函数。
例如，在JavaScript中：
function foo(x, y) {
if (y === 0) return;
x(x, y - 1);
}
foo(foo, 10);
上面的代码将在y达到零之前恰好执行11次foo（），从而导致递归终止。
我尝试在OCaml中定义类似的功能，如下所示：
let rec foo x y = if y < 1 then "hi" else x x (y - 1);;
但是它失败并出现类型错误：
Error: This expression has type 'a -> 'b -> 'c
but an expression was expected of type 'a
The type variable 'a occurs inside 'a -> 'b -> 'c
我想知道，是否可以在OCaml中定义这样的功能？我对OCaml特别感兴趣，因为我知道它具有全局类型推断系统。我想知道这样的功能是否与全局类型推断兼容。因此，我正在寻找任何具有全局类型推断功能的语言的示例。
ocaml type-systems type-inference hindley-milner anonymous-recursion
我正在为一种玩具语言实施算法 W。我遇到了一个我认为会进行类型检查的案例，但事实并非如此。我在 Haskell 中尝试了同样的方法，但令我惊讶的是它在那里也不起作用。
> (\id -> id id 'a') (\x -> x)
Couldn't match type ‘Char -> t’ with ‘Char’
Expected type: Char -> t
Actual type: (Char -> t) -> Char -> t
我认为这id将是多态的，但似乎不是。请注意，如果id使用 let 而不是作为参数传递定义，则此示例有效：
let id x = x in id id 'a'
'a'
:: Char
在查看算法 W 的推理规则时，这是有道理的，因为它具有 let 表达式的泛化规则。
但我想知道这是否有任何原因？函数参数不能被泛化，以便它可以多态使用吗？
I'm making a strongly typed toy functional programming language. It uses the Hindley Milner algorithm as type inference algorithm.
Implementing the algorithm, I have a question on how to infer types of the mutually recursive functions.
let rec f n = if n == 0 then 0 else g (n - 1)
let rec g n = if n == 0 then 0 else f (n - 1)
f and g are mutually recursive functions. Now, when the type checker …
compiler-construction ocaml haskell functional-programming hindley-milner
我最近一直在学习β微积分。我了解未类型化和类型化的α演算之间的区别。但是，我对Hindley-Milner类型系统和类型化α-微积分之间的区别还不太清楚。是关于参数多态性还是其他差异？
谁能清楚指出两者之间的差异（和相似之处）？
functional-programming type-inference lambda-calculus hindley-milner parametric-polymorphism
我已经看到了“给定类型签名XXX，在 Haskell 中找到实现”形式的各种问题。因此很自然地会问这是否可以推广或算法化。一个类似的问题是here。然而，很明显，通常这项任务是不可能的。所以下一个问题是用一些通用性来换取实用性。
问题：如果所有类型签名都由刚性类型变量和一些约束组成，从固定集（例如
Monad, Traversable, Foldable？）
一个典型的问题是(Monad m) => (m j -> [m d]) -> m [j] -> [m [d]]，我使用[]代替 是(..Constraints t) => t为了方便。
我读过Rust在使用Hindley-Milner时具有很好的类型推断。Rust还具有可变变量，并且当HM算法具有可变性时，AFAIK必须存在一些约束，因为它可能过于笼统。如下代码：
let mut a;
a = 3;
a = 2.5;
不进行编译，因为在第二行推断出整数，并且不能将浮点值分配给整数变量。因此，我猜测对于简单变量，一旦推断出非泛型类型，该变量就会成为单类型并且无法再进行泛化。
但是，像Vec这样的模板呢？例如此代码：
let mut v;
v = Vec::new();
v.push(3);
v.push(2.3);
这再次失败，但对于最后一行再次失败。这意味着第二行部分推断了类型（Vec），而第三行推断了容器类型。
怎么了 有我不知道的诸如价值限制之类的东西吗？还是我使事情复杂化了，Rust有更严格的规则（就像根本没有泛化一样）？
hindley-milner ×10
haskell ×5
type-systems ×3
ocaml ×2
types ×2
algorithm ×1
linear-types ×1
mutable ×1
printf ×1
recursion ×1
rust ×1
scheme ×1
type-theory ×1