Σύστημα τύπων

Στην επιστήμη υπολογιστών, ως σύστημα τύπων (type system) μπορεί να οριστεί ένα διαχειρίσιμο συντακτικό πλαίσιο για την κατάταξη φράσεων ανάλογα με τις τιμές που υπολογίζουν. Ένα σύστημα τύπων αποδίδει τύπους (types) σε κάθε υπολογισμένη τιμή. Εξετάζοντας τη ροή αυτών των τιμών, ένα σύστημα τύπων πρέπει να αποδείξει ότι δεν πρόκειται να συμβούν σφάλματα τύπων (type errors). Αν και κάθε διαφορετικό σύστημα τύπων ορίζει τι αποτελεί σφάλμα τύπου, γενικά ένα σύστημα τύπων προσπαθεί να εξασφαλίσει ότι λειτουργίες που δέχονται τιμές συγκεκριμένου είδους δε χρησιμοποιούνται με τιμές που δεν πρέπει.

Ένας μεταγλωττιστής μπορεί να χρησιμοποιήσει το στατικό τύπο μιας τιμής για να βελτιστοποιήσει τον τρόπο με τον οποίο αυτή θα αποθηκευθεί και τι αλγόριθμοι μπορούν να χρησιμοποιηθούν σε αυτή. Για παράδειγμα, σε πολλούς μεταγλωττιστές της C, ο τύπος δεδομένων "αριθμός κινητής υποδιαστολής" ("float") αναπαρίσταται από 32 bits, σύμφωνα με το πρότυπο κινητής υποδιαστολής απλής ακρίβειας κατά IEEE. Σε αυτήν την περίπτωση η C χρησιμοποιεί λειτουργίες ειδικά για αριθμούς κινητής υποδιαστολής σε αυτές τις τιμές (πρόσθεση αριθμών κινητής υποδιαστολής, πολλαπλασιασμός, κλπ).

Το πόσο λεπτομερείς είναι οι περιορισμοί των τύπων και ο τρόπος με τον οποίο αποτιμώνται επηρεάζει την τυποποίηση (typing) μιας γλώσσας. Μια γλώσσα προγραμματισμού μπορεί επιπλέον να αντιστοιχίζει λειτουργίες διαφορετικές υλοποιήσεις αλγορίθμων σε διαφορετικούς τύπους στην περίπτωση του πολυμορφισμού τύπων (type polymorphism). Θεωρία τύπων (type theory) είναι η μελέτη των συστημάτων τύπων, αν και σημαντικό μέρος των συστημάτων τύπων που χρησιμοποιούνται στην πράξη προέρχονται από έρευνα στην αρχιτεκτονική υπολογιστών, την υλοποίηση μεταγλωττιστών και τη σχεδίαση γλωσσών.

Βασικές έννοιες

Η αντιστοίχιση τύπων σε δεδομένα (τυποποίηση) δίνει σημασία σε ακολουθίες από bits. Οι τύποι συνήθως αντιστοιχίζονται σε τιμές στη μνήμη ή σε αντικείμενα όπως οι μεταβλητές. Επειδή κάθε τιμή αποτελείται από μια ακολουθία bits σε έναν υπολογιστή, το υλικό δε μπορεί να ξεχωρίσει μεταξύ διευθύνσεων μνήμης, εντολών, χαρακτήρων, ακεραίων και αριθμών κινητής υποδιαστολής. Αν σε μια ακολουθία από bits όμως αποδοθεί κάποιος τύπος, τότε αυτό αποτελεί πληροφορία προς τα προγράμματα και τους προγραμματιστές για το τι σημαίνει αυτή η ακολουθία.

Σημαντικές λειτουργίες των συστημάτων τύπων περιλαμβάνουν:

• Ασφάλεια – Η χρήση των τύπων μπορεί να επιτρέψει σε ένα μεταγλωττιστή να εντοπίσει ακατάλληλο κώδικα. Για παράδειγμα, η έκφραση 3 / "Hello, World" μπορεί να θεωρηθεί μη έγκυρη γιατί οι κανόνες της αριθμητικής δεν ορίζουν πώς διαιρείται ένας ακέραιος με μια συμβολοσειρά. Όπως αναπτύσσεται παρακάτω, η ισχυρή τυποποίηση (strong typing) προσφέρει μεγαλύτερη ασφάλεια αλλά συνήθως όχι πλήρως (δείτε ασφάλεια τύπων για περισσότερες πληροφορίες).
• Βελτιστοποίηση – Ο στατικός έλεγχος τύπων μπορεί να παρέχει χρήσιμες πληροφορίες στο χρόνο μεταγλώττισης. Για παράδειγμα, αν ένας τύπος απαιτεί μια τιμή να στοιχίζεται σε διευθύνσεις μνήμης που είναι πολλαπλάσια των 4 bytes, ο μεταγλωττιστής θα πρέπει να μπορεί να κάνει χρήση πιο αποδοτικών εντολών.
• Τεκμηρίωση – Στα πιο εκφραστικά συστήματα τύπων, οι τύποι μπορούν να είναι χρήσιμοι σαν μια μορφή τεκμηρίωσης, μιας και φανερώνουν τις προθέσεις του προγραμματιστή. Για παράδειγμα, οι ημερομηνίες (timestamps) μπορούν να αναπαρασταθούν σαν ακέραιοι — αν όμως ο προγραμματιστής δηλώσει ότι μια συνάρτηση επιστρέφει ημερομηνία αντί απλά ακέραιο, αυτό αποτελεί μέρος της τεκμηρίωσης της συνάρτησης.
• Αφαίρεση (abstraction) ή modularity – Οι τύποι επιτρέπουν στους προγραμματιστές να σκέφτονται τα προγράμματά τους σε ένα ανώτερο επίπεδο από τα bits ή τα bytes, χωρίς να χρειάζεται να ασχοληθούν με την υλοποίηση σε χαμηλό επίπεδο. Για παράδειγμα, μια συμβολοσειρά μπορεί να θεωρηθεί σαν μια συλλογή από χαρακτήρες, αντί ενός απλού πίνακα από bytes. Οι τύποι μπορούν επίσης να εκφράσουν τη διαπροσωπεία (interface) ανάμεσα σε δύο υποσυστήματα. Αυτό βοηθά στον εντοπισμό των ορισμών που χρειάζονται για να επικοινωνήσουν δύο υποσυστήματα και αποκλείει σφάλματα στον τρόπο που γίνεται η επικοινωνία τους.

