İdris'te, serbest teoremleri, örn. forall t türünün tek (toplam) işlevi. t -> t 'id' nedir?

Question

Yeterli polimorfik tipler için parametriklik, fonksiyonun kendisini benzersiz şekilde belirleyebilir (ayrıntılar için bkz. Wadler's Theorems for free!). Örneğin, forall t. t -> t tipindeki tek toplam işlev, id kimlik işlevidir.

Bunu Idris'da belirtip ispatlamak mümkün mü? (Ve eğer İdris'in içinde kanıtlanamazsa, bu zaten doğru mu?)

Aşağıdakiler benim girişimdir (fonksiyon eşitliğinin İdriste ilkel bir kavram olmadığını biliyorum, bu yüzden jenerik tipin herhangi bir işlevini ileri sürüyorum) kimlik işlevi dönecekti olarak t -> t her zaman) aynı sonucu verir:

%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 

çıkan delik:

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

yapamazsın. Bu gibi teoremler ("serbest teorem"), türlerin soyut olduğu ve kalıpların eşleşmediği veya yapısını herhangi bir şekilde ayırt edemeyeceği varsayımından gelir. Ancak, İdris'te, türler için soyut olma özelliğini içsel olarak ifade edemezsiniz. Tip teorisinin ana akım uygulaması bu durumu mümkün kılmaz. Type theory in color bu özelliğe sahiptir, ancak çok karmaşıktır ve pratik bir uygulaması yoktur.

Yine de ücretsiz teoremleri postüle edebilir ve bunları kullanabilirsiniz, ancak değerlendirmek istediğiniz şeylerin değerlendirmesini engellemediğinden emin olmanız gerekir.