Dlaczego funkcja typu polimorficznego `forall t: Type, t-> t` musi być funkcją tożsamości?

Jestem nowy w teorii języków programowania. Oglądałem kilka wykładów online, w których instruktor twierdził, że funkcją typu polimorficznego forall t: Type, t->tjest tożsamość, ale nie wyjaśniłem dlaczego. Czy ktoś może mi wyjaśnić, dlaczego? Może dowód roszczenia z pierwszych zasad.

Pierwszą rzeczą do odnotowania jest to, że niekoniecznie jest to prawda. Na przykład, w zależności od języka, funkcja tego typu, oprócz tego, że jest funkcją tożsamości, może: 1) zapętlać na zawsze, 2) mutować jakiś stan, 3) zwracać null, 4) zgłaszać wyjątek, 5) wykonywać pewne operacje we / wy, 6) rozwiąż wątek, aby zrobić coś innego, 7) zróbcall/cc shenanigany, 8) użyj czegoś takiego jak Java Object.hashCode, 9) użyj odbicia, aby określić, czy typ jest liczbą całkowitą i zwiększ go, jeśli tak, 10) użyj odbicia, aby przeanalizować stos wywołań i zrobić coś w oparciu o kontekst, w którym się nazywa, 11) prawdopodobnie wiele innych rzeczy, a na pewno dowolne kombinacje powyższych.

Zatem właściwość, która do tego prowadzi, parametryczność, jest właściwością języka jako całości i istnieją jego silniejsze i słabsze odmiany. W przypadku wielu formalnych rachunku różniczkowego badanych w teorii typów nie może wystąpić żadne z powyższych zachowań. Na przykład dla Systemu F / czystego polimorficznego rachunku lambda, w którym najpierw badano parametryczność, żadne z powyższych zachowań nie może wystąpić. Po prostu nie ma wyjątków, stan zmienny,null , call/cc, I / O, odbicie, i to mocno normalizacji więc nie może pętla zawsze. Jak wspomniał Gilles w komentarzu, artykuł Twierdzenia za darmo!Phila Wadlera jest dobrym wstępem do tego tematu, a jego odniesienia przejdą dalej do teorii, a zwłaszcza techniki relacji logicznych. Ten link zawiera również kilka innych artykułów Wadlera na temat parametryczności.

Ponieważ parametryczność jest właściwością języka, udowodnienie, że wymaga ona formalnego sformułowania języka, a następnie stosunkowo skomplikowanego argumentu. Nieformalny argument w tym konkretnym przypadku, zakładając, że jesteśmy w polimorficznym rachunku lambda, jest taki, że ponieważ nic nie wiemy o tym, tnie możemy wykonać żadnych operacji na danych wejściowych (np. Nie możemy go zwiększyć, ponieważ nie wiemy, czy jest to liczba) lub utwórz wartość tego typu (dla wszystkich wiemy t= Voidtyp bez żadnych wartości). Jedynym sposobem na wygenerowanie wartości typu tjest zwrócenie tej, która została nam przekazana. Żadne inne zachowania nie są możliwe. Jednym ze sposobów, aby to zobaczyć, jest zastosowanie silnej normalizacji i wykazanie, że istnieje tylko jeden normalny termin tego typu.

Dowód roszczenia jest dość złożony, ale jeśli tego naprawdę chcesz, możesz sprawdzić oryginalny artykuł Reynoldsa na ten temat.

Kluczową ideą jest to, że odnosi się do parametrycznie polimorficznych funkcji, gdzie ciało funkcji polimorficznej jest takie samo dla wszystkich monomorficznych instancji funkcji. W takim systemie nie można przyjąć żadnych założeń dotyczących typu parametru typu polimorficznego, a jeśli jedyna wartość w zakresie ma typ ogólny, nie ma z tym nic wspólnego, ale zwraca go lub przekazuje innym funkcjom Zdefiniowaliśmy, że z kolei nie można nic zrobić, tylko zwrócić go lub przekazać .. .etc. Ostatecznie wszystko, co możesz zrobić, to łańcuch funkcji tożsamości przed zwróceniem parametru.

Biorąc pod uwagę wszystkie zastrzeżenia, o których wspomina Derek, i ignorując paradoksy wynikające z zastosowania teorii mnogości, pozwól mi naszkicować dowód w duchu Reynoldsa / Wadlera.

Funkcja typu:

f :: forall t . t -> t

jest rodziną funkcji indeksowanych według typu t .$f_t$$t$

Chodzi o to, że aby formalnie zdefiniować funkcje polimorficzne, nie powinniśmy traktować typów jako zbiorów wartości, ale raczej jako relacje. Podstawowe typy, takie jak Intindukują relacje równości - np. Dwie Intwartości są powiązane, jeśli są równe. Funkcje są powiązane, jeśli odwzorowują powiązane wartości na powiązane wartości. Ciekawym przypadkiem są funkcje polimorficzne. Mapują typy pokrewne na powiązane wartości.

W naszym przypadku, chcemy nawiązać relację między dwie funkcje polimorficzne i g typu:$f$$g$

forall t . t -> t