Η ασφάλεια τύπων προσφέρει ορθότητα προγράμματος αλλά όχι πλήρως (αλλιώς ο έλεγχος τύπων γίνεται μη υπολογίσιμο πρόβλημα). Ανάλογα με το σύστημα τύπων, ένα πρόγραμμα μπορεί να δίνει λάθος αποτέλεσμα ενώ έχει τους σωστούς τύπους και δεν προκαλεί σφάλματα μεταγλώττισης. Για παράδειγμα η διαίρεση με το μηδέν δεν εντοπίζεται από τον ελεγκτή τύπων στις περισσότερες γλώσσες προγραμματισμού αλλά αποτελεί σφάλμα χρόνου εκτέλεσης (runtime error). Η απόδειξη της έλλειψης σφαλμάτων διασφαλίζεται συχνά από ένα σύνολο τυπικών μεθόδων (formal methods), γνωστές συνολικά με τον όρο ανάλυση προγράμματος, καθώς και από τις δοκιμές λογισμικού (software testing), μια συχνά χρησιμοποιούμενη εμπειρική μέθοδο για τον εντοπισμό λαθών που δε μπορεί να βρει ο ελεγκτής τύπων.

Ένα πρόγραμμα συνήθως αντιστοιχίζει σε κάθε τιμή κάποιον τύπο (και ένας τύπος μπορείς να έχει έναν ή περισσότερους υποτύπους, subtypes). Επίσης, τα αντικείμενα, οι μονάδες (modules), τα κανάλια επικοινωνίας (communication channels), οι εξαρτήσεις (dependencies), ακόμα και οι ίδιοι οι τύποι μπορούν να έχουν κάποιον τύπο. Ανάλογα με την υλοποίηση υπάρχουν και οι εξής χαρακτηρισμοί (που όμως τεχνικά αποτελούν διαφορετικές ιδέες):

• τύπος δεδομένων (data type) – ο τύπος μιας τιμής
• κλάση (class) – ο τύπος ενός αντικειμένου
• kind – ο τύπος ενός τύπου

Ένα σύστημα τύπων (type system), κάποιας γλώσσας προγραμματισμού, ελέγχει τον τρόπο με τον οποίο μπορούν να συμπεριφέρονται τα τυποποιημένα προγράμματα και θεωρεί μη έγκυρη τη συμπεριφορά έξω από αυτούς τους κανόνες. Ένα effect system συνήθως παρέχει λεπτομερέστερο έλεγχο από ένα σύστημα τύπων.

Τυπικά η θεωρία τύπων μελετά τα συστήματα τύπων. Πολυπλοκότερα συστήματα τύπων (όπως οι εξαρτώμενοι τύποι, dependent types) επιτρέπουν την επαλήθευση λεπτομερών προδιαγραφών προγραμμάτων από έναν ελεγκτή τύπων αλλά αυτό έχει το μειονέκτημα ότι η εξαγωγή τύπων και άλλες ιδιότητες γενικά γίνονται μη-υπολογίσιμες, ενώ ο έλεγχος τύπων εξαρτάται από αποδείξεις που δίνονται από το χρήστη. Αποτελεί σημαντική πρόκληση η εύρεση ενός αρκετά εκφραστικού συστήματος τύπων που να ικανοποιεί προγραμματιστικές πρακτικές με τυπικά ασφαλή τρόπο.

Έλεγχος τύπων

Η επαλήθευση και η εφαρμογή των περιορισμών των τύπων - έλεγχος τύπων (type checking) – μπορεί να συμβεί είτε στο χρόνο μεταγλώττισης (στατικός έλεγχος), είτε στο χρόνο εκτέλεσης (δυναμικός έλεγχος). Αν ο ορισμός μιας γλώσσας απαιτεί ισχυρούς κανόνες τύπων (συνήθως επιτρέποντας μόνο αυτόματες μετατροπές τύπων που δε χάνουν πληροφορία), αυτή μπορεί να ονομαστεί ισχυρά τυποποιήσιμη (strongly typed), σε αντίθετη περίπτωση, ασθενώς τυποποιήσιμη (weakly typed). Οι όροι αυτοί δε χρησιμοποιούνται με αυστηρό τρόπο.

Στατικοί τύποι

Μια γλώσσα προγραμματισμού λέγεται ότι χρησιμοποιεί στατικούς τύπους όταν ο έλεγχος τύπων γίνεται κατά τη διάρκεια του χρόνου μεταγλώττισης αντί του χρόνου εκτέλεσης. Οι γλώσσες με στατικούς τύπους περιλαμβάνουν την Ada, την ActionScript 3, τη C, τη C++, τη C#, την Eiffel, την F#, τη Go, τη JADE, τη Java, τη Fortran, τη Haskell, την ML, την Objective-C, την Pascal, την Perl (που διακρίνει μεταξύ βαθμωτών τιμών (scalars), πινάκων, πινάκων κατακερματισμού και υπορουτινών) και τη Scala. Επειδή ο στατικός έλεγχος είναι μια περιορισμένη μορφή επαλήθευσης προγράμματος (program verification) (βλ. ασφάλεια τύπων), επιτρέπει σε πολλά σφάλματα τύπων να εντοπίζονται νωρίς κατά τη διάρκεια του κύκλου της ανάπτυξης του λογισμικού. Οι στατικοί ελεγκτές τύπων εκτιμούν μόνο την πληροφορία που μπορούν να προσδιορίσουν στο χρόνο μεταγλώττισης αλλά μπορούν να επαληθεύσουν ότι οι συνθήκες που ελέγχονται ισχύουν για όλες τις πιθανές εκτελέσεις του προγράμματος, με αποτέλεσμα να μη χρειάζεται να επαναλαμβάνεται ο έλεγχος τύπων κάθε φορά που εκτελείται το πρόγραμμα. Η εκτέλεση του προγράμματος μπορεί επίσης να γίνει πιο αποδοτική (σε ταχύτητα ή σε κατανάλωση μνήμης) όταν λείπει ο έλεγχος τύπων στο χρόνο εκτέλεσης και υπάρχουν βελτιστοποιήσεις.

Επειδή αναλύουν πληροφορία στο χρόνο μεταγλώττισης, και άρα δεν έχουν διαθέσιμη πληροφορία τύπων του χρόνου εκτέλεσης, οι στατικοί ελεγκτές τύπων είναι συντηρητικοί. Μπορεί να απορρίψουν κάποια προγράμματα που έχουν καλή συμπεριφορά στο χρόνο εκτέλεσης, αλλά δε φαίνεται στατικά ότι έχουν σωστούς τύπους. Για παράδειγμα, ακόμα και αν η έκφραση <πολύπλοκη συνθήκη> πάντα αποτιμάται σε αληθές στο χρόνο εκτέλεσης, ένα πρόγραμμα που περιέχει τον κώδικα

αν <πολύπλοκη συνθήκη> τότε 42 αλλιώς <σφάλμα τύπου>

θα απορριφθεί ως πρόγραμμα με λάθος τύπους, γιατί μια στατική ανάλυση δε μπορεί να βρει ότι ο κώδικας στο σκέλος αλλιώς δε θα εκτελεστεί ποτέ. Η συντηρητική συμπεριφορά των στατικών ελεγκτών τύπων αποτελεί πλεονέκτημα όταν η <πολύπλοκη συνθήκη> αποτιμάται σε ψευδές σπάνια: ένας στατικός ελεγκτής τύπων μπορεί να εντοπίσει σφάλματα τύπων σε σπάνια χρησιμοποιούμενα μονοπάτια μέσα στον κώδικα. Χωρίς το στατικό έλεγχο τύπων, ακόμα και δοκιμές κάλυψης κώδικα (code coverage) με 100% κάλυψη, μπορεί να μη βρουν αυτά τα σφάλματα. Οι δοκιμές μπορεί να μη τα εντοπίσουν γιατί πρέπει να ληφθεί υπόψη ο συνδυασμός όλων των σημείων που δημιουργούνται τιμές και όλων των σημείων που μια τιμή χρησιμοποιείται.

