Для достаточно полиморфных типов параметричность может однозначно определять сама функция (подробнее см. теоремы Вадлера бесплатно!). Например, единственной полной функцией с типом forall t. t -> t является тождественная функция id.
Можно ли утверждать и доказывать это в Идрисе? (И если он не может быть доказан внутри Идриса, это правда?)
Ниже приведена моя попытка (я знаю, что равенство функций не является примитивной концепцией в Идрисе, поэтому я утверждаю, что любая функция родового типа 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
