2

鉴于这两个程序（用 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 类型 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))
... 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)

总有办法吧？这不就是代数数据类型的全部意义吗？

让我们看一个简化的例子来澄清我的问题：如果我们有一个类似addand的函数map......

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

如果我们想定义一个函数 usingmap并且我们可以在不知道or的实现的情况下系统地add找出类型 addmap

// 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

HINDLEY MILNER 如何

4

1 回答 1

3

让我们看看我们知道什么。让我们单独看看comp2's 的实现：

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是什么，但是我们需要做一些 alpha 重命名，这样我们的变量名就不会发生冲突：

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

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

接下来，我们可以对第二个参数做同样的事情，统一 type 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

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

于 2016-07-31T10:23:39.743 回答