Warum brauchen wir eine separate Notation für П-Typen?

Question

Hauptsächlich

Ich bin verwirrt über die Motivation hinter der Notwendigkeit einer separaten Notation für П-Typen, die man in Typsystemen ab λ2 finden kann.Die Antwort lautet normalerweise so: Überlegen Sie, wie man eine Signatur einer Identitätsfunktion darstellen kann – das kann sein λa:type.λx:a.x oder λb:type.λx:b.x.Der subtile Teil, sagen sie, ist, dass diese beiden Signaturen nicht nur not equal, Sie sind als Typvariablen nicht alphaäquivalent a Und b sind freie Variablen innerhalb ihrer entsprechenden Abstraktionen.Um dieses lästige syntaktische Problem zu lösen, stellen wir einen П-Ordner vor, der gut mit der Alpha-Konvertierung zusammenarbeitet.

Also die Frage:Warum das?Warum nicht einfach den Begriff der Alpha-Äquivalenz korrigieren?

UPDATE z:

Oh, dumm von mir, λa:type.λx:a.x Und λb:type.λx:b.x sind Alpha-äquivalent.Aber warum a:type -> a -> a Und b:type -> b -> b dann nicht.

UPDATE erfolgreich:

Aha, interessant, ich denke, das ist ein perfektes Beispiel für selektive Blindheit =D

Ich lese das buch Typentheorie und formaler Beweis, und im Kapitel über Lambda2 begründet der Autor die Existenz von П Mit genau dieser Argumentation kann man das nicht sagen \t:*.\v:t.v : * -> t -> t weil dies zwei alphaäquivalente Terme ergibt\t:*.\v:t.v Und \g:*.\v:g.v haben unterschiedliche Typen, da entsprechende Typen nicht alpha-äquivalent sind, während Typen wie t:* -> t -> t sind tatsächlich alpha-invariant. Beachten Sie den Unterschied zwischen t:* -> t -> t Und * -> t -> t.Aber macht es dieses Argument nicht etwas trivial und ist es überhaupt sinnvoll, über Typ zu sprechen? a -> b Wo a Und b sind nicht an Quantifizierervariablen gebunden.Andrej Bauer habe in den Kommentaren darauf hingewiesen П Es ähnelt tatsächlich einer Lambda-Abstraktion mit ein paar zusätzlichen Schnickschnack.

Alles in allem bin ich damit fertig, vielen Dank.

Answer 1

Ich denke, wir müssen hier einfach ein paar Dinge klarstellen:

1. Im Ausdruck $\lambda a :\mathsf{Typ} .\lambda x :A .x$ Die Variable $a$ ist gebunden (durch die äußere $\lambda$).Die Ausdrücke $\lambda a :\mathsf{Typ} .\lambda x :A .x$ Und $\lambda b :\mathsf{Typ} .\lambda x :B .x$ Sind $\alpha$-gleich.
2. Der Ausdruck $\lambda a :\mathsf{Typ} .\lambda x :A .x$ Ist die Identitätsfunktion, es ist nicht die „Signatur der Identitätsfunktion“.
3. Wenn Sie mit „Signatur der Identitätsfunktion“ „den Typ der Identitätsfunktion“ meinen, dann wäre es so etwas wie $\Pi_{a :\mathsf{Typ}} .(a \zu a)$, oder wenn Sie nur Produkttypen wünschen, dann ist dies der Fall $\Pi_{a :\mathsf{Typ}} \Pi_{x :a} a$.

Gibt es noch eine Frage?

Vielleicht hilft das:

• der Typ der Identitätsfunktion $\lambda x :A .x$ Ist $a \zu a$
• der Typ der Identitätsfunktion $\lambda y :B .y$ Ist $b o b$
• die Funktionen $\lambda x :A .x$ Und $\lambda y :B .y$ sind anders
• die Typen $a \zu a$ Und $b \zu b$ sind anders
• die Art der polymorph Identitätsfunktion $\lambda c :\mathsf{Typ} .\lambda z :C .z$ Ist $\Pi_{c :\mathsf{Typ}} .c \zu c$.
• die Funktionen $\lambda a :\mathsf{Typ} .\lambda x :A .x$ Und $\lambda c :\mathsf{Typ} .\lambda z :C .z$ Sind $\alpha$-gleich
• die Typen $\Pi_{a :\mathsf{Typ}} .a \zu a$ Und $\Pi_{c :\mathsf{Typ}} .c \zu c$ Sind $\alpha$-gleich.

Ergänzend: Nachdem ich bei einer Tasse Tee mit Alex Simpson gesprochen habe, kann ich noch etwas sagen.Wir nicht brauchen separate $\lambda$ Und $\Pi$ Konstruktoren, da beide genau die gleiche syntaktische Form haben (zwei Argumente nehmen, eine Variable binden).In der Tat, wenn ich mich richtig erinnere, Automatismus verwendete die gleiche Notation für $\lambda$-Abstraktionen und $\Pi$-Typen.Aber der Punkt ist, dass wir wollen zwei verschiedene Konstruktoren zu verwenden, weil sie bezeichnen verschiedene Konzepte.