idris - 在 Idris 中，我可以证明自由定理吗，例如类型为 `forall t. 的唯一（总）函数。t -> t` 是`id`？

Question

对于足够多态的类型，参数性可以唯一地确定函数本身（详情请参阅Wadler定理！）。例如，唯一具有类型的总函数forall t. t -> t是恒等函数id。

是否有可能在 Idris 中陈述和证明这一点？（如果它不能在 Idris 内部得到证明，那是真的吗？）

以下是我的尝试（我知道函数相等不是 Idris 中的原始概念，所以我断言任何泛型类型的函数t -> t总是返回与恒等函数返回的结果相同的结果）：

%default total

GenericEndomorphism: Type
GenericEndomorphism = (t: Type) -> (t -> t)

id_is_an_example : GenericEndomorphism
id_is_an_example t = id

id_is_the_only_example : (f : GenericEndomorphism) -> (t : Type) -> (x : t) -> f t x = x
id_is_the_only_example f t x = ?id_is_the_only_example_rhs

产生的洞是：

- + Main.id_is_the_only_example_rhs [P]
 `--                                f : GenericEndomorphism
                                    t : Type
                                    x : t
     -------------------------------------------------------
      Main.id_is_the_only_example_rhs : f t x = x

Answer 1

你不能。像这样的定理（“自由定理”）遵循以下假设：类型是抽象的，您无法对它们进行模式匹配或以任何方式辨别它们的结构。但是你不能在 Idris 内部表达类型的抽象属性。没有类型理论的主流实现使这成为可能。 颜色中的类型理论有这个特点，但它非常复杂，没有实际的实现。

您仍然可以假设自由定理并使用它们，但您必须确保它们不会阻止对您想要评估的事物的评估。