在Idris中,我可以证明自由定理,例如`forall t类型的唯一(总)函数.t - > t`是`id`？

Question

对于足够多态的类型,参数可以唯一地确定函数本身(有关详细信息,请参阅Wadler的定理免费!).例如,唯一具有类型的总函数forall t. t -> t是标识函数id.

是否有可能在伊德里斯陈述并证明这一点？(如果在伊德里斯内部无法证明,无论如何都是真的吗？)

以下是我的尝试(我知道函数相等不是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内部表达类型的抽象属性.没有类型理论的主流实现使这成为可能. 彩色类型理论具有此功能,但它非常复杂,没有实际的实现.

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