Θεωρία τύπων

Στα Μαθηματικά, στη Λογική και στη Επιστήμη των Υπολογιστών, η **Θεωρία Τύπων** είναι ένα από τα τυπικά συστήματα τα οποία χρησιμοποιούνται στην Απλοϊκή Θεωρία Συνόλων, ή στη μελέτη τέτοιων φορμαλισμών γενικότερα.  Στη Θεωρία των Γλωσσών Προγραμματισμού, ενός κλάδου της Επιστήμης των Υπολογιστών, η *Θεωρία Τύπων* μπορεί να αναφέρεται στο σχεδιασμό, στην ανάλυση και στη μελέτη των Συστημάτων Τύπων, παρόλο που κάποιοι επιστήμονες της Πληροφορικής περιορίζουν τη σημασία του όρου στη μελέτη των αφηρημένων φορμαλισμών όπως ο λ-λογισμός με τύπους.

Ο Μπέρτραντ Ράσελ εφηύρε την πρώτη θεωρία τύπων μετά την ανακάλυψή του πως η εκδοχή της Απλοϊκής Θεωρίας Συνόλων του Γκότλομπ Φρέγκε υπόκειντο στο Παράδοξο του Ράσελ.  Αυτή η θεωρία τύπων βρίσκεται σε περίοπτη θέση στο *[[Principia Mathematica]]* των Άλφρεντ Νορθ Γουάιτχεντ και Ράσελ. Αποφεύγει το Παράδοξο του Ράσελ με το να δημιουργεί πρώτα μία ιεραρχία τύπων, και κατόπιν να αναθέτει κάθε μαθηματική (και πιθανώς άλλη) οντότητα σε έναν τύπο. Τα αντικείμενα ενός δοσμένου τύπου δημιουργούνται αποκλειστικά από αντικείμενα προηγούμενων τύπων (αυτών που είναι χαμηλότερα στην ιεραρχία), αποφεύγοντας έτσι τις επαναλήψεις.

Ο Αλόνσο Τσερτς, εφευρέτης του λ-λογισμού, ανέπτυξε μια Λογική Υψηλής Τάξης γνωστότερη ως *Θεωρία Τύπων του Τσερτς*, με σκοπό να αποφύγει το Παράδοξο Κλέινι-Ρόσερ που ταλαιπωρούσε τον αρχικό αμιγή λ-λογισμό.  Η θεωρία τύπων του Τσερτς είναι μια παραλλαγή του λ-λογισμού στην οποία οι εκφράσεις (που επίσης καλούνται φόρμουλες ή λ-όροι) κατηγοριοποιούνται σε τύπους, και οι τύποι των εκφράσεων περιορίζουν τους τρόπους με τους οποίους μπορούν να συνδυαστούν. Με άλλα λόγια, είναι ένας λ-λογισμός με τύπους.

Το άρθρο Η Θεωρία Τύπων του Church στην Εγκυκλοπαίδεια την Φιλοσοφίας του Στάνφορντ είναι αφιερωμένο σε αυτό το θέμα.

Σήμερα χρησιμοποιούνται πολλοί άλλοι παρόμοιοι λογισμοί, συμπεριλαμβανομένης της Ιντουισιονιστικής θεωρίας τύπων του Περ Μάρτιν-Λέφ , του Συστήματος F του Ζαν-Ιβ Ζιράρ και του Λογισμoύ των κατασκευών. Στον λ-λογισμό με τύπους, οι τύποι παίζουν ένα ρόλο παρόμοιο με αυτό των συνόλων στη Θεωρία Συνόλων.

## Ιστορία
### 1900 - 1927
**Η Προέλευση της Θεωρίας Τύπων του Ράσελ**: Σε ένα γράμμα του προς τον Γκότλομπ Φρέγκε (1902) ο Ράσελ ανακοίνωσε την ανακάλυψη του παραδόξου στο Begriffsschrift του Φρέγκε. Ο Φρέγκε απάντησε τάχιστα, αναγνωρίζοντας το πρόβλημα και προτείνοντας μια λύση σε μια τεχνική συζήτηση επιπέδων (levels). Παραθέτοντας τον Φρέγκε:

