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

Question

鉴于这两个程序（用JavaScript编写）＆hellip;

// 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的实现，它很容易和hellip;我们可以通过整个评估使用替代模型来得到扩展的表达式hellip;

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)) 
... keep going until ... 
= f=> g=> x=> y=> f (g (x) (y))

环一鼎。扩展评估匹配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) 

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

有一定的办法吧？这不是什么algebraic data types是关于什么？

---

让我们来看一个简单的例子来阐明我的问题：如果我们有像add和map＆hellip功能;

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

如果我们想用map和add定义一个函数，我们可以计算出类型系统不知道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 

HOW TO辛德雷MILNER

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 

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