In Idris, can I prove free theorems, e.g. the only (total) function of type `forall t. t -> t` is `id`?

13
votes

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.

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

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

The resulting hole is:

- + 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
1
idrisparametric-polymorphismfree-theorem

1 Answers

16
votes

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.