Συνεχίζει δείχνοντας πως θα μπορούσε αυτό να δουλέψει αλλά φαίνεται πως τελικά κάνει πίσω. (Σε μια υποσημείωση, ο φαν Χάιενορτ (van Heijenoort) σημειώνει πως ο Φρέγκε είχε χρησιμοποιήσει ένα σύμβολο (horseshoe) «για την αναγωγή συναρτήσεων δεύτερου επιπέδου σε συναρτήσεις πρώτου επιπέδου»). Ως συνέπεια αυτού που έχει γίνει γνωστό ως το Παράδοξο του Ράσελ τόσο ο Frege όσο και ο Ράσελ έπρεπε να διορθώσουν γρήγορα τα έργα τους που είχαν προς εκτύπωση. Στο Παράρτημα Β που ο Ράσελ πρόσθεσε στο βιβλίο του Principles of Mathematics του 1903,  μπορεί κανείς να βρει την «διστακτική» του «θεωρία τύπων».

Το θέμα στοίχειωνε τον Ράσελ για περίπου πέντε χρόνια (1903–1908). Ο Γουίλαρντ Κιν (Willard Quine) στον πρόλογό του για το *Η Μαθηματική λογική βασισμένη στην θεωρία των τύπων* (1908) του Ράσελ παρουσιάζει μια ιστορική σύνοψη για την προέλευση της θεωρίας των τύπων και της «διακλαδιζόμενης» θεωρίας των τύπων. Ο Ράσελ πρότεινε με σειρά του κάποιες εναλλακτικές: (i) εγκαταλείποντας την θεωρία των τύπων (1905) και προτείνοντας  τρεις θεωρίες το 1905: (ii.1) την θεωρία ζιγκ ζαγκ (zigzag theory), (ii.2) την θεωρία του περιορισμού του μεγέθους (theory of limitation of size), (ii.3) την θεωρία χωρίς κλάσεις (no-class theory) (1905–1906), και κατόπιν (iii) επανέφερε την θεωρία των τύπων (1908).

Ο Κιν παρατηρεί ότι η εισαγωγή της έννοιας της «προφανούς μεταβλητής» από τον Ράσελ είχε το ακόλουθο αποτέλεσμα: «η διάκριση μεταξύ του 'όλα' ('all') και του 'κάποιο' ('any'): Το 'όλα' εκφράζεται από την δεσμευμένη ('προφανή') μεταβλητή της καθολικής ποσοτικοποίησης, που εκτείνεται πάνω σε έναν τύπο, και το 'κάποιο' εκφράζεται από την ελεύθερη ('πραγματική') μεταβλητή που αναφέρεται σχηματικά σε οτιδήποτε ανεξαρτήτως τύπου». Ο Κιν απορρίπτει αυτή την ιδέα της «δεσμευμένης μεταβλητής» ως «άσκοπη εκτός μια συγκεκριμένη πτυχή της θεωρίας των τύπων».

#### Η «διακλαδιζόμενη» θεωρία τύπων του 1908
Ο Κιν εξηγεί την *διακλαδιζόμενη* θεωρία ως εξής: «Ονομάζεται έτσι επειδή ο τύπος μιας συνάρτησης εξαρτάται τόσο από τους τύπους των παραμέτρων της όσο και από τους τύπους των προφανών μεταβλητών που περιέχονται σε αυτήν (ή στην έκφρασή της), σε περίπτωση που αυτές υπερβαίνουν τους τύπους των παραμέτρων». Ο Στίβεν Κλέινι στο βιβλίο του *Εισαγωγή στα Μετα-Μαθηματικά* του 1952 περιγράφει την *διακλαδιζόμενη* θεωρία τύπων ως εξής:

#### Το αξίωμα της αναγωγής και η ιδέα της «μήτρας»
Αλλά επειδή οι παραδοχές της διακλαδιζόμενης θεωρίας θα αποδεικνύονταν (παραθέτοντας τον Κιν) «επαχθείς», ο Ράσελ το 1908 στο έργο του *Η Μαθηματική λογική βασισμένη στην θεωρία των τύπων* θα πρότεινε επίσης το *[[αξίωμα της αναγωγής]]*. Ως το 1910, οι Ουάιτχεντ και ο Ράσελ στο έργο τους *Principia Mathematica* θα επαύξαναν περαιτέρω αυτό το αξίωμα με την ιδέα μιας *μήτρας*, η οποία ήταν μια πλήρως επεκτάσιμη προδιαγραφή μιας συνάρτησης. Από την μήτρα της μια συνάρτηση θα μπορούσε να παραχθεί μέσω της διαδικασίας της «γενίκευσης» και αντίστροφα, δηλ. οι δύο διεργασίες είναι αντιστρέψιμες -- (i) γενίκευση από μήτρα σε συνάρτηση (με χρήση προφανών μεταβλητών)  και (ii) η αντίστροφη διαδικασία της αναγωγής τύπου με κλάσεις-τιμών αντικατάσταση των ορισμάτων για την προφανή μεταβλητή. Με αυτή τη μέθοδο αποφεύγουμε το να είμαστε μη κατηγορηματικοί.