Οι γλώσσες προγραμματισμού με στατικούς τύπους που χρησιμοποιούνται συχνότερα, δεν είναι επισήμως ασφαλείς ως προς τους τύπους τους (type safe). Περιέχουν "παραθυράκια" ("loopholes") στον ορισμό τους, ώστε ο προγραμματιστής να μπορεί να γράφει κώδικα που να αποφεύγει την επαλήθευση του στατικού ελεγκτη τύπων, για να λύσει κάποια προβλήματα. Για παράδειγμα, οι περισσότερες γλώσσες τύπου C έχουν τέτοιες εντολές ("type punning"), ενώ η Haskell έχει χαρακτηριστικά όπως η συνάρτηση unsafePerformIO: αυτές οι λειτουργίες μπορεί να μην είναι ασφαλείς στο χρόνο εκτέλεσης, επειδή δημιουργούν ανεπιθύμητη συμπεριφορά λόγω εσφαλμένων τύπων των τιμών όταν εκτελείται το πρόγραμμα.

Δυναμικοί τύποι

Μια γλώσσα προγραμματισμού λέγεται ότι έχει δυναμικούς τύπους όταν το μεγαλύτερο μέρος του ελέγχου τύπων της εκτελείται στο χρόνο εκτέλεσης αντί του χρόνου μεταγλώττισης. Στους δυναμικούς τύπους, οι τιμές έχουν τύπους αλλά οι μεταβλητές δεν έχουν με αποτέλεσμα μια μεταβλητή να μπορεί να αναφέρεται σε τιμές κάθε είδους. Οι γλώσσες με δυναμικούς τύπους περιλαμβάνουν την APL, την Erlang, τη Groovy, τη JavaScript, τη Lisp, τη Lua, αυτές των MATLAB/GNU Octave, την Perl (όσον αφορά τους τύπου που ορίζονται από το χρήστη αλλά όχι τους ενσωματωμένους), την PHP, την Prolog, την Python, τη Ruby, τη Smalltalk και την Tcl. Οι δυναμικοί τύποι μπορούν να είναι πιο ευέλικτοι από τους στατικούς τύπους (π.χ. επιτρέποντας σε ένα πρόγραμμα να παράγει τύπους και λειτουργίες με βάση δεδομένα στο χρόνο εκτέλεσης), αλλά εις βάρος λιγότερων εγγυήσεων εκ των προτέρων. Αυτό οφείλεται στο ότι μια γλώσσα με δυναμικούς τύπους δέχεται και προσπαθεί να εκτελέσει ορισμένα προγράμματα που θεωρούνται μη έγκυρα από τον στατικό ελεγκτή τύπων.

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

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

Η ανάπτυξη λογισμικού σε γλώσσες με δυναμικούς τύπους συχνά υποστηρίζεται από πρακτικές όπως ο έλεγχος μονάδας (unit testing). Οι δοκιμές αποτελούν βασική πρακτική στην επαγγελματική ανάπτυξη λογισμικού και είναι ιδιαίτερα σημαντικές σε γλώσσες με δυναμικούς τύπους. Στην πράξη, οι δοκιμές μπορούν να εντοπίσουν ένα ευρύτερο πεδίο σφαλμάτων σε σχέση με το στατικό έλεγχο τύπων αλλά δεν είναι το ίδιο πλήρεις και εξαντλητικές.

Συνδυασμοί δυναμικών και στατικών τύπων

Η παρουσία στατικών τύπων σε μια γλώσσα προγραμματισμού δεν αποκλείει απαραίτητα τους μηχανισμούς των δυναμικών τύπων. Στη Java για παράδειγμα, καθώς και σε άλλες αντικειμενοστρεφείς γλώσσες, αν και χρησιμοποιούνται οι στατικοί τύποι, κάποιες λειτουργίες (downcasting) απαιτούν ελέγχους στο χρόνο εκτέλεσης, μια μορφή δυναμικών τύπων.

Κάποιες γλώσσες, όπως η Clojure, έχουν δυναμικούς τύπους αλλά επιτρέπουν τη χρήση ρητών σημειώσεων τύπων (explicit type hints) που έχουν ως αποτέλεσμα στατικούς τύπους. Ένας πιθανός λόγος που χρησιμοποιούνται είναι για τη βελτιστοποίηση κώδικα με απαιτήσεις ταχύτητας, με βάση τους στατικούς τύπους.

Από την έκδοση 4.0, το .NET Framework υποστηρίζει μια παραλλαγή των δυναμικών τύπων μέσω του χώρου ονομάτων System.Dynamic όπου ένα στατικό αντικείμενο (static) τύπου 'δυναμικό' ('dynamic') χρησιμοποιείται ως χώρος που το σύστημα χρόνου εκτέλεσης της πλατφόρμας .NET ρωτά για τις δυναμικές δυνατότητές του ώστε να επιλύσει μια αναφορά σε κάποιο αντικείμενο.

Στατικός και δυναμικός έλεγχος τύπων στην πράξη

Η απόφαση να χρησιμοποιηθούν στατικοί ή δυναμικοί τύποι εξαρτάται από πολλούς παράγοντες, με κάποιες αναγκαίες υποχωρήσεις σε κάθε περίπτωση (trade-offs).

Οι στατικοί τύποι μπορούν να εντοπίσουν σφάλματα τύπων στο χρόνο μεταγλώττισης, κάτι που κανονικά κάνει ένα πρόγραμμα πιο αξιόπιστο. Όμως, οι προγραμματιστές διαφωνούν σχετικά με το πόσο συχνά συμβαίνουν σφάλματα τύπων και ποιο ποσοστό από τα λάθη κατά την ανάπτυξη ενός προγράμματος εντοπίζεται με τους στατικούς τύπους. Οι υποστηρικτές των στατικών τύπων πιστεύουν ότι ένα πρόγραμμα είναι πιο αξιόπιστο όταν έχει περάσει τον έλεγχο τύπων ενώ οι υποστηρικτές των δυναμικών τύπων δείχνουν κατανεμημένο κώδικα που έχει αποδειχτεί αξιόπιστος. Η ισχύς των στατικών τύπων αυξάνεται όσο αυξάνεται και η ισχύς του συστήματος τύπων. Οι υποστηρικτές των γλωσσών με εξαρτώμενους τύπους (dependent types) όπως η Dependent ML και η Epigram, θεωρούν ότι σχεδόν όλα τα σφάλματα μπορούν να θεωρηθούν σφάλματα τύπων, αν οι τύποι που χρησιμοποιούνται σε ένα πρόγραμμα έχουν δηλωθεί σωστά από τον προγραμματιστή ή έχουν εξαχθεί σωστά από το μεταγλωττιστή.

