Sind Typen Aussagen? (Was genau sind Typen?)

25

Ich habe viel über Typsysteme und dergleichen gelesen und verstehe ungefähr, warum sie eingeführt wurden (um Russels Paradoxon zu lösen). Ich verstehe auch in etwa deren praktische Relevanz in Programmiersprachen und Proofsystemen. Ich bin jedoch nicht ganz sicher, dass meine intuitive Vorstellung, was ein Typ ist, richtig ist.

Meine Frage ist, ist es gültig zu behaupten, dass Typen Sätze sind?

Mit anderen Worten entspricht die Aussage "n ist eine natürliche Zahl" der Aussage "n hat den Typ" natürliche Zahl ", was bedeutet, dass alle algebraischen Regeln, die natürliche Zahlen beinhalten, für n gelten. (Anders ausgedrückt, algebraische Regeln sind Aussagen. Aussagen, die für natürliche Zahlen gelten, gelten auch für n.)

Bedeutet dies dann, dass ein mathematisches Objekt mehr als einen Typ haben kann?

Außerdem weiß ich, dass Mengen nicht den Typen entsprechen, weil Sie nicht alle Mengen haben können. Könnte ich behaupten, dass, wenn eine Menge ein mathematisches Objekt ist, das einer Zahl oder einer Funktion ähnlich ist , ein Typ eine Art metamathematisches Objekt ist und nach der gleichen Logik eine Art ein metamathematisches Objekt ist? (in dem Sinne, dass jedes "Meta" eine höhere Abstraktionsebene anzeigt ...)

Hat dies irgendeine Verbindung zur Kategorietheorie?

Rehno Lindeque
quelle
5
Eine eng verwandte Frage: Beweise / Programme und Sätze / Typen
Marc Hamann
1
Eine weitere Diskussion zum Thema
Marc Hamann
Einen
Rehno Lindeque
1
In gewissem Sinne läuft dies auf eine Frage der Ontologie hinaus. Was ist eine Menge, ein Satz usw. Außerdem gibt es viele Menschen, die Typen auch als Mengen betrachten. Wenn man genauer sein will, kann man zwischen kleinen Typen (die Mengen sind) und Universumstypen unterscheiden. Für eine nette Lektüre, die einige dieser Themen betrifft, empfehle ich Martin-Löfs klassisches Papier "Intuitionistic Type Theory"
Tobias Raski
1
Jemand sollte eine Antwort aus Sicht der Homotopie-Typ-Theorie schreiben.
Robin Green

Antworten:

20

Die Schlüsselrolle von Typen besteht darin, die interessierenden Objekte in verschiedene Universen zu unterteilen, anstatt alles zu berücksichtigen, was in einem Universum existiert. Ursprünglich wurden Typen entwickelt, um Paradoxien zu vermeiden, aber Sie wissen, dass sie viele andere Anwendungen haben. Typen bieten die Möglichkeit, Objekte zu klassifizieren oder zu schichten (siehe Blogeintrag ).

Einige arbeiten mit dem Slogan, dass Sätze Typen sind , also dient Ihre Intuition Ihnen sicherlich gut, obwohl es Arbeiten wie Propositions as [Types] von Steve Awodey und Andrej Bauer gibt, die etwas anderes argumentieren, nämlich dass jedem Typ ein Satz zugeordnet ist. Die Unterscheidung wird getroffen, weil Typen einen rechnerischen Inhalt haben, Propositionen dagegen nicht.

Ein Objekt kann mehr als eine Art hat aufgrund Subtypisierung und über Art Nötigungen .

Typen sind im Allgemeinen in einer Hierarchie organisiert, in der Arten die Rolle des Typs von Typen spielen, aber ich würde nicht so weit gehen zu sagen, dass Typen metamathematisch sind. Alles läuft auf der gleichen Ebene ab - dies gilt insbesondere für abhängige Typen .

Es gibt eine sehr starke Verbindung zwischen Typen und Kategorietheorie. Tatsächlich sagt Bob Harper (Lambek zitierend), dass Logik, Sprachen (wo Typen existieren) und Kategorien eine heilige Dreifaltigkeit bilden . Zitat:

Diese drei Aspekte führen zu drei Sekten der Anbetung: Logik, die Beweisen und Aussagen den Vorrang gibt; Sprachen, die Programmen und Typen den Vorrang geben; Kategorien, die Mappings und Strukturen den Vorrang geben.

Sie sollten sich die Curry-Howard-Korrespondenz ansehen, um die Verbindung zwischen Logik- und Programmiersprachen (Typen sind Sätze) und geschlossenen kartesischen Kategorien zu sehen, um den Zusammenhang mit der Kategorietheorie zu untersuchen.

Dave Clarke
quelle
Vielen Dank, der erste Link war besonders hilfreich! Darin teilt Mark mit, dass über Typen eine "totale Beziehung <" besteht. Bedeutet dies also, dass alle "Sätze" eines Typs auch alle "Sätze" in den darunter liegenden Typen enthalten müssen? Ich erwartete, dass es zumindest eine "partielle Beziehung <" über Typen sein würde ....
Rehno Lindeque
1
Wie ich es lese, gibt es eine totale Ordnung über Atomen, die lediglich dafür gesorgt hat, dass es unendlich viele Atome gibt.
Dave Clarke
Oh, ich verstehe, dass ich zwischen dem "Axiom of Comprehension" und dem "Axiom of Infinity" verwechselt wurde ... Wäre ein Typ "nat" (der Typ aller natürlichen Zahlen) ein "Typ der unendlichen Ebene 0"?
Rehno Lindeque
3
Die "heilige Dreifaltigkeit" ist wirklich Lambek zu verdanken. Vgl. die Diskussion der Typentheorie bei Lambek & Scott (1986). Ich habe gehört, dass in McGill von der Curry-Howard-Lambek-Korrespondenz die Rede ist.
Charles Stewart
@Charles: Ich stimme zu, dass Lambek für seinen massiven Beitrag unterbewertet ist, auch wenn ich ironischerweise durch das Lesen des Buches von Lambek und Scott davon überzeugt wurde, dass die "heilige Dreifaltigkeit" ein Schwindel ist: Sie bricht in Gegenwart eines potenziellen Nicht zusammen -Beendigung.
Marc Hamann