Dlaczego dwukropek oznacza, że ​​wartość należy do typu?

Pierce (2002) wprowadza relację pisania na stronie 92, pisząc:

Relacja typowania wyrażeń arytmetycznych, zapisana „t: T”, jest zdefiniowana przez zestaw reguł wnioskowania przypisujących typy do terminów

a przypis mówi: Symbol $\in$ jest często używany zamiast:. Moje pytanie brzmi po prostu, dlaczego teoretycy tekstu wolą używać: ponad $\in$ ? Jeśli typ jest zbiorem wartości, wówczas idealnie jest napisać , nie jest wymagana nowa notacja.$T$$t \in T$

Czy jest to podobne do tego, jak niektórzy pisarze cs wolą nawet sądząc, że jest to nadużycie zapisu i powinno być napisane ?$3n^2 = O(n^2)$$3n^2 \in O(n^2)$

Ponieważ to, co znajduje się po prawej stronie jelita grubego, niekoniecznie musi być zbiorem, a to, co jest po lewej stronie jelita grubego, niekoniecznie jest członkiem tego zestawu.

Teoria typów rozpoczęła się na początku XX wieku jako podejście do podstaw matematyki. Bertrand Russel odkrył paradoks w naiwnej teorii zbiorów i pracował nad teorią typów jako sposobem ograniczenia mocy ekspresyjnej teorii zbiorów, aby uniknąć tego (i każdego innego) paradoksu. Przez lata Russel i inni zdefiniowali wiele teorii typów. W niektórych teoriach typów typy są zestawami o określonych właściwościach, ale w innych są innym rodzajem bestii.

W szczególności wiele teorii typów ma sformułowanie składniowe . Istnieją reguły, które powodują, że coś ma typ. Kiedy reguły pisania są podstawą teorii, ważne jest, aby odróżnić to, co mówią reguły pisania od tego, co można wywnioskować, stosując dodatkową wiedzę zewnętrzną. Jest to szczególnie ważne, jeśli reguły typowania są podstawą teorii dowodu: twierdzenia, które są oparte na teorii mnogości z logiką klasyczną i aksjomatem wyboru, mogą na przykład zawierać logikę konstruktywną. Jednym z przełomowych prac z tej dziedziny jest Kościół „s preparat o prostej teorii typów (1940)

Być może sposób, w jaki rozróżnienie między typami i zestawami jest najbardziej widoczne, polega na tym, że najbardziej podstawowa reguła dla zbiorów, a mianowicie, że dwa zestawy są równe, jeśli mają te same elementy, zwykle nie ma zastosowania do typów. Zobacz odpowiedź Andreja Bauera tutaj i jego odpowiedź na powiązane pytanie w celu uzyskania przykładów. Ten drugi wątek zawiera inne odpowiedzi, które warto przeczytać.

W rachunku typowym stwierdzenie, że typy są zestawami, w rzeczywistości daje semantykę typom. Podanie rachunku semantyki teoretycznej nie jest trywialne. Załóżmy na przykład, że definiujesz język z funkcjami. Jaki zestaw jest rodzajem funkcji? Funkcje całkowite są określone na podstawie ich wykresu, jak uczymy w teorii mnogości 101. Ale co z funkcjami częściowymi? Czy chcesz nadać wszystkim nie kończącym się funkcjom tę samą semantykę? Nie można interpretować typów jako zestawów dla rachunku różniczkowego, który umożliwia funkcje rekurencyjne, dopóki nie odpowiesz na to pytanie. Nadanie językom programowania lub rachunkom denotacyjnej semantyki było trudnym problemem na początku lat siedemdziesiątych. Artykuł podsumowujący jest w kierunku semantyki matematycznej dla języków komputerowych (1971) autorstwaDana Scott i Christopher Strachey . Haskell Wikibook ma dobrą prezentację tematu.

Jak napisałem powyżej, drugą częścią odpowiedzi jest to, że nawet jeśli zdołałeś nadać typom semantykę teoretyczną, to rzecz po lewej stronie dwukropka nie zawsze jest elementem zestawu. Wartości mają typy, ale także inne rzeczy, takie jak wyrażenia i zmienne . Na przykład wyrażenie w typowym języku programowania ma typ, nawet jeśli się nie kończy. Może być skłonny do scalenia integeri $\mathbb{Z}$ , ale (x := 0; while true; do x := x + 1; x)nie jest elementem $\mathbb{Z}$ .

Nie wiem, kiedy pojawiła się notacja dwukropka dla typów. Jest teraz standardem w semantyce i powszechny w językach programowania, ale ani Russel, ani Church nie użyli go. Algol go nie używał, ale mocno inspirowany Algolem język, którym posługiwał się Pascal w 1971 roku. Podejrzewam, że nie był to pierwszy, ponieważ wiele prac teoretycznych z wczesnych lat 70. używa tego zapisu, ale nie znam wcześniejsze użycie. Co ciekawe, nastąpiło to wkrótce po ujednoliceniu koncepcji typów z programowania i logiki - jak pokazuje Simon Martini w kilku typach typów w językach programowania , tak zwany „typ” w językach programowania do lat sześćdziesiątych pochodzi z języka ojczystego użycie słowa, a nie z teorii typów.

Głównym powodem preferowania zapisu dwukropka $t : T$ od relacji członkostwa $t \in T$ jest to, że relacja członkostwa może wprowadzać w błąd, ponieważ typy nie są (tylko) kolekcjami .

[ Uzupełnienie: Należy zauważyć, że teoria typów historycznych została napisana przy użyciu $\in$ . Koncepcja typu Martina-Löfa miała konstruktywnie wychwytywać zbiory, a Russell i Whitehead już używali $\epsilon$ do członkostwa w klasie. Interesujące byłoby wyśledzenie momentu, w którym $:$ stał się bardziej rozpowszechniony niż $\in$ .]

Typ opisuje pewien rodzaj konstrukcji, tj. Jak tworzyć obiekty o określonej strukturze, jak z nich korzystać i jakie równania się z nimi wiążą.

Na przykład typ produktu $A \times B$ ma zasady wprowadzania, które wyjaśniają, jak tworzyć uporządkowane pary, oraz zasady eliminacji wyjaśniające, że możemy rzutować pierwszy i drugi komponent z dowolnego elementu$A \times B$ . Definicja$A \times B$ jestniezaczynają się od słów „zbierania wszystkich ...” i nie robi to znaczy nigdzie czegoś podobnego „wszystkie elementy$A \times B$ są pary” (ale tonastępujez definicji, że każdy element$A \times B$ jestpropozycjonalnierówna parze). Przeciwnie, teoretyczna definicja $X \times Y$ jest określona jako „zbiór wszystkich uporządkowanych par ...”.

Oznaczenie $t : T$ , oznacza, że $t$ ma strukturę opisaną przez $T$ .

Typ $T$ nie należy mylić z jego przedłużeniem , która stanowi zbiór wszystkich obiektów typu $T$ . Typ nie jest określony przez jego rozszerzenie, tak jak grupa nie jest określona przez jego zestaw nośny. Ponadto może się zdarzyć, że dwa typy mają to samo rozszerzenie, ale są różne, na przykład:

1. Rodzaj wszystkich parzystych liczb pierwszych większych niż dwa: $\Sigma (n : \mathbb{N}) . \mathtt{isprime}(n) \times \mathtt{iseven}(n) \times (n > 2)$ .
2. Rodzaj wszystkich liczb nieparzystych mniejszych niż dwa: $\Sigma (n : \mathbb{N}) . \mathtt{isprime}(n) \times \mathtt{isodd}(n) \times (n < 2)$ .

Rozszerzenie obu jest puste, ale nie są tego samego typu.

Istnieją dalsze różnice między teorią typu $:$ a teorią zbioru $\in$ . Obiekt w teorii mnogości istnieje niezależnie od tego, co określa ona należy, a może należeć do kilku zestawów. W przeciwieństwie do większości teorie typu zaspokoić wyjątkowość wpisywać: jeśli t : T i t : U ówczesnego T ≡ U . Innymi słowy, konstrukcja teoretyczna typu t ma dokładnie jeden typ T , aw rzeczywistości nie ma sposobu, aby mieć tylko obiekt t bez jego (jednoznacznie określonego) typu.$a$$t : T$$t : U$$T \equiv U$$t$$T$$t$

Inną różnicą jest to, że w teorii mnogości możemy zaprzeczyć faktu, że ∈ pisząc ¬ ( ∈$a \in A$$\lnot (a \in A)$ lub$a \not\in A$ . Nie jest to możliwe w teorii typów, ponieważ$t : T$ jestosądem,który można uzyskać na podstawie reguł teorii typów, ale w teorii typów nie ma niczego, co pozwalałoby stwierdzić, że coś nie zostało wyprowadzone. Kiedy dziecko robi coś z klocków LEGO, z dumą biegnie do rodziców, aby pokazać im konstrukcję, ale nigdy nie biegnie do rodziców, aby pokazać im, czego nie zrobili.

Björn,

Prawdopodobnie istnieje wcześniejsze odniesienie, ale z jednej strony dwukropek był używany w języku programowania Pascal: