多态推理

Question

我正在学习哈斯克尔，在互联网上，我从菲利普·瓦德勒那里找到了paper。

我读了它，一点也不理解，但它以某种方式与多态函数联系在一起。

例如：

polyfunc :: a -> a -> a

它是任何类型的多态函数。

与示例polyfunc相关的自由定理是什么

Answer 1

我觉得如果我真的理解了那篇论文，那么我写的任何代码都将是上帝的合著。

不过，我对这个问题的最好猜测是，polyfunc所能做的要么总是返回第一个参数，要么总是返回第二个参数。所以实际上只有两种polyfunc实现，

polyfuncA a _ = a
polyfuncB _ b = b

这篇论文为你提供了一种证明这一说法的方法。

这是一个非常重要的概念。例如，我以前参与过数据质量研究。这个自由定理说，没有函数可以从两个任意数据片段中选择最佳数据。我们需要知道更多的东西。事实上，我惊讶地发现有些人愿意忽视这一点，这是显而易见的。

Answer 2

我也从来没有真正理解过那篇论文中提出的算法，所以我想我应该试着弄清楚它。

(1) Type of function in question
f :: a -> a -> a

(2) Rephrasing as a relation
f : ∀X. X -> X -> X

(3) By parametricity
(f, f) ∈ ∀X. X -> X -> X

(4) By definition of ∀ on relations
for all Q : A <=> A',
  (fA, fA') ∈ Q -> Q -> Q

(5) Applying definition of -> on relations to the first -> in (4)
for all Q : A <=> A',
  for all (x, x') ∈ Q,
    (fA x, fA' x') ∈ Q -> Q

(6) Applying definition of -> on relations to (5)
for all Q : A <=> A',
  for all (x, x') ∈ Q,
    for all (y, y') ∈ Q,
      (fA x y, fA' x' y') ∈ Q

在这一点上，我已经完成了关系定义的扩展，但不确定如何将其从关系中恢复到函数和类型方面，因此我找到了一个将automatically derive the free theorem for a type的webapp。我不会破坏它给出的结果，但看看它确实帮助我弄清楚了我的证明中的下一步。

下一步是从关系域返回到函数域，注意Q可以是任何函数的类型，并且仍然有效。

(7) Specializing Q to a function g :: p -> q
for all p, q
  for all g :: p -> q
    where g x = x'
      and g y = y'
        g (f x y) = f x' y'

(8) By definitions of x' and y'
for all p, q
  for all g :: p -> q
    g (f x y) = f (g x) (g y)

看起来是真的，对吧？这相当于使用g转换这两个元素，然后让f在它们之间进行选择，或者让f选择一个元素，然后用g转换它。通过参数化，f不能根据g所做的任何事情来改变它是选择left还是right元素。

当然，特雷弗·库克的答案中的说法是正确的：f要么总是选择第一个参数，要么总是选择第二个参数。我不确定我导出的自由定理是否等同于它，或者是它的一个较弱的版本。

顺便说一句，这是论文中已经明确介绍的东西的一个特例。它给出了一个定理

k :: x -> y -> x

当然，这与您的函数f相同，其中包含x ~ a和y ~ a。它给出的结果与我描述的结果是一样的：

for all a, b, x, y
  a (k x y) = k (a x) (b y)

如果我们选择b=a来使两个结果等价。