#### Πίνακες Αλήθειας
Τελικά ο Έμιλ Ποστ (1921) θα έβαζε τέλος στην προβληματική θεωρία τύπων του Ράσελ με τις «συναρτήσεις αλήθειας» και τους αντίστοιχους πίνακες αληθείας. Στην «Εισαγωγή» του κατηγορεί την έννοια της προφανούς μεταβλητής του Ράσελ. Αν και η πλήρης θεωρία [των Ουάιτχεντ και Ράσελ (1910, 1912, 1913)] απαιτεί για την έκφραση των λημμάτων τις πραγματικές και προφανείς μεταβλητές οι οποίες αναπαριστούν ατομικές και προτασιακές συναρτήσεις διαφορετικών ειδών, οπότε απαιτεί την προβληματική θεωρία των τύπων, αυτή η υποθεωρία χρησιμοποιεί μόνο πραγματικές μεταβλητές οι οποίες αναπαριστούν μόνο μία οντότητα την οποία οι συγγραφείς ονομάζουν βασικές προτάσεις.

Περίπου τον ίδιο καιρό ο Λούντβιχ Βιτγκενστάιν το 1922 έκανε μια σύντομη εργασία στη θεωρία των τύπων στο έργο του Tractatus Logico-Philosophicus στην οποία σημειώνει τα ακόλουθα στα μέρη 3.331&ndash;3.333:

::3.331 Από αυτή την παρατήρηση αποκτούμε μια καλύτερη εικόνα &ndash; της Θεωρίας Τύπων του Ράσελ. Το λάθος του Ράσελ φαίνεται από το γεγονός ότι σχεδιάζοντας τους συμβολικούς του κανόνες πρέπει να μιλήσει για τη σημασία των συμβόλων αυτών.

::3.332 Καμία πρόταση δεν μπορεί να πει κάτι για τον εαυτό της, επειδή το σύμβολο της πρότασης δεν μπορεί να εμπεριέχεται στον εαυτό του (αυτή είναι όλη η «θεωρία των τύπων»).

::3.333 Μια συνάρτηση δεν μπορεί να είναι παράμετρός της, επειδή το σύμβολο της συνάρτησης περιέχει ήδη το πρωτότυπο της παραμέτρου του και δεν μπορεί να περιέχει τον εαυτό του...

Ο Βιτγκενστάιν επίσης πρότεινε τη μέθοδο του πίνακα αλήθειας. Από το 4.3 έως το 5.101, ο Βιτγκενστάιν υιοθετεί μια μη δεσμευμένη μολυβιά του Σέφερ (Sheffer stroke στα αγγλικά, η μολυβιά του Σέφερ είναι ο χαρακτήρας '|') ως τη θεμελιώδη λογική οντότητά του και κατόπιν καταγράφει όλες τις 16 συναρτήσεις δύο μεταβλητών (5.101).

Η ιδέα της μήτρας ως πίνακα αλήθειας εμφανίζεται στα 1940-1950 στο έργο του Τάρσκι, π.χ. στα ευρετήριά του το 1946 «Μήτρα, βλέπε: Πίνακας αλήθειας»

#### Οι αμφιβολίες του Ράσελ
Ο Ράσελ στην *Εισαγωγή στη Μαθηματική Φιλοσοφία* (1920) αφιερώνει ένα κεφάλαιο στο «Αξίωμα του Απείρου και των λογικών τύπων» στο οποίο λέει τα εξής:

