问题标签 [hindley-milner]

AFAIK，Hindley-Milner 类型系统中使用的统一可以通过在构造函数位置允许类型 var 并在这种情况下放宽 arity 约束来推广以统一更高种类的类型：

我想还涉及种类，但我不知道如何。

以我的一点经验，我会说这对于高级类型的声音统一来说已经足够了。与高阶统一的主要区别可能是

• 广义的HM是可判定的，HOU不是一般的
• 广义的 HM 受到更多限制，即拒绝在 HOU 中合法的类型

虽然我以某种方式回答了我的问题，高阶统一给了我们什么，但我不知道应用高阶统一时涉及哪些（简化的）规则。该算法与广义 HM 有何不同？

我能够统一以下术语：

但是我坚持为以下统一应用正确的规则，因为foo需要一个三元函数但bar只有两个参数：

推断类型来自 GHCI。我如何到达那里？

我正在通过参加fp 课程练习来学习 Haskell。有一个问题挡住了我的去路。我不知道 Haskell 是如何推断lift2 (<$>) (,)的类型，结果如何Functor k => (a1 -> k a2) -> a1 -> k (a1, a2)。

我试过lift2 (<$>)'s type，并通过 GHCI's command 验证:t lift2 (<$>)。步骤如下。
我知道lift2 :: Applicative k => (a -> b -> c) -> k a -> k b -> k c
我也知道(<$>) :: Functor f => (m -> n) -> (f m) -> (f n)
然后通过 lambda 演算的 Beta 转换，我可以找出lift2 (<$>)的类型是
(Applicative k, Functor f) => k (m -> n) -> k (f m) -> k (f n)通过替换awith (m -> n), bwith (f m), cwith(f n)

当我要弄清楚lift2 (<$>) (,)的类型时，它阻止了我。
我知道(,) :: a -> b -> (a,b)
和lift2 (<$>) :: (Applicative k, Functor f) => k (m -> n) -> k (f m) -> k (f n)。
Haskell 是如何应用lift2 (<$>)的(,)？
的第一个变量lift2 (<$>)是Applicative k => k (m -> n)。
要应用的值是, ,(,) :: a -> b -> (a, b)
如何替换为, ?kmnab

GHCI 的答案是lift2 (<$>) (,) :: Functor k => (a1 -> k a2) -> a1 -> k (a1, a2)输入:t lift2 (<$>) (,). 我无法自己推断出这个答案。

所以我有2个问题。
1.有人可以一步一步地告诉我推论吗？
2.在这种情况下，转换似乎不是 lambda 演算中的 Beta 转换（可能是我错了）。转换是什么？

有人可以解释如何理解这个符号：

请参阅：https ://ramdajs.com/docs/#reduce

我想实现 Hindley-Milner 类型推断，但作为一个根本不了解类型理论的非学术人士，我对所有不同的算法及其属性、论文对论文的依赖以及所有内容感到有点不知所措我必须学习的新概念。

我正在寻找一种算法或一些算法，它们在它可以生成的错误消息方面脱颖而出（算法 W 和算法 M 不擅长的东西）。

任何人都可以向我指出任何有用的资源，或者向我解释我应该在算法中寻找什么，以确定它是否有利于生成错误消息，或两者兼而有之？

注意：如果它可以支持更高种类的类型会很好，但这不是一个直接的要求。

我正在阅读一个名为Frisby 教授的最充分的函数式编程指南的函数式编程教程，作者对其进行了介绍Hindley-Milner和几个示例，其中一个是：

的第一个参数reduce是一个函数，它的类型签名是b -> a -> b，这正是我不明白的部分。上面的代码是用 js 编写的，这意味着f应该接受两个参数并返回一个，如下所示：

因此，类型签名f应该是(b, a) -> b而不是b -> a -> b，对吧？f不应该是一阶函数（由 暗示b -> a -> b），至少在 js 中不应该。

所以我的问题是，这是教程的错误吗？(b, a) -> b如果是这样，在 Hindley-Milner中表示的正确方法是什么？

我正在尝试使用基于 Hindley-Milner 算法的类型推断来实现语言。但我不知道如何推断递归函数的类型：

f在这里，我必须为和一起生成和解决约束，g因为如果我早些时候为一个函数执行此操作，它将不知道另一个函数的类型。但我不能同时对模块中的所有功能执行此操作：

在fI haveh :: Int -> Int和 in gI haveh :: String -> Int中，如果我同时解决它会产生错误，但如果我将推断h之前类型的类型f和g（h :: forall a. a -> Int并且可以用于f和g不同的替换a），则不会产生错误。

我如何推断这些类型？

第 995 页上的“Haskell Programming from First Principles”的第 16 章有一个练习来手动计算类型检查的方式(fmap . fmap)。它建议将每个类型的类型替换fmap为组合运算符类型中的函数类型：

T1(.) :: (b -> c) -> (a -> b) -> a -> c

T2fmap :: Functor f => (m -> n) -> f m -> f n

T3fmap :: Functor g => (x -> y) -> g x -> g y

通过（尝试）将 T2 和 T3 代入 T1，我得出以下结论：

T4：((m -> n) -> f m -> f n) -> ((x -> y) -> g x -> g y) -> a -> c

此外，它建议检查类型(fmap . fmap)以查看最终类型应该是什么样子。

T5：(fmap . fmap) :: (Functor f1, Functor f2) => (a -> b) -> f1 (f2 a) -> f1 (f2 b)

我无法理解我应该在这里做什么。任何知识渊博的haskellers可以帮助我开始，或者提供类似练习的例子来展示如何手工计算类型？

我在这里修改算法：

https://eli.thegreenplace.net/2018/unification/

我只有一组字符串和数字的等式。例如对于以下集合 l = [('x1', 'x2'), ('x2', 'x3')] 我希望映射说例如 {x1:x2, x2:x2, x3:x2 }。相反，我得到{'x1'：'x2'，'x2'：'x3'}。

这是修改后的代码。我不担心发生检查或除常量和字符串（变量）之外的任何其他结构。

结果：{'x1': 'x2', 'x2': 'x3'}

有没有办法修改它以引用此映射范围内的相同变量？

我正在为一种玩具语言实现算法 W。我遇到了一个我想象会键入检查的案例，但没有。我在 Haskell 中尝试过同样的方法，令我惊讶的是它也没有在那里工作。

我认为这id将是多态的，但似乎并非如此。请注意，如果id使用 let 定义而不是作为参数传递，则此示例有效：

在查看算法 W 的推理规则时，这是有道理的，因为它具有 let 表达式的泛化规则。

但我想知道这是否有任何原因？函数参数不能被泛化以便可以多态使用吗？