Οι στατικοί τύποι συνήθως έχουν ως αποτέλεσμα μεταγλωττισμένο κώδικα που εκτελείται πιο γρήγορα. Όταν ο μεταγλωττιστής γνωρίζει ποιοι ακριβώς τύποι δεδομένων χρησιμοποιούνται, μπορεί να παράγει βελτιστοποιημένο κώδικα. Κάποιες γλώσσες με δυναμικούς τύπους όπως η Common Lisp επιτρέπουν προαιρετικά τη δήλωση τύπων για τη βελτιστοποίηση κατά αυτόν τον τρόπο. Οι στατικοί τύποι αποτελούν επομένως τη γενίκευση αυτού του φαινομένου σε όλο το εύρος του κώδικα. Βλ. βελτιστοποίηση (optimization).

Αντίθετα, οι δυναμικοί τύποι μπορούν να επιτρέψουν στο μεταγλωττιστή να εκτελείται πιο γρήγορα και στο διορθωτή να φορτώνει δυναμικά νέο κώδικα, επειδή οι αλλαγές στον πηγαίο κώδικα στις γλώσσες με δυναμικούς τύπους έχουν ως αποτέλεσμα λιγότερο περαιτέρω έλεγχο και λιγότερο κώδικα για επανεξέταση. Κάτι τέτοιο σε ορισμένες περιπτώσεις μπορεί να μικρύνει τον κύκλο διόρθωση-μεταγλώττιση-δοκιμή-αποσφαλμάτωση (edit-compile-test-debug).