**Ο Ράσελ εγκαταλείπει το αξίωμα της αναγωγής**: Στη δεύτερη έκδοση του *Principia Mathematica* (1927) αναγνωρίζει το επιχείρημα του Βιτγκενστάιν. Στην αρχή της εισαγωγής παραδέχεται: «δεν υπάρχει αμφιβολία... ότι δε χρειάζεται η διαφοροποίηση των εννοιών πραγματική και προφανής μεταβλητή». Οικειοποιείται την έννοια της μήτρας και δηλώνει «Μια συνάρτηση μπορεί να εμφανιστεί σε μια μήτρα μόνο μέσω των τιμών της» (αλλά συμπληρώνει σε μια υποσημείωση: «Αντικαθιστά (όχι αρκετά ικανοποιητικά) το αξίωμα της αναγωγής.») Επιπλέον εισάγει τη νέα (συντομευμένη, γενική) έννοια της «μήτρας», αυτή της «λογικής μήτρας .. που δεν περιέχει σταθερές. Επομένως το p|q είναι μια λογική μήτρα». Βλέπουμε ότι ο Ράσελ εγκατέλειψε την ιδέα του αξιώματος της αναγωγής αλλά στις τελευταίες παραγράφους δηλώνει ότι «από τις παρούσες πρωταρχικές έννοιες» δεν μπορεί να παράγει «σχέσεις του Ντέντεκιντ και σχέσεις καλώς διατεταγμένες» και παρατηρεί ότι αν υπάρχει κάποιο καινούριο αξίωμα να αντικαταστήσει το αξίωμα της αναγωγής «μένει να ανακαλυφθεί».

### Θεωρία των απλών τύπων
Στη δεκαετία του 20 οι Λέον Τσβίστεκ και Φρανκ Π. Ράμσεϊ παρατήρησαν ότι αν κάποιος θέλει να εγκαταλείψει την αρχή του φαύλου κύκλου, η ιεραρχία των επιπέδων των τύπων στην «διακλαδιζόμενη θεωρία των τύπων» (δείτε το ιστορικό σημείωμα πριν) μπορεί να καταρρεύσει.

Η προϊούσα περιορισμένη λογική ονομάζεται θεωρία των απλών τύπων ή πιο  απλά θεωρία των τύπων. Λεπτομερείς εκθέσεις της απλής θεωρίας των τύπων εκδόθηκαν στα τέλη του 1920 και στις αρχές του 30 από τους Ρ. Κάρναπ, Φ. Ράμσεϊ, Ου.Β.Ο. Κιν και Α. Τάρσκι. Το 1940 ο Αλόνσο Τσέρτς την επανασχεδίασε ως λ-λογισμό με απλούς τύπους. και εξετάστηκε και από τον Γκέντελ το 1944.

### 1940s - σήμερα

Ο Κιν αναφέρει ότι ο Ράμσεϊ το 1931 παρότρυνε την «πτώση του διακλαδισμού και του αξιώματος της αναγωγής». Ο Κιν είναι της γνώμης ότι «η αποτυχία του Ράσελ ήταν εξαιτίας αυτής της αποτυχίας της διακρίσεως ανάμεσα στις προτασιακές συναρτήσεις ως συμβολισμούς και τις προτασιακές συναρτήσεις ως ιδιότητες και σχέσεις [Ο σχολιασμός του Κιν στο Ράσελ 1908 στο φαν Χάιενορτ 1967:151-152].»\in. Σε οποιαδήποτε φόρμουλα οι μεταβλητές χωρίς τόνο έχουν όλες τον ίδιο τύπο ενώ οι μεταβλητές με τόνο (x') έχουν τον αμέσως μεγαλύτερο τύπο.  Οι ατομικές φόρμουλες της **ST** έχουν δύο μορφές, x=y (ταυτότητα) και y\in x'. Το πρόθεμα  \in δηλώνει την προτιθέμενη ερμηνεία, την σχέση μέλους συνόλου.

Όλες οι μεταβλητές που εμφανίζονται στον ορισμό της ταυτότητας και στα αξιώματα της *Εκτασιμότητας* και *Κατανόησης* προέρχονται από άτομα από ένα εκ των δύο συνεχόμενων τύπων. Μόνο οι μεταβλητές χωρίς τόνο (που προέρχονται από τον «χαμηλότερο» τύπο) μπορούν να εμφανιστούν στα αριστερα του '\in', ενώ τα δεξιά μόνο μεταβλητές με τόνο (που προέρχονται από «υψηλότερο» τύπο) μπορούν να εμφανιστούν. Ο πρώτης-τάξης φορμαλισμός του **ST** αποκλείει την ποσοτικοποίηση προς όφελος των τύπων. Ως συνέπεια κάθε ζευγάρι από συνεχόμενους τύπους απαιτεί το δικό του αξίωμα της Εκτασιμότητας και Κατανόησης, το οποίο είναι πιθανό αν η Εκτασιμότητα και η Κατανόηση παρακάτω θεωρούνται σαν σχήματα αξιωμάτων που εφαρμόζονται σε τύπους.   
 
* **Ταυτότητα**, ορίζεται ως x=y\leftrightarrow\forall z' [x\in z'\leftrightarrow y\in z'].

* **[[Αξίωμα της Εκτασιμότητας|Επεκτασιμότητα]]**.  Ένα αξιωματικό σχήμα. \forall x[x\in y' \leftrightarrow x\in z'] \rightarrow [y'=z'].

: Αν \Phi(x) είναι οποιαδήποτε φόρμουλα πρώτης τάξης που περιέχει την ελεύθερη μεταβλητή x.

* **Κατανόηση**.  Ένα αξιωματικό σχήμα. \exists z'\forall x[x\in z'\leftrightarrow \Phi(x)].

