是否有可能将自由定理作为命题的等式？

Question

Wadler的论文"免费定理"意义上的"自由定理" 关于某些值的等式是仅基于它们的类型导出的.所以,例如,

f : {A : Set} ? List A ? List A

自动满足

f . map g = map g . f

我可以接受以下类型的Agda术语:

(f : {A : Set} ? List A ? List A) {B C : Set} (g : B ? C) (xs : List B)
  ? f (map g xs) ? map g (f xs)

或者如果是这样/如果没有,我可以做更多/更少一般的事情吗？

我知道轻量级自由定理库的存在,但我认为它没有做我想要的(或者如果它确实如此,我不能很好地理解它).

(一个示例用例是我有一个仿函数,F : Set ? Set并且想要证明多态函数F A × F B ? F (A × B)自动转换.)

Answer 1

不,构建Agda的类型理论不足以证明这一点.这需要一个名为"内化参数"的功能,参见Guilhem的工作:

• Jean-Philippe Bernardy和Guilhem Moulin:参数化的计算解释(2012)
• Guilhem Moulin:具有内化参数定理的纯类型系统(2013)

这将允许您例如证明"(A:Set)→A→A"的所有居民都等于(多态)身份函数.据我所知,这还没有用任何语言实现.

Answer 2

Chantal Keller 和 Marc Lasson 为 Coq 开发了一种策略，生成与（封闭）类型相对应的参数关系，并证明该类型的居民满足生成的关系。您可以在凯勒的网站上找到有关这项工作的更多详细信息。

现在，在 Agda 的例子中，理论上可以通过使用一种称为反射的技术在纯 Agda 中实现该策略来完成相同类型的工作。