Οι γλώσσες με στατικούς τύπους που δεν έχουν εξαγωγή τύπων (όπως η Java και η C) απαιτούν ο προγραμματιστής να δηλώνει όλους τους τύπους που πρόκειται να χρησιμοποιήσει μια μέθοδος ή μια συνάρτηση. Αυτό μπορεί να αποτελέσει επιπλέον τεκμηρίωση για το πρόγραμμα, την οποία ο μεταγλωττιστής δεν επιτρέπει στον προγραμματιστή να αγνοήσει ή να μην αντιστοιχεί στον κώδικα. Όμως μια γλώσσα μπορεί να έχει στατικούς τύπους χωρίς να απαιτεί δηλώσεις τύπων (π.χ. η Haskell, η Scala, και σε κάποιο βαθμό η C#), επομένως αυτό δεν είναι απαραίτητη συνέπεια των στατικών τύπων.

Οι δυναμικοί τύποι επιτρέπουν δομές που οι στατικοί τύποι απορρίπτουν ως μη επιτρεπτές. Για παράδειγμα, επιτρέπουν συναρτήσεις τύπου αποτίμησε (eval), που εκτελούν αυθαίρετα κομμάτια κώδικα. Επιπλέον οι δυναμικοί τύποι χειρίζονται καλύτερα κώδικα σε μεταβατική φάση (transitional code) και τη γρήγορη ανάπτυξη πρωτοτύπων (prototyping), όπως η χρήση μιας κενής δομής δεδομένων (ψευδο-αντικείμενο, mock object) στη θέση μιας πλήρους δομής δεδομένων (συνήθως για πειραματισμούς και δοκιμές).

Οι δυναμικοί τύποι χρησιμοποιούνται στο duck typing που μπορεί να υποστηρίζει ευκολότερη επαναχρησιμοποίηση κώδικα.

Οι δυναμικοί τύποι συνήθως διευκολύνουν το μεταπρογραμματισμό (metaprogramming). Για παράδειγμα, τα πρότυπα της C++ (templates) συνήθως είναι δυσκολότερα στη χρήση από αντίστοιχο κώδικα σε Ruby ή Python. Πιο προχωρημένες δομές χρόνου εκτέλεσης όπως οι μετακλάσεις και η ενδοσκόπηση (introspection) συχνά είναι πιο δύσχρηστες σε γλώσσες με στατικούς τύπους.

Ισχυροί και ασθενείς τύποι

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

Οι ασθενείς τύποι (Weak typing) σημαίνουν ότι μια γλώσσα έμμεσα μετατρέπει τους τύπους. Έστω το εξής παράδειγμα:

var x := 5;    // (1)  (η x είναι ακέραιος)
var y := "37"; // (2)  (η y είναι συμβολοσειρά)
x + y;         // (3)  (?)

Σε μια γλώσσα με ασθενείς τύπους, το αποτέλεσμα της τελευταίας λειτουργίας δεν είναι ξεκάθαρο. Κάποιες γλώσσες όπως η Visual Basic, θα παρήγαγαν εκτελέσιμο κώδικα που όταν εκτελεστεί να έχει αποτέλεσμα 42: το σύστημα θα μετέτρεπε τη συμβολοσειρά "37" στον αριθμό 37 ώστε να καταφέρει να βρει νόημα στη λειτουργία της πρόσθεσης. Άλλες γλώσσες όπως η JavaScript θα παρήγαγαν το αποτέλεσμα "537": το σύστημα θα μετέτρεπε τον αριθμό 5 στη συμβολοσειρά "5" και στη συνέχεια θα συνένωνε τις δύο συμβολοσειρές. Και στη Visual Basic και στη JavaScript, ο τύπος του αποτελέσματος ορίζεται από κανόνες που αφορούν και τις δύο παραμέτρους μιας λειτουργίας. Σε κάποιες γλώσσες όπως η AppleScript, ο τύπος της τιμής που προκύπτει καθορίζεται από τον τύπο της παραμέτρου που είναι στα αριστερά της έκφρασης.

Στη C μια μετατροπή (cast) που αποτυγχάνει δείχνει το πρόβλημα που μπορεί να εμφανιστεί αν λείπουν οι ισχυροί τύποι - αν ο προγραμματιστής μετατρέπει μια τιμή από έναν τύπο σε έναν άλλο στη C, όχι μόνο πρέπει ο μεταγλωττιστής να το επιτρέψει στο χρόνο μεταγλώττισης αλλά να το επιτρέψει και το ίδιο το σύστημα χρόνου εκτέλεσης. Αυτό μπορεί να έχει ως αποτέλεσμα μικρότερο και γρηγορότερο κώδικα C, αλλά δυσκολεύει την αποσφαλμάτωση.

Συστήματα με ασφαλείς και μη ασφαλείς τύπους

Ένας τρίτος τρόπος κατηγοριοποίησης του συστήματος τύπων μιας γλώσσας προγραμματισμού βασίζεται στην ασφάλεια των λειτουργιών με τύπους και των μετατροπών. Μια γλώσσα θεωρείται ότι έχει "ασφαλείς τύπους" ("type-safe") αν δεν επιτρέπει λειτουργίες ή μετατροπές που να οδηγούν σε εσφαλμένες καταστάσεις.

Άλλοι όροι που χρησιμοποιούνται είναι γλώσσα με ασφαλή μνήμη (memory-safe language) ή ασφαλής γλώσσα (safe language), που περιγράφουν γλώσσες που δεν επιτρέπουν μη ορισμένες λειτουργίες. Για παράδειγμα, μια γλώσσα αυτού του τύπου ελέγχει τα όρια των πινάκων ή εγγυάται με κάποιον άλλο τρόπο στατικά (π.χ. στη μεταγλώττιση) ότι η πρόσβαση εκτός ορίων ενός πίνακα θα προκαλέσει σφάλμα στο χρόνο μεταγλώττισης και ίσως και στο χρόνο εκτέλεσης.

var x := 5;     // (1)
var y := "37";  // (2)
var z := x + y; // (3)

Σε γλώσσες όπως η Visual Basic, η μεταβλητή z του παραδείγματος παίρνει την τιμή 42. Αν και ο προγραμματιστής μπορεί να μην ήθελε κάτι τέτοιο, το αποτέλεσμα ορίζεται στη γλώσσα και το πρόγραμμα δεν αποτυγχάνει, ούτε δίνει κάποια λάθος τιμή στη z. Υπό αυτό το πρίσμα, τέτοιες γλώσσες έχουν ασφαλείς τύπους - αν όμως η τιμή της y ήταν μια συμβολοσειρά που δε μπορεί να μετατραπεί σε αριθμό (π.χ. "γεια σου, κόσμε"), το αποτέλεσμα δε θα ήταν ορισμένο. Επομένως, αν και τέτοιες γλώσσες έχουν ασφαλείς τύπους (τα προγράμματά τους δεν αποτυγχάνουν), μπορούν εύκολα να παράγουν ανεπιθύμητα αποτελέσματα.

Έστω ο εξής κώδικας σε C:

int x = 5;
char y[] = "37";
char* z = x + y;

Σε αυτό το παράδειγμα η z δείχνει σε μια διεύθυνση μνήμης 5 χαρακτήρες μετά την y, ισοδύναμα με τρεις χαρακτήρες μετά τον τερματικό χαρακτήρα μηδέν της συμβολοσειράς στην οποία δείχνει η y. Η διεύθυνση αυτής της θέσης μνήμης δεν ορίζεται και μπορεί να βρίσκεται εκτός της μνήμης που βλέπει το πρόγραμμα. Ακόμα και ο απλός υπολογισμός ενός τέτοιου δείκτη μπορεί να έχει ως αποτέλεσμα ακαθόριστη συμπεριφορά (ακόμα και κατάρρευση του προγράμματος) σύμφωνα με το πρότυπο της C, και στα πιο πολλά συστήματα η απλή χρήση της διεύθυνσης της z σε αυτό το σημείο θα προκαλούσε αστοχία του προγράμματος. Επομένως το πρόγραμμα έχει σωστούς τύπους αλλά δεν είναι ασφαλές ως προς τη μνήμη - κάτι τέτοιο δε θα συνέβαινε σε μια γλώσσα με ασφαλείς τύπους.

Πολυμορφισμός και τύποι

Ο όρος "πολυμορφισμός" ("polymorphism") αναφέρεται στη δυνατότητα του κώδικα να εφαρμόζεται σε τιμές διαφορετικών τύπων ή στη δυνατότητα διαφορετικών στιγμιοτύπων (instances) της ίδιας δομής δεδομένων να περιέχουν στοιχεία διαφορετικών τύπων. Τα συστήματα τύπων που επιτρέπουν πολυμορφισμό συνήθως το κάνουν για να αυξήσουν τη δυνατότητα επαναχρησιμοποίησης κώδικα: σε μια γλώσσα με πολυμορφισμό, ο προγραμματιστής χρειάζεται να υλοποιήσει μια δομή δεδομένων όπως η λίστα ή ο πίνακας συσχέτισης (associative array) μια φορά, αντί για κάθε τύπο στοιχείων που πρόκειται να χρησιμοποιηθεί. Για αυτόν το λόγο, κάποιες μορφές πολυμορφισμού ονομάζονται generic programming. Οι τυπο-θεωρητικές βάσεις του πολυμορφισμού είναι συγγενείς με αυτές της αφαίρεσης (abstraction), του modularity και (κάποιες φορές) των υποτύπων (subtyping).

Duck typing

Στο "duck typing", μια εντολή που καλεί μια μέθοδο m ενός αντικειμένου δε βασίζεται στο δηλωμένο τύπο του αντικειμένου αλλά μόνο στο αν αυτό το αντικείμενο υλοποιεί τη μέθοδο που καλείται. Στα συστήματα με duck typing, ο τύπος ενός αντικειμένου μπορεί να θεωρηθεί ότι εξαρτάται από το ίδιο το αντικείμενο και καθορίζεται από το ποιες μεθόδους υλοποιεί, επομένως αυτά τα συστήματα έχουν εξ ορισμού ασφαλείς τύπους αφού μπορούν να κληθούν μόνο μέθοδοι που πραγματικά υλοποιεί ένα αντικείμενο. Μπορεί επίσης να θεωρηθεί ότι το αντικείμενο ανήκει σε πολλούς τύπους, οι οποίοι περιλαμβάνουν και τον τύπο που περιγράφει το γεγονός ότι "έχει μια μέθοδο m." Ο έλεγχος τύπων όμως συμβαίνει στο χρόνο εκτέλεσης, όταν ζητηθεί, κάθε φορά που μια μέθοδος m πρέπει να εκτελεστεί, και όχι στο χρόνο μεταγλώττισης ή φόρτωσης.

Το duck typing διαφέρει από τους δομικούς τύπους (structural typing) γιατί αν το τμήμα (όλης της δομής της μονάδας κώδικα) που χρειάζεται για ένα δεδομένο τοπικό υπολογισμό υπάρχει στο χρόνο εκτέλεσης, το σύστημα ικανοποιείται από την ανάλυση και την ταυτοποίηση τύπων. Από την άλλη πλευρά, ένα σύστημα δομικών τύπων θα απαιτούσε την ανάλυση όλης της δομής της μονάδας κώδικα στο χρόνο μεταγλώττισης για να καθορίσει την ταυτότητα τύπων ή τις μεταξύ τους εξαρτήσεις.

Το duck typing διαφέρει από ένα ονομαστικό σύστημα τύπων (nominal type system) από διάφορες απόψεις. Η κύρια είναι ότι καθορίζει την πληροφορία τύπων στο χρόνο εκτέλεσης (και όχι στο χρόνο μεταγλώττισης) και το όνομα ενός τύπου δεν έχει σημασία κατά την εύρεση της ταυτότητας ή των εξαρτήσεων τύπων - χρειάζεται μόνο μερική πληροφορία για τη δομή, σε κάθε στιγμή της εκτέλεσης του προγράμματος.

Ο όρος αρχικά προέκυψε από τον Alex Martelli, στα πλαίσια της κοινότητας της Python, με τη βασική αρχή του duck typing (όσον αφορά τις τιμές της γλώσσας) να είναι: "αν περπατάει σαν πάπια (σ.σ. duck) και κάνει σαν πάπια, τότε είναι πάπια".

Εξειδικευμένα συστήματα τύπων

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

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

Οι εξαρτώμενοι τύποι (dependent types) βασίζονται στην ιδέα της χρήσης δεδομένων για την ακριβέστερη περιγραφή του τύπου κάποιων άλλων δεδομένων. Για παράδειγμα ο τύπος "matrix(3,3)" μπορεί να περιγράφει έναν 3×3 πίνακα. Τότε μπορούν να οριστούν κανόνες τυποποίησης όπως ο ακόλουθος του πολλαπλασιασμού πινάκων:

matrix_multiply : matrix(k,m) × matrix(m,n) → matrix(k,n)

όπου k, m, n είναι αυθαίρετες ακέραιες τιμές. Μια παραλλαγή της ML, που ονομάζεται Dependent ML, βασίζεται σε αυτό το σύστημα τύπων, αλλά επειδή ο κλασικός έλεγχος των εξαρτώμενων τύπων είναι μη-υπολογίσιμο πρόβλημα, προγράμματα που τους χρησιμοποιούν δε μπορούν πάντα να ελεγχθούν ότι έχουν τους σωστούς τύπους χωρίς κάποιας μορφής περιορισμούς. Η Dependent ML περιορίζει τον τύπο της ισότητας που μπορεί να υπολογίσει στην αριθμητική Presburger. Άλλες γλώσσες όπως η Epigram έχουν υπολογίσιμους τύπους σε όλες τις εκφράσεις της γλώσσας, κάνοντας υπολογίσιμο και τον έλεγχο τύπων, ενώ επίσης μπορεί μια γλώσσα να είναι Τιούρινγκ-πλήρης (Turing complete) με το κόστος του μη-υπολογίσιμου ελέγχου τύπων, όπως στην Cayenne.

Γραμμικοί τύποι

Οι γραμμικοί τύποι (linear types), που βασίζονται στη θεωρία της γραμμικής λογικής (linear logic), και σχετίζονται με τους τύπους μοναδικότητας (uniqueness types), είναι τύποι αποδίδονται σε τιμές που έχουν την ιδιότητα να υπάρχει ακριβώς μια αναφορά σε αυτές σε κάθε χρονική στιγμή. Είναι σημαντικοί για την περιγραφή μεγάλων τιμών που δεν αλλάζουν (immutable values) όπως οι συμβολοσειρές ή τα αρχεία, γιατί κάθε λειτουργία που ταυτόχρονα καταστρέφει ένα γραμμικό αντικείμενο και ταυτόχρονα δημιουργεί ένα παρόμοιο αντικείμενο (όπως ο κώδικας 'str = str + "a"') μπορεί να βελτιστοποιηθεί σαν επιτόπου τροποποίηση (in-place mutation). Κανονικά κάτι τέτοιο δε θα ήταν δυνατό, γιατί τέτοιες αλλαγές μπορεί να προκαλούσαν παρενέργειες σε μέρη του προγράμματος που έχουν αναφορές προς το αντικείμενο, κατά παράβαση της διαφάνειας αναφοράς (referential transparency). Χρησιμοποιούνται επίσης στο λειτουργικό σύστημα Singularity για επικοινωνία μεταξύ των διεργασιών, βεβαιώνοντας στατικά ότι οι διαδικασίες δε μπορούν να μοιράζονται αντικείμενα σε κοινή μνήμη, ώστε να αποφεύγονται καταστάσεις απροσδιοριστίας (race conditions). Η γλώσσα Clean (που είναι παρόμοια με τη Haskell) χρησιμοποιεί ένα σχετικό σύστημα τύπων ώστε να έχει καλύτερη ταχύτητα εκτέλεσης, μένοντας ασφαλής.

Τύποι τομής

Οι τύποι τομής (intersection types) περιγράφουν τιμές που ανήκουν ταυτόχρονα σε δύο άλλους τύπους, με επικαλυπτόμενα πεδία τιμών. Για παράδειγμα, στις περισσότερες υλοποιήσεις της C ο χαρακτήρας με πρόσημο (signed char) έχει εύρος μεταξύ -128 και 127 και ο χαρακτήρας χωρίς πρόσημο (unsigned char) έχει εύρος μεταξύ 0 και 255, επομένως ο τύπος τομής αυτών των δύο τύπων έχει εύρος μεταξύ 0 και 127. Ένας τέτοιος τύπος τομής θα μπορούσε να περαστεί με ασφάλεια σε συναρτήσεις που περιμένουν χαρακτήρες με πρόσημο ή χωρίς πρόσημο, γιατί και οι δύο τύποι είναι συμβατοί.

Οι τύποι τομής είναι χρήσιμοι για την περιγραφή υπερφορτωμένων (overloaded) τύπων συναρτήσεων: για παράδειγμα, αν ο τύπος των συναρτήσεων που δέχονται έναν ακέραιο και επιστρέφουν ακέραιο είναι "int → int", και ο τύπος των συναρτήσεων που δέχονται έναν αριθμό κινητής υποδιαστολής and επιστρέφουν αριθμό κινητής υποδιαστολής είναι "float → float", τότε η τομή αυτών των δύο τύπων μπορεί να χρησιμοποιηθεί για συναρτήσεις που κάνουν είτε το πρώτο είτε το δεύτερο, με βάση τον τύπο της παραμέτρου τους. Μια τέτοια συνάρτηση μπορεί να περαστεί σε κάποια άλλη συνάρτηση που περιμένει συνάρτηση τύπου "int → int" με ασφάλεια - απλά δε θα χρησιμοποιούσε τη λειτουργικότητα του τύπου "float → float".

Σε μια ιεραρχία με υποκλάσεις, η τομή ενός τύπου και ενός γονικού τύπου είναι ο τύπος χαμηλότερα στην ιεραρχία. Η τομή αδελφικών τύπων είναι ο κενός τύπος.

Η γλώσσα Forsythe περιλαμβάνει μια γενική υλοποίηση των τύπων τομής. Μια σχετική μορφή είναι οι refinement types.

Τύποι ένωσης

Οι τύποι ένωσης (union types) περιγράφουν τιμές που ανήκουν σε έναν μόνο από δύο τύπους. Για παράδειγμα, στη C, ο χαρακτήρας με πρόσημο έχει εύρος μεταξύ -128 και 127, και ο χαρακτήρας χωρίς πρόσημο έχει εύρος μεταξύ 0 και 255, επομένως η ένωση αυτών των δύο τύπων έχει εύρος μεταξύ -128 και 255. Κάθε συνάρτηση που χειρίζεται αυτόν τον τύπο ένωσης θα έπρεπε να χειρίζεται τους ακεραίους σε όλο αυτό το εύρος. Γενικά, οι μόνες έγκυρες λειτουργίες σε έναν τύπο ένωσης είναι αυτές που είναι έγκυρες και στους δύο τύπους που ενώνονται. Η δομή "union" της C είναι παρόμοια με τους τύπους ένωσης, αλλά δεν έχει ασφαλή τύπο γιατί επιτρέπει λειτουργίες που είναι έγκυρες σε οποιονδήποτε από τους δύο τύπους, αντί και για τους δύο. Οι τύποι ένωσης είναι σημαντικοί στην ανάλυση προγράμματος, όπου χρησιμοποιούνται για την αναπαράσταση συμβολικών τιμών, των οποίων η ακριβής φύση (π.χ. τιμή, τύπος) δεν είναι γνωστή.

Σε μια ιεραρχία με υποκλάσεις, η ένωση ενός τύπου και ενός προγόνου του, είναι ο πρόγονος. Η ένωση δύο αδελφικών τύπων είναι υποτύπος του κοινού τους προγόνου (όλες οι λειτουργίες που επιτρέπονται στον κοινό πρόγονο επιτρέπονται και στον τύπο ένωσης, αλλά μπορεί επίσης να υπάρχουν και άλλες κοινές λειτουργίες).

Υπαρξιακοί τύποι

Οι υπαρξιακοί τύποι (existential types) χρησιμοποιούνται συχνά μαζί με τους τύπους εγγραφής (record types) στην αναπαράσταση μονάδων κώδικα (modules) και αφηρημένων δομών δεδομένων (abstract data types), λόγω της ικανότητάς τους να διαχωρίζουν μεταξύ υλοποίησης και διαπροσωπείας (interface). Για παράδειγμα, ο τύπος "T = ∃X { a: X; f: (X → int); }" περιγράφει τη διαπροσωπεία μιας μονάδας κώδικα που έχει ένα μέλος δεδομένων τύπου X και μια συνάρτηση που παίρνει μια παράμετρο του ίδιου τύπου X και επιστρέφει έναν ακέραιο. Αυτό μπορεί να υλοποιηθεί με διάφορους τρόπους, για παράδειγμα:

• intT = { a: int; f: (int → int); }
• floatT = { a: float; f: (float → int); }

Οι παραπάνω τύποι είναι υποτύποι του γενικότερου υπαρξιακού τύπου T και αντιστοιχούν σε συμπαγείς τύπους της υλοποίησης, επομένως κάθε τιμή ενός από αυτούς τους τύπους είναι τιμή του τύπου T. Έστω μία τιμή "t" τύπου "T", τότε ξέρουμε ότι η "t.f(t.a)" έχει σωστό τύπο, όποιος και να είναι ο αφηρημένος τύπος X. Αυτό επιτρέπει ευελιξία στην επιλογή τύπων που να ταιριάζουν σε κάθε εφαρμογή, ενώ οι χρήστης του αφηρημένου τύπου χρησιμοποιούν μόνο τον τύπο της διαπροσωπείας—τον υπαρξιακό τύπο—και δεν έρχονται σε επαφή με αυτήν την επιλογή.

Γενικά ο ελεγκτής τύπων δε μπορεί να βρει αυτόματα σε ποιόν υπαρξιακό τύπο ανήκει μια μονάδα κώδικα. Στο παραπάνω παράδειγμα, ο intT { a: int; f: (int → int); } θα μπορούσε να έχει επίσης τύπο ∃X { a: X; f: (int → int); }. Η ευκολότερη λύση θα ήταν να σημειώνεται κάθε μονάδα κώδικα με τον τύπο που προορίζεται να έχει, π.χ.:

• intT = { a: int; f: (int → int); } as ∃X { a: X; f: (X → int); }

Αν και οι αφηρημένοι τύποι δεδομένων και οι μονάδες κώδικα είχαν υλοποιηθεί από παλιά στις γλώσσες προγραμματισμού, το 1988 εδραιώθηκε η τυπική θεωρία από τον John C. Mitchell και τον Gordon Plotkin, με το σύνθημα: "Οι αφηρημένοι τύποι δεδομένων έχουν υπαρξιακό τύπο" Η θεωρία είναι λ-λογισμός με τύπους δεύτερης τάξης με τύπους, όμοιος με το Σύστημα F, αλλά με υπαρξιακούς αντί για καθολικούς ποσοδείκτες.

Ρητή ή έμμεση δήλωση και εξαγωγή

Πολλά στατικά συστήματα τύπων, όπως της C και της Java, απαιτούν δηλώσεις τύπων (type declarations): ο προγραμματιστής πρέπει να αντιστοιχίσει ρητά κάθε μεταβλητή με ένα συγκεκριμένο τύπο. Άλλα συστήματα, όπως της Haskell, κάνουν εξαγωγή τύπων (type inference): ο μεταγλωττιστής βγάζει συμπεράσματα για τους τύπους των μεταβλητών, με βάση πώς χρησιμοποιούνται αυτές από τον προγραμματιστή. Για παράδειγμα, αν η συνάρτηση f(x,y) προσθέτει τις μεταβλητές x και y, ο μεταγλωττιστής μπορεί να συμπεράνει ότι οι x και y είναι αριθμοί – εφόσον η πρόσθεση ορίζεται μόνο για αριθμούς. Επομένως, κάθε κλήση στην f οπουδήποτε στο πρόγραμμα που χρησιμοποιεί ένα μη-αριθμητικό τύπο (π.χ. συμβολοσειρά ή λίστα) σαν όρισμά της, θα αποτελούσε λάθος.

Οι αριθμητικές σταθερές, οι σταθερές συμβολοσειρών και οι εκφράσεις στον κώδικα συνήθως υπονοούν ένα συγκεκριμένο περιβάλλον στο οποίο χρησιμοποιούνται. Για παράδειγμα, η έκφραση 3.14 θα μπορούσε να υπονοεί τον τύπο των αριθμών κινητής υποδιαστολής (floating-point), ενώ η [1, 2, 3] θα μπορούσε να υπονοεί μια λίστα από ακέραιους.

Η εξαγωγή τύπων γενικά μπορεί να γίνεται μόνο όταν είναι υπολογίσιμο πρόβλημα στη θεωρία τύπων που χρησιμοποιείται. Επιπλέον, ακόμα και αν η εξαγωγή γενικά δεν είναι υπολογίσιμη για μια δεδομένη θεωρία τύπων, η εξαγωγή συνήθως είναι δυνατή για ένα μεγάλο υποσύνολο προγραμμάτων στην πράξη. Το σύστημα τύπων της Haskell, παραλλαγή του Hindley-Milner, που είναι περιορισμός του Συστήματος Fω στους αποκαλούμενους πολυμορφικούς τύπους rank-1, στους οποίους η εξαγωγή τύπων είναι υπολογίσιμο πρόβλημα. Οι περισσότεροι μεταγλωττιστές της Haskell επιτρέπουν ως επέκταση, πολυμορφισμό για κάθε rank, κάτι που όμως κάνει την εξαγωγή τύπων μη υπολογίσιμη. (Ο έλεγχος τύπων όμως είναι υπολογίσιμος και τα προγράμματα rank-1 εξακολουθούν να έχουν εξαγωγή τύπων ενώ τα προγράμματα ανώτερου rank απορρίπτονται αν δε δοθούν ρητές σημειώσεις τύπων.)

Οι τύποι των τύπων

Ο τύπος τύπων είναι είδος (kind). Τα είδη εμφανίζονται στον προγραμματισμό με τύπους (typeful programming), όπως οι κατασκευαστές τύπων (type constructors) στη γλώσσα Haskell.

Οι τύποι έχουν πολλές κατηγορίες:

• Πρωτογενείς τύποι (primitive types) – οι απλούστεροι τύποι, π.χ. οι ακέραιοι και οι αριθμοί κινητής υποδιαστολής
  • Τιμή αλήθειας (boolean)
  • Τύποι integral – τύποι ολόκληρων αριθμών, π.χ. ακέραιοι ή φυσικοί αριθμοί
  • Τύποι κινητής υποδιαστολής (floating point) – τύποι αριθμών σε αναπαράσταση κινητής υποδιαστολής
• Τύποι αναφοράς (reference types)
• Τύποι επιλογής (option types)
  • Nullable types
• Σύνθετοι τύποι – τύποι που αποτελούνται από βασικούς τύπους, π.χ. πίνακες ή εγγραφές

  Αφηρημένοι τύποι δεδομένων

• Αλγεβρικοί τύποι
• Υποτύποι
• Εξαγόμενοι τύποι (derived types))
• Τύποι αντικειμένων, π.χ. μεταβλητές τύπων
• Μερικοί τύποι (partial types)
• Αναδρομικοί τύποι
• Συναρτησιακοί τύποι, π.χ. δυαδικές συναρτήσεις
• Τύποι καθολικά ποσοδεικτούμενοι, όπως οι παραμετρικοί τύποι
• Τύποι υπαρξιακά ποσοδεικτούμενοι, όπως οι μονάδες κώδικα (modules)
• Τύποι εκλέπτυνσης (refinement types) – τύποι που ορίζουν υποσύνολα άλλων τύπων
• Εξαρτώμενοι τύποι (dependent types) – τύποι που εξαρτώνται από όρους (τιμές)
• Τύποι ιδιοκτησίας (ownership types) – τύποι που περιγράφουν ή περιορίζουν τη δομή αντικειμενοστρεφών συστημάτων

