W Idris, mogę udowodnić darmowe twierdzenia, np. jedyna (całkowita) funkcja typu `forall t. t -> t` to "id"?

Question

Dla typów wystarczająco polimorficznych parametryczność może jednoznacznie określać samą funkcję (szczegóły: patrz Wadler's Theorems for free!). Na przykład jedyną pełną funkcją z typem forall t. t -> t jest funkcja identyfikacji id.

Czy można to stwierdzić i udowodnić w Idris? (A jeśli nie można tego sprawdzić w Idrisie, czy to prawda?)

Oto moja próba (wiem, że funkcja równości nie jest prymitywną koncepcją w Idris, więc twierdzę, że każda funkcja rodzaju ogólnego t -> t zawsze zwraca ten sam wynik jak funkcja tożsamości wróci):

%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 

Powstała dziura jest:

- + 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

nie możesz. Twierdzenia takie jak te ("wolne twierdzenie") wynikają z założenia, że ​​typy są abstrakcyjne i nie można ich dopasować do wzorca lub w jakikolwiek sposób rozróżnić ich struktury. Ale nie możesz wewnętrznie wyrazić w Idrisie własności abstrakcji dla typów. Żadna główna implementacja teorii typów nie czyni tego możliwym. Type theory in color ma tę funkcję, ale jest bardzo złożona i nie ma praktycznej implementacji.

Możesz nadal postulować swobodne twierdzenia i używać ich, ale musisz upewnić się, że nie blokują one oceny rzeczy, które chcesz ocenić.