Jak można motywować relacyjną parametryczność?

Czy istnieje jakiś naturalny sposób na zrozumienie istoty semantyki relacyjnej polimorfizmu parametrycznego?

Właśnie zacząłem czytać o pojęciu parametryczności relacyjnej, a la John Reynolds „Typy, abstrakcja i polimorfizm parametryczny” i mam problem ze zrozumieniem, w jaki sposób motywowana jest semantyka relacyjna. Zestaw semantyki ma dla mnie idealny sens i zdaję sobie sprawę, że semantyka zestawu jest niewystarczająca do opisania polimorfizmu parametrycznego, ale skok do semantyki relacyjnej wydaje się magiczny, pochodzący całkowicie znikąd.

Czy istnieje jakiś sposób wyjaśnienia tego w następujący sposób: „Załóżmy relacje na podstawowych typach i terminach, a następnie interpretacja pochodnych terminów jest po prostu naturalną relacją między … a taką naturalną rzeczą… w twoim języku programowania „? Lub jakieś inne naturalne wytłumaczenie?

Cóż, parametryczna relacja jest jednym z najważniejszych pomysłów wprowadzonych przez Johna Reynoldsa, więc nie powinno być zaskoczeniem, że wygląda jak magia. Oto bajka o tym, jak mógł ją wymyślić.

Załóżmy, że próbujesz sformalizować pogląd, że niektóre funkcje (tożsamość, mapa, składanie, odwracanie list) działają „tak samo na wielu typach”, tzn. Masz intuicyjne wyobrażenia o polimorfizmie parametrycznym i sformułowałeś pewne reguły do tworzenia takich map, tj. polimorficznego -calculus lub jego wczesnego wariantu. Zauważasz, że naiwna semantyka teoretyczna nie działa.$\lambda$

Na przykład patrzymy na typ który powinien zawierać tylko mapę tożsamości, ale naiwna semantyka teoretyczna zestawu pozwala na niepożądane funkcje, takie jak Aby wyeliminować tego rodzaju rzeczy, musimy nałożyć pewne dodatkowe warunki na funkcje. Na przykład, moglibyśmy wypróbować teorię domen: wyposażyć każdy zestaw w częściowy porządek i wymagać, aby wszystkie funkcje były monotoniczne. Ale to nie całkiem go ogranicza, ponieważ powyższa niepożądana funkcja jest stała lub identyczna, w zależności od , a są to mapy monotoniczne.

Częściowy porządek $\leq$ jest relatywny, przechodni i antysymetryczny. Możemy spróbować zmienić strukturę, na przykład możemy spróbować zastosować ścisły porządek częściowy, porządek liniowy, relację równoważności lub po prostu relację symetryczną. Jednak w każdym przypadku wkradają się niechciane przykłady. Na przykład relacje symetryczne eliminują naszą niechcianą funkcję, ale pozwalają na inne funkcje uwarunkowane (ćwiczenie).

A potem zauważasz dwie rzeczy:

1. Do chcieli przykłady nie są eliminowane, co stosunki użyć zamiast częściowych zamówień $\leq$ .
2. Dla każdego konkretnego niechcianego przykładu, na który patrzysz, możesz znaleźć relację, która go eliminuje, ale nie ma jednej relacji, która eliminowałaby wszystkie z nich.

Zatem masz genialną myśl, że pożądanymi funkcjami są te, które zachowują wszystkie relacje , i rodzi się model relacyjny.

Odpowiedź na twoje pytanie znajduje się w bajce Reynoldsa (część 1). Pozwól, że spróbuję to dla ciebie zinterpretować.

W języku lub formalizmie, w którym typy są traktowane jako abstrakcje , zmienna typu może oznaczać dowolne pojęcie abstrakcyjne. Nie zakładamy, że typy są generowane za pomocą jakiejś składni terminów typu lub jakiegoś stałego zbioru operatorów typów, lub że możemy przetestować dwa typy pod kątem równości itp. W takim języku, jeśli funkcja obejmuje zmienną typu, wówczas jedyna rzeczą, którą funkcja może zrobić z wartościami tego typu, jest tasowanie wokół podanych wartości. Nie może wymyślić nowych wartości tego typu, ponieważ nie „wie”, co to za typ! To intuicyjna koncepcja parametryczności .

$t$$A$$A'$$R : A \leftrightarrow A'$$x \in A$$x' \in A'$$x$$x'$$R$$t$$x$$x'$$R$$x$$x'$

$A$$A'$$A$$A'$$A'$$A$

$R$$I_K$$K$$t \times Int \to Int \times t$$R \times I_{Int} \to I_{Int} \times R$$f$$(x,n)$$(x',n)$$(m,x)$$(m,x')$$F(I_{A_1},\ldots,I_{A_n}) = I_{F(A_1,\ldots,A_n)}$ własność.

$t \to t$$t \to Int$$Int \to t$$t \times t \to t \times t$$(t \to t) \to t$$(t \to t) \to (t \to t)$

$\omega$

Ponadto kuszące jest identyfikowanie funkcji o tym samym zachowaniu ekstensywnym, co prowadzi do relacji równoważności. Relacja jest częściowa, jeśli wykluczymy funkcje „niezdefiniowane”, czyli funkcje, które „zapętlają” się w przypadku niektórych dobrze sformułowanych danych wejściowych.

Modele PER są uogólnieniem tego.

Innym sposobem na zobaczenie tych modeli jest (bardzo) specjalny przypadek prostego zestawu modeli teorii typów homotopii . W tych ramach typy są interpretowane jako (uogólnienie), zestawy ze relacjami oraz relacje między tymi relacjami itp. Na najniższym poziomie mamy po prostu modele PER.

Wreszcie, w dziedzinie matematyki konstruktywnej pojawiły się pokrewne pojęcia, w szczególności Teoria zbiorów biskupa obejmuje opisanie zbioru poprzez podanie zarówno elementów, jak i wyraźnej relacji równości, która musi być równoważna. Naturalne jest oczekiwanie, że niektóre zasady matematyki konstruktywnej wkroczą do teorii typów.