Συμβατότητα: ισοδυναμία και υποτύποι

Ο ελεγκτής τύπων για μια γλώσσα με στατικούς τύπους πρέπει να βεβαιώνει ότι ο τύπος κάθε έκφρασης συμφωνεί με τον τύπο που περιμένει το περιβάλλον στο οποίο αυτή εμφανίζεται. Για παράδειγμα, σε μια εντολή ανάθεσης της μορφής x := e, ο τύπος που συνάγεται για την έκφραση e πρέπει να συμφωνεί με τον τύπο που δηλώθηκε ή βρέθηκε αυτόματα για τη μεταβλητή x. Αυτή η συνέπεια ονομάζεται συμβατότητα (compatibility) και διαφέρει ανάμεσα στις γλώσσες προγραμματισμού.

Αν ο τύπος της e και ο τύπος της x είναι ο ίδιος και επιτρέπεται η ανάθεση για αυτόν, τότε πρόκειται για έγκυρη έκφραση. Σε απλά συστήματα τύπων, η ερώτηση αν δύο τύποι είναι συμβατοί ανάγεται στον αν είναι ίσοι ή ισοδύναμοι. Άλλες γλώσσες όμως έχουν άλλα κριτήρια για το πότε δύο εκφράσεις θεωρείται ότι σημαίνουν τιμές του ίδιου τύπου. Αυτές οι θεωρίες ισοδυναμίας (equational theories) γενικά διαφέρουν, με δύο ακραίες περιπτώσεις να είναι τα δομικά συστήματα τύπων (structural type systems), στα οποία δύο τύποι είναι ισοδύναμοι όταν περιγράφουν τιμές με την ίδια δομή, και τα ονομαστικά συστήματα τύπων (nominative type systems), στα οποία δύο συντακτικά ξεχωριστοί τύποι ποτέ δε σημαίνουν τον ίδιο τύπο (δηλαδή δύο τύποι πρέπει να έχουν το ίδιο "όνομα" για να είναι ίσοι).

