javascript - 如何根据其实现派生过程的 HM 类型？

Question

给定这两个程序(用 JavaScript 编写)......

// comp :: (b -> c) -> (a -> b) -> (a -> c)
const comp = f=> g=> x=> f (g (x))

// comp2 :: (c -> d) -> (a -> b -> c) -> (a -> b -> d)
const comp2 = comp (comp) (comp)

我的问题是如何导出comp2的Hindley-Milner Type 没有引用comp的实现

---

如果我们知道 comp 的实现，就很容易了……我们可以在整个求值过程中使用替换模型来得到扩展表达式……

comp (comp) (comp)
= (f => g => x => f (g (x))) (comp) (comp) 
= x => comp (comp (x))
= y => comp (comp (y)) 
= y => (f => g => x => f (g (x))) (comp (y))
<em>... keep going until ...</em>
<b>= f=> g=> x=> y=> f (g (x) (y))</b>

铃声响起。扩展的评估匹配 comp2 的类型。没有人留下深刻印象。

// comp2 :: (c -> d) -> (a -> b -> c) -> (a -> b -> d)
const comp2 = f=> g=> x=> y=> f (g (x) (y))

但是，如果我们只知道 comp 的类型而不知道它的实现会怎么样？除了评估代码以确定类型，我是否可以对 comp 的类型执行某种替换/评估以最终得到 comp2 的类型？

---

仅鉴于此，问题就变得更加困难……(至少对我而言)

// comp :: (b -> c) -> (a -> b) -> (a -> c)

<b>// comp2 :: ???</b>
const comp2 = comp (comp) (comp)

总有办法吧？这不就是algebraic data types吗都是关于什么？

---

让我们看一个简化的例子来澄清我的问题:如果我们有像 add 和 map 这样的函数......

// add :: Number -> Number -> Number
// map :: (a -> b) -> [a] -> [b]

如果我们想使用 map 和 add 定义一个函数，我们可以在不知道 的情况下系统地 找出类型添加或map的实现

// add :: Number -> Number -> Number
// map :: (a -> b) -> [a] -> [b]

// add6 :: Number -> Number
let add6 = add (6) 

// mapAdd6 :: [Number] -> [Number]
let mapAdd6 = map(add6)

这真的很强大，因为它允许你推理你没有编写的代码，而不必深入研究实现(尽可能多)

但是，当尝试使用 comp2 示例执行此操作时，我很快就卡住了

// comp :: (b -> c) -> (a -> b) -> (a -> c)

// comp2 :: ??
const comp2 = comp (comp) (comp)

// initial type
(b -> c) -> (a -> b) -> (a -> c)

// apply to comp once ... ???
[(b -> c) -> (a -> b) -> (a -> c)] -> (a -> b) -> (a -> c)

// apply the second time ... ???
[(b -> c) -> (a -> b) -> (a -> c)] -> [(b -> c) -> (a -> b) -> (a -> c)] -> (a -> c)

// no... this can't be right

如何去亨德利·米尔纳

Answer 1

让我们看看我们知道什么。让我们单独看一下 comp2 的实现:

comp2 = comp comp comp

让我们考虑一下 comp 的类型签名:

comp :: (b -> c) -> (a -> b) -> (a -> c)

现在，comp2 的结果将是 comp 应用于两个参数的结果，这是 comp< 的最右侧 类型签名。因此，我们知道comp2的类型是a -> c类型，只是不知道a和是什么c 还没有。

但是，我们可以弄清楚。我们可以通过手动统一类型(通过知道两种类型需要相同)，然后替换已知类型变量为其具体类型来手动解决这个问题。这两个参数都是comp，但它们应该有不同的类型:分别是b -> c 和a -> b。让我们添加一些类型注释以使其更加清晰:

comp2 = (comp (comp :: b -> c)
              (comp :: a -> b))

我们可以先尝试统一b -> c和comp的类型来确定b和c 是，但是我们需要做一些字母重命名，这样我们的变量名就不会冲突:

b          -> c
(b1 -> c1) -> (a1 -> b1) -> (a1 -> c1)

b = b1 -> c1
c = (a1 -> b1) -> (a1 -> c1)

接下来，我们可以对第二个参数做同样的事情，统一为 a -> b 类型:

a          -> b
(b2 -> c2) -> (a2 -> b2) -> (a2 -> c2)

a = b2 -> c2
b = (a2 -> b2) -> (a2 -> c2)

但是等等!我们现在对同一类型变量 b 有两个不同的定义，因此它们也必须统一。让我们对这两种类型执行相同的过程:

b1         -> c1
(a2 -> b2) -> (a2 -> c2)

b1 = a2 -> b2
c1 = a2 -> c2

现在，回到我们为 comp2 提供的原始类型，我们可以执行一系列替换以得到一个完整的类型:

a -> c                                                 | type of comp2, from the return type of comp
(b2 -> c2) -> c                                        | substituting the definition of a
(b2 -> c2) -> (a1 -> b1) -> (a1 -> c1)                 | substituting the definition of c
(b2 -> c2) -> (a1 -> (a2 -> b2)) -> (a1 -> c1)         | substituting the definition of b1
(b2 -> c2) -> (a1 -> (a2 -> b2)) -> (a1 -> (a2 -> c2)) | substituting the definition of c1
(b2 -> c2) -> (a1 -> a2 -> b2) -> a1 -> a2 -> c2       | removing unnecessary parentheses
(c -> d) -> (a -> b -> c) -> a -> b -> d               | alpha renaming

您会注意到这与您手动指定的类型相同。