$s$$t$$f$$s$$f_s$$s \to s$$t$$g_t$$t \to t$$f$$g$$f_s$$g_t$

fst$f_s$$f_t$

()()t()t((), c)ct$f_{(\,)}$$f_t$$f_{(\,)}$()()$f_t$cc()c$f_t$$id_t$tfid

Więcej szczegółów znajdziesz na moim blogu .

EDYCJA: Powyższy komentarz podał brakujący element. Niektórzy ludzie celowo bawią się w mniej niż kompletne języki. Wyraźnie nie dbam o takie języki. Naprawdę łatwy do opanowania język nie jest szalony i trudny do zaprojektowania. Cała reszta omawia to, co się dzieje, próbując zastosować te twierdzenia do pełnego języka.

Fałszywy!

function f(a): forall t: Type, t->t
    function g(a): forall t: Type, t->t
       return (a is g) ? f : a
    return a is f ? g : a

gdzie isoperator porównuje dwie zmienne dla tożsamości referencyjnej. Oznacza to, że zawierają tę samą wartość. Nie jest to wartość równoważna, ta sama wartość. Funkcje fi gsą z definicji równoważne, ale nie są takie same.

Jeśli ta funkcja zostanie przekazana sama, zwraca coś innego; w przeciwnym razie zwraca dane wejściowe. Coś innego ma ten sam typ, co sam, dlatego można je zastąpić. Innymi słowy, ftożsamość nie jest, ponieważ f(f)zwraca g, podczas gdy tożsamość powraca f.

Aby twierdzenie się utrzymało, musi ono przyjąć absurdalną zdolność redukcji

function cantor(n, <z, a>) : forall t: t: Type int, <int, t> -> <int, t>
    return n > 1 ? cantor((n % 2 > 0) ? (n + 1) : n / 2, <z + 1, a>) : <z, a>
return cantor(1000, <0, a>)[1]¹

Jeśli zechcesz założyć, że możesz założyć, że łatwiejsze jest wnioskowanie o typie.

Jeśli spróbujemy ograniczyć domenę, dopóki twierdzenie się nie utrzyma, ostatecznie musimy ją okropnie ograniczyć.

• Pure Functional (bez stanu zmiennego, bez IO). OK, mogę z tym żyć. Dużo czasu chcemy przeprowadzać testy funkcji.
• Opróżnij standardową bibliotekę. meh
• Nie raise i nie exit. Teraz zaczynamy się ograniczać.
• Nie ma typu dna.
• Język ma regułę, która pozwala kompilatorowi zwinąć nieskończoną rekurencję, zakładając, że musi się zakończyć. Kompilator może odrzucać trywialną nieskończoną rekurencję.
• Kompilator może zawieść, jeśli zostanie zaprezentowany z czymś, czego nie można udowodnić w żaden sposób. ² Teraz biblioteka standardowa nie może przyjmować funkcji jako argumentu. Gwizd.
• Nie ma nil. To zaczyna być problematyczne. Skończyły się nam sposoby radzenia sobie z 1 / 0.³
• Język nie może dokonywać wnioskowania typu rozgałęzienia i nie ma przesłonięcia, gdy programiści mogą udowodnić wnioskowanie typu, którego nie może język. To jest całkiem złe.

Istnienie obu ostatnich dwóch ograniczeń okaleczyło język. Mimo że Turing jest kompletnym jedynym sposobem na uzyskanie z niego ogólnego celu, jest symulacja wewnętrznej platformy, która interpretuje język o luźniejszych wymaganiach.

¹ Jeśli uważasz, że kompilator może to wywnioskować, wypróbuj ten

function fermat(z) : int -> int
    function pow(x, p)
        return p = 0 ? 1 : x * pow(x, p - 1)
    function f2(x, y, z) : int, int, int -> <int, int>
        left = pow(x, 5) + pow(y, 5)
        right = pow(z, 5)
        return left = right
            ? <x, y>
            : pow(x, 5) < right
                ? f2(x + 1, y, z)
                : pow(y, 5) < right
                    ? f2(2, y + 1, z)
                    : f2(2, 2, z + 1)
    return f2(2, 2, z)
function cantor(n, <z, a>) : forall t: t: Type int, <int, t> -> <int, t>
    return n > 1 ? cantor((n % 2 > 0) ? (n + 1) : n / 2, <z + 1, a>) : <z, a>
return cantor(fermat(3)[0], <0, a>)[1]

² Dowód, że kompilator nie może tego zrobić, zależy od oślepienia. Możemy użyć wielu bibliotek, aby kompilator nie widział pętli jednocześnie. Ponadto zawsze możemy zbudować coś, co program działałby, ale nie można go skompilować, ponieważ kompilator nie może wykonać indukcji dostępnej pamięci.

³ Ktoś myśli, że możesz mieć ten zerowy zero bez arbitralnych typów ogólnych zwracających zero. To płaci okropną karę, za którą nie widziałem skutecznego języka, który mógłby ją zapłacić.

function f(a, b, c): t: Type: t[],int,int->t
    return a[b/c]

nie można kompilować. Podstawowym problemem jest to, że indeksowanie tablicy wykonawczej już nie działa.