在Idris中，我可以证明自由定理吗? forall t类型的唯一(全部)函数. t-> t是"id"吗? [英] In Idris, can I prove free theorems, e.g. the only (total) function of type `forall t. t -> t` is `id`?

问题描述

对于足够多态的类型，参数性可以唯一地确定函数本身(请参见

For sufficiently polymorphic types, parametricity can uniquely determine the function itself (see Wadler's Theorems for free! for details). For example, the only total function with type forall t. t -> t is the identity function id.

是否有可能在Idris中陈述并证明这一点? (而且，如果无法在Idris内部证明这一点，那是真的吗?)

Is it possible to state and prove this in Idris? (And if it can't be proven inside Idris, is it true anyway?)

以下是我的尝试(我知道函数相等性不是Idris中的原始概念，因此我断言，泛型t -> t的任何函数总是返回与标识函数将返回的结果相同的结果):

The following is my attempt (I know that function equality is not a primitive concept in Idris, so I assert that any function of generic type t -> t always returns the same result as the identity function would return):

%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

推荐答案

您不能.像这样的定理(自由定理")是基于这样的假设，即类型是抽象的，您无法对其进行模式匹配或以任何方式辨别其结构.但是您不能在Idris内部表达类型的抽象性.类型理论的主流实现都无法做到这一点. 彩色类型理论具有此功能，但是非常复杂，没有实际实现.

You can't. Theorems like this ("free theorem") follow from the assumption that types are abstract and you can't pattern match on them or discern their structure in any way. But you can't internally express in Idris the property of abstractness for types. No mainstream implementation of type theory makes this possible. Type theory in color has this feature but it is very complex and has no practical implementation.

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

You can still postulate the free theorems and use them, but you have to make sure that they don't block evaluation for things which you'd like to evaluate.

这篇关于在Idris中，我可以证明自由定理吗? forall t类型的唯一(全部)函数. t-> t是"id"吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！