: *Σημείωση*. Κάθε συλλογή αντικειμένων του ίδιου τύπου αποτελούν ένα αντικείμενο με επόμενης τάξης τύπο. Η Κατανόηση είναι σχηματική όσον αφορά το \Phi(x) όπως επίσης και τους τύπους.

* **[[Αξίωμα του απείρου|Άπειρο]]**. Υπάρχει μια μη κενή δυαδική σχέση R  στα άτομα του χαμηλότερου τύπου, που είναι μη ανακλαστική, ματαβατική, και ισχυρά συνδεδεμένη: \forall x,y [x\neq y\rightarrow[xRy\vee yRx]].

: *Σημείωση*. Το άπειρο είναι το μοναδικό πραγματικό αξίωμα τoυ **ST** που είναι καθαρά μαθηματικό στη φύση του. Μας βεβαιώνει ότι το R είναι μια αυστηρά ολική διάταξη, με ένα  πεδίο ταυτόσημο με το συμπληρωματικό πεδίο. Αν αναθέσουμε 0 στο χαμηλότερο τύπο το R έχει τύπο 3. Το άπειρο μπορεί να ικανοποιηθεί αν ο (συμπληρωματικό) τομέας του R είναι άπειρο, οπότε απαιτεί την ύπαρξη ενός άπειρου συνόλου. Αν οι σχέσεις ορίζονται σε σχέση με  διατεταγμένα ζεύγη, το αξίωμα απαιτεί τον προηγούμενο ορισμό του διατεταγμένου ζεύγους. Ο ορισμός του Κουρατόφσκι, προσαρμοσμένος στο **ST**, είναι αυτό που χρειάζεται. Στη βιβλιογραφία δεν εξηγείται γιατί το σύνηθες αξίωμα του απείρου (υπάρχει άλλες συνολοθεωρίες δεν μπορεί να ταιριάξει με το **ST**.

Το **ST** αποκαλύπτει πως η θεωρία τύπων μπορεί να αναχθεί στην αξιωματική θεωρία συνόλων. Επιπλέον η πιο λεπτομερής οντολογία του **ST**, περιορισμένη σε αυτό που τώρα ονομάζεται «επαναλαμβανόμενη σύλληψη του συνόλου» (αγγλικά: iterative conception of set), περιέχει αξιώματα που είναι πολύ απλούστερα των συμβατικών συνολοθεωριών, όπως της ZFC. Συνολοθεωρίες των οποίων σημείο εκκίνησης είναι η θεωρία τύπων αλλά τα αξιώματά τους, η Οντολογία και η ορολογία διαφέρουν από αυτή περιλαμβάνουν τη Νέα Θεμέλια και Συνολοθεωρία των Σκοτ-Πότερ.

### Φόρμουλες βασισμένες στην ισότητα

Η θεωρία τύπων του Τσερτς έχει μελετηθεί εκτενώς από δύο μαθητές του, τον Λέον Χένκιν και τον Πίτερ Μπρους Άντριους. Καθώς η ST είναι μια λογική υψηλής τάξης, και στις λογικές υψηλής τάξης μπορεί κανείς να ορίσει προτασιακούς συνδέσμους από την άποψη της λογικής ισοδυναμίας και των ποσοδεικτών, το 1963 ο Χένκιν ανέπτυξε μια μορφοποίηση της **ST** βασισμένη στην ισότητα, αλλά στην οποία περιόρισε την προσοχή του στους κατηγορηματικούς τύπους. Το παραπάνω απλοποιήθηκε αργότερα τον ίδιο χρόνο από τον Άντριους στη θεωρία '''Q<sub>0</sub>'''. Κάτω από αυτό το πρίσμα η **ST** μπορεί να θεωρηθεί ως ένα είδος λογικής υψηλής τάξης, η οποία χαρακτηρίστηκε από τον Π.Τ. Τζόνστον στο *Sketches of an Elephant* ότι έχει μια λάμδα-υπογραφή η οποία είναι μια υψηλής-τάξης υπογραφή που δεν περιέχει σχέσεις και χρησιμοποιεί μόνο γινόμενα και βέλη (τύποι συναρτήσεων) ως κατασκευαστές τύπων. Επιπλέον, όπως το έθεσε ο Τζόντστον η **ST** είναι «χωρίς λογική» με την έννοια ότι δεν περιέχει λογικές συνδέσεις ή ποσοδείκετες στον ορισμό της.

### Επεκτάσεις
#### Πολυμορφισμός τύπων

Ο **Πολυμορφισμός** είναι ένα χαρακτηριστικό των γλωσσών προγραμματισμού που μας επιτρέπει να χειριστούμε τιμές διαφορετικών δομών δεδομένων χρησιμοποιώντας μία ομοιόμορφη διεπαφή. Η έννοια του παραμετρικού πολυμορφισμού ισχύει τόσο για τις δομές δεδομένων όσο και για τις συναρτήσεις. Μια συνάρτηση που μπορεί να αποτιμήσει ή να εφαρμοστεί σε τιμές διαφορετικών τύπων είναι γνωστή ως *πολυμορφική συνάρτηση*. Ένας τύπος δεδομένων που μπορεί να φαίνεται γενικευμένου τύπου (π.χ. μία λίστα με στοιχεία αόριστου τύπου) χαρακτηρίζεται ως *πολυμορφικός τύπος δεδομένων* όπως ο γενικευμένος τύπος από τον οποίο γίνονται αυτές οι εξειδικεύσεις.

#### Εξαρτώμενοι τύποι

Ο **εξαρτώμενος τύπος** είναι ένας τύπος που εξαρτάται από μία τιμή. Οι εξαρτώμενοι τύποι παίζουν ένα κεντρικό ρόλο στην Ιντουισιονιστική θεωρία τύπων και στον σχεδιασμό των συναρτησιακών γλωσσών προγραμματισμού όπως η ATS, η Agda και η Epigram.

Ένα παράδειγμα είναι ο τύπος της *n*-πλειάδας πραγματικών αριθμών. Αυτός είναι ένας εξαρτώμενο τύπος διότι ο τύπος *εξαρτάται* από την τιμή *n*.

## Πρακτικές συνέπειες
### Πληροφορική

Η πιο προφανής εφαρμογή της Θεωρίας Τύπων είναι στην κατασκευή αλγορίθμων ελέγχου τύπων στην φάση της σημασιολογικής ανάλυσης των μεταγλωττιστών των γλωσσών προγραμματισμού. Οι ορισμοί του *συστήματος τύπων* ποικίλλουν, αλλά ο επόμενος χάρη στον Μπέντζαμιν Κρόφορντ Πιρς αντιστοιχεί χονδρικά στη σημερινή ομοφωνία της κοινότητας της θεωρίας των γλωσσών προγραμματισμού:

Με άλλα λόγια, ένα σύστημα τύπων χωρίζει τις τιμές του προγράμματος σε σύνολα που ονομάζονται τύποι - αυτό ονομάζεται *ανάθεση τύπων* - και καθιστά ορισμένες συμπεριφορές του προγράμματος μη έγκυρες με βάση τους τύπους που έχουν ανατεθεί. Για παράδειγμα, ένα σύστημα τύπων μπορεί να κατηγοριοποιήσει την τιμή "hello" ως συμβολοσειρά και την τιμή 5 ως αριθμό, και να απαγορεύσει στον προγραμματιστή να προσθέσει το "hello" με το 5 βάσει αυτής της ανάθεσης τύπων. Σε αυτό το σύστημα τύπων, το πρόγραμμα

:`"hello" + 5`

θα ήταν μη έγκυρο. Ως εκ τούτου, κάθε πρόγραμμα που περνάει από το σύστημα τύπων αποδεδειγμένα δεν θα εμφανίζει την εσφαλμένη συμπεριφορά της πρόσθεσης συμβολοσειρών με αριθμούς.

Ο σχεδιασμός και η υλοποίηση των συστημάτων τύπων είναι ένα θέμα σχεδόν τόσο ευρύ όσο και το θέμα των γλωσσών προγραμματισμού καθαυτό. Στην πραγματικότητα, οι υποστηρικτές της θεωρίας τύπων διακηρύσσουν ότι ο σχεδιασμός των συστημάτων τύπων είναι η ουσία του σχεδιασμού των γλωσσών προγραμματισμού: «Σχεδίασε σωστά το σύστημα τύπων, και η γλώσσα θα σχεδιάσει τον εαυτό της.»

### Γλωσσολογία
Η θεωρία τύπων χρησιμοποιείται ευρέως στις τυπικές θεωρίες της σημασιολογίας των φυσικών γλωσσών, ειδικότερα της γραμματικής Μόνταγκιου και των απογόνων της. Η πιο κοινή κατασκευή παίρνει τους βασικούς τύπους e και t για άτομα και αληθοτιμές, αντίστοιχα, και ορίζει το σύνολο των τύπων ως εξής:

* Εάν a και b είναι τύποι, τότε τύπος είναι και ο \langle a,b\rangle.
* Τύποι είναι μόνο οι βασικοί τύποι και ό,τι μπορεί να κατασκευαστεί από αυτούς μέσω της παραπάνω πρότασης.

Ένας σύνθετος τύπος \langle a,b\rangle είναι ο τύπος των συναρτήσεων συναρτήσεων από οντότητες τύπου a σε οντότητες τύπου b. Έτσι κάποιος έχει τύπους όπως \langle e,t\rangle που ερμηνεύονται ως στοιχεία του συνόλου των συναρτήσεων από οντότητες σε αληθοτιμές, δηλ. χαρακτηριστικές συναρτήσεις του συνόλου των οντοτήτων. Μια συνάρτηση τύπου \langle\langle e,t\rangle,t\rangle είναι μια συνάρτηση από οντότητες σε αληθοτιμές, δηλ. μια χαρακτηριστική συνάρτηση ενός συνόλου από σύνολα. Αυτός ο τελευταίος τύπος συχνά θεωρείται ο τύπος των ποσοδεικτών των φυσικών γλωσσών, όπως οι * όλοι* ή * κανένας* (Μόνταγκιου 1973, Μπάρουαϊς και Κούπερ 1981).

### Κοινωνικές επιστήμες
Ο Gregory Bateson εισήγαγε μια θεωρία λογικών τύπων στις κοινωνικές επιστήμες; οι ιδέες του της διπλής δέσμευσης και των λογικών επιπέδων βασίζονται στη θεωρία τύπων του Ράσελ.

## Συνδέσεις με την Κατασκευαστική Λογική

## Δείτε επίσης
* Θεωρία κατηγοριών
* Θεωρία μοντέλων
* Θεωρία πεδίων
* Σύστημα Τύπων για μια πιο πρακτική συζήτηση των συστημάτων τύπων για γλώσσες προγραμματισμού
* Τύπος (θεωρία μοντέλων)
* Τύπος δεδομένων για συμπαγείς τύπους δεδομένων στον προγραμματισμό

## Αναφορές

*Mendelson, Elliot, 1997. *Εισαγωγή στην Μαθηματική Λογική*, 4η έκδοση. Chapman & Hall.
*W. Farmer, *Οι 7 αρετές της απλή θεωρίας τύπων*, Περιοδικό της Εφαρμοσμένης Λογικής, Vol. 6, No. 3. (Σεπτέμβριος 2008), σελ.&nbsp;267–286.



## Επιπλέον διάβασμα
* Constable, Robert L., 2002, "Απλοϊκή θεωρία τύπων υπολογισμού," στο  *Απόδειξη και Αξιοπιστία του συστήματος*: των H. Schwichtenberg και R. Steinbruggen (eds.), 213&ndash;259. Προορισμένο ως ομόλογο του *[[Naive Set Theory (book)|Naive Set Theory]]* του Πολ Χάλμος (1960) σχετικά με τη θεωρία τύπων
* 
* Covers type theory in depth, including polymorphic and dependent type extensions. Gives categorical semantics.
*  Παρέχει μια ιστορική έρευνα των εξελίξεων της θεωρίας των τύπων με εστίαση στην άρνηση της θεωρίας ως ένα θεμέλιο των μαθηματικών διαμέσου των τεσσάρων δεκαετιών που ακολούθησαν την δημοσιοποίηση της 2ης έκδοσης της 'Principia Mathematica'.
* Cardelli, Luca, 1997, "Συστήματα Τύπων, " in Allen B. Tucker, ed., *Η Πληροφορική και το Εγχειρίδιο του Μηχανικού*. CRC Press: 2208&ndash;2236.
* Thompson, Simon, 1991. *[http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ Θεωρία Τύπων και Συναρτησιακός Προγραμματισμός]*. Addison-Wesley. ISBN 0-201-41667-0.
* J. Roger Hindley, *Βασική Απλή Θεωρια Τύπων*, Cambridge University Press, 2008, ISBN 0521054222 (also 1995, 1997). Μια καλή εισαγωγή στη θεωρία τύπων για επιστήμονες της Πληροφορικής. Το σύστημα που περιγράφεται δεν είναι ακριβώς το STT του Church όμως. Book review
* Stanford Encyclopedia of Philosophy: Θεωρία Τύπων" &ndash; από τον Τιερί Κοκάντ.
* Fairouz D. Kamareddine, Twan Laan, Rob P. Nederpelt, *Μια σύγχρονη προοπτική στη θεωρία τύπων: από τις καταβολές της ως σήμερα*, Springer, 2004, ISBN 1402023340
* Jose Ferreiros, Jose Ferreiros Dominguez, *Λαβύρινθος σκέψεων: μια ιστορία της θεωρίας συνόλων και τον ρόλο της στα σύγχρονα μαθηματικά*, 2η Έκδοση, Springer, 2007, ISBN 3764383496, Κεφάλαιο X "Λογική και Θεωρία Τύπων κατά τη διάρκεια του Μεσοπολέμου"

### Πηγές για το τμήμα της Ιστορίας
* Μπέρτραντ Ράσελ (1903) *Οι αρχές των Μαθηματικών: Τόμος 1*, Cambridge at the University Press, Cambridge, UK, επανεκτυπωμένο ως googlebook.
* Μπέρτραντ Ράσελ (1920) *Εισαγωγή στην Μαθηματική Φιλοσοφία* (2η έκδοση), Dover Publishing Inc., New York NY, ISBN 0-486-27724-0 (pbk).
* Άλφρεντ Τάρσκι (1946) *Εισαγωγή στη Λογική και στις Επιστήμες Εξαγωγής Συμπερασμάτων*, επανεκτυπωμένο το 1995 από την Dover Publications, Inc., New York, NY ISBN 0-486-28462-x
* Jean van Heijenoort (1967, 3η εκτύπωση 1976), *Από τον Frege στον Godel: Ένα βασικό βιβλίο στη Μαθηματική Λογική, 1879-1931*, Harvard University Press, Cambridge, MA, ISBN 0-674-32449-8 (pbk)
** Μπέρτραντ Ράσελ (1902) *Γράμμα στον Frege* με σχολιασμό από τον van Heijenoort, σελίδες 124-125. Όπου ο Ράσελ ανακοινώνει την ανακάλυψή του ενός "παραδόξου" στην εργασία του Frege.
** Gottlob Frege (1902) *Γράμμα στον Ράσελ* με σχολιασμό από τον van Heijenoort, σελίδες 126-128.
** Μπέρτραντ Ράσελ (1908a) *Η μαθηματική λογική βασιμένη στη θεωρία των τύπων*, με σχολιασμό από τον Γουίλαρντ Κιν, σελίδες 150-182.
** Emil Post (1921) *Εισαγωγή σε μια γενική θεωρία βασικών προτάσεων*, με σχολιασμό από τον van Heijenoort, σελίδες 264-283.
* Alfred North Whitehead και Μπέρτραντ Ράσελ (1910–1913, 1927 2η έκδοση επανεκτυπωμένη το 1962), *Principia Mathematica to *56*, Cambridge at the University Press, London UK, χωρίς ISBN ή US card αριθμό καταλόγου.
* Λούντβιχ Βιτγκενστάιν (επανεκτυπωμένο 2009) *Μεγάλα έργα: Επιλεγμένα φιλοσοφικά έργα", HarperCollins, New York. ISBN 978-0-06-155024-9. Το *Tractatus Logico-Philosophicus'' του Βιτγκενστάιν (1921 στα Αγγλικά) σελίδες 1–82.

## Εξωτερικοί Σύνδεσμοι
* Types Project lecture notes των θερινών μαθημάτων 2005-2008
** The 2005 summer school έχει εισαγωγικές διαλέξεις
* [ftp://ftp.cs.cornell.edu/pub/nuprl/doc/book.ps.gz The Nuprl Book]: "Εισαγωγή στη Θεωρία Τύπων."


Κατηγορία:Ιεραρχία