Σε γλώσσες με υποτύπους (subtyping), η σχέση συμβατότητας είναι πιο πολύπλοκη. Ειδικότερα, αν ο A είναι υποτύπος του B, τότε μια τιμή τύπου A μπορεί να χρησιμοποιηθεί σε ένα περιβάλλον που απαιτείται μια τιμή τύπου B, ακόμα και αν το ανάποδο δεν ισχύει. Όπως στην ισοδυναμία, η σχέση υποτύπου ορίζεται διαφορετικά για κάθε γλώσσα προγραμματισμού, με πολλές δυνατές παραλλαγές. Η παρουσία παραμετρικού και περιστασιακού (ad hoc) πολυμορφισμού σε μια γλώσσα μπορεί επίσης να έχει επιπτώσεις στη συμβατότητα τύπων.

Προγραμματιστικό στυλ

Κάποιοι προγραμματιστές προτιμούν τις γλώσσες με στατικούς τύπους ενώ άλλοι αυτές με δυναμικούς τύπους. Οι γλώσσες με στατικούς τύπους ειδοποιούν τον προγραμματιστή για σφάλματα τύπων κατά τη μεταγλώττιση ενώ μπορεί να είναι και πιο γρήγορες στο χρόνο εκτέλεσης. Οι υποστηρικτές των γλωσσών με δυναμικούς τύπους υποστηρίζουν ότι είναι καλύτερες στη γρήγορη ανάπτυξη πρωτότυπου λογισμικού (rapid prototyping) και ότι τα σφάλματα τύπων είναι μόνο ένα υποσύνολο των σφαλμάτων ενός προγράμματος. Επίσης, συνήθως δεν είναι αναγκαίο να ορίζονται ρητά όλοι οι τύποι σε μια γλώσσα που υποστηρίζει εξαγωγή τύπων ενώ πολλές γλώσσες με δυναμικούς τύπους έχουν βελτιστοποιήσεις στο χρόνο εκτέλεσης που μπορούν να παράγουν γρήγορο κώδικα με ταχύτητα που να πλησιάζει αυτήν των μεταγλωττιστών για στατικές γλώσσες, συχνά χρησιμοποιώντας μερική εξαγωγή τύπων (partial type inference).

Δείτε επίσης

• Θεωρία τύπων
• Υπερφόρτωση τελεστή (operator overloading)
• Γλώσσα προγραμματισμού

Περαιτέρω διάβασμα

• What To Know Before Debating Type Systems (Αγγλικά)
• Laurence Tratt, Dynamically Typed Languages, Advances in Computers, vol. 77, pages 149-184, July 2009 (Αγγλικά)