Εξαγωγή τύπων

Ο όρος εξαγωγή τύπων ή συμπερασμός τύπων (type inference) αναφέρεται στην αυτόματη συνεπαγωγή του τύπου μιας τιμής σε μια γλώσσα προγραμματισμού. Σαν χαρακτηριστικό συναντάται σε κάποιες γλώσσες με ισχυρό στατικό σύστημα τύπων. Συχνά χρησιμοποιείται σε γλώσσες συναρτησιακού προγραμματισμού αλλά δεν περιορίζεται σε αυτές. Κάποιες γλώσσες που έχουν εξαγωγή τύπων είναι η Visual Basic (από την έκδοση 9.0), η C# (από την έκδοση 3.0), η Clean, η Haskell, η ML, η OCaml και η Scala. Επίσης πρόκειται να υποστηρίζεται από την C++0x και την Perl 6. Η ικανότητα αυτόματης εξαγωγής τύπων διευκολύνει πολλές προγραμματιστικές διεργασίες, επιτρέποντας στον προγραμματιστή να παραλείπει τον τύπο μιας έκφρασης, χωρίς να εμποδίζει τον έλεγχο των τύπων (type checking).

Γενική περιγραφή

Στις περισσότερες γλώσσες προγραμματισμού όλες οι τιμές έχουν έναν τύπο, ο οποίος περιγράφει το είδος των δεδομένων που απεικονίζει η τιμή. Στις γλώσσες με δυναμικούς τύπους ο τύπος μιας έκφρασης είναι γνωστός μόνο κατά το χρόνο εκτέλεσης. Στις γλώσσες με στατικούς τύπους ο τύπος μιας έκφρασης είναι γνωστός στο χρόνο μεταγλώττισης. Στις γλώσσες με στατικούς τύπους οι τύποι εισόδου και εξόδου των συναρτήσεων και οι τοπικές μεταβλητές συνήθως πρέπει να συνοδεύονται από σημειώσεις τύπων (type annotations). Για παράδειγμα, στη C:

int addone(int x) {
    int result; /* δηλώνει αποτέλεσμα ακέραιο (της C) */

    result = x+1;
    return result;
}

Στην αρχή αυτού του ορισμού συνάρτησης, η int addone(int x) δηλώνει ότι η addone είναι μια συνάρτηση που παίρνει ένα όρισμα, που είναι ακέραιος, και επιστρέφει ακέραιο. Η int result; δηλώνει ότι η τοπική μεταβλητή result είναι ακέραιος. Σε μια υποτιθέμενη γλώσσα με εξαγωγή τύπων, ο κώδικας θα μπορούσε να γραφτεί ως εξής:

addone(x) {
    val result;  /* ο τύπος του result θα εξαχθεί */
    val result2; /* ο τύπος του result #2 θα εξαχθεί */

    result = x+1;
    result2 = x+1.0;  /* δεν είναι αποδεκτό (στην υποτιθέμενη γλώσσα) */
    return result;
}

Τα παραπάνω μοιάζουν με κώδικα γραμμένο σε κάποια γλώσσα με δυναμικούς τύπους, αλλά με κάποιους επιπλέον περιορισμούς (που θα αναφερθούν στη συνέχεια) είναι δυνατό να εξαχθούν (infer) οι τύποι όλων των μεταβλητών στο χρόνο μεταγλώττισης. Στο παραπάνω παράδειγμα, ο μεταγλωττιστής θα κατέληγε ότι η result και η x έχουν τύπο ακέραιο και η addone είναι συνάρτηση int -> int. Η μεταβλητή result2 δε χρησιμοποιείται σωστά, επομένως δε θα είχε κάποιο τύπο.

Ο μεταγλωττιστής θα υπέθετε, αν δεν υπήρχε αντίθετη πληροφορία, ότι ο τελεστής + δέχεται δύο ακεραίους και επιστρέφει έναν ακέραιο (κάτι που ισχύει για παράδειγμα στην OCaml). Από αυτό, ο εξαγωγέας τύπων μπορεί να εξάγει ότι ο τύπος της x+1 είναι ακέραιος, που σημαίνει ότι η result είναι ακέραιος και επομένως η τιμή επιστροφής της addone είναι ακέραιος. Όμοια, επειδή ο + απαιτεί και τα δύο ορίσματά του να έχουν τον ίδιο τύπο, η x πρέπει να είναι ακέραιος και επομένως η addone δέχεται σαν όρισμα έναν ακέραιο.

Στην επόμενη γραμμή όμως, η result2 υπολογίζεται προσθέτοντας τον δεκαδικό "1.0" (αριθμητική κινητής υποδιαστολής), προκαλώντας σύγκρουση με τη χρήση της x για ακέραιες εκφράσεις και εκφράσεις κινητής υποδιαστολής ταυτόχρονα. Μια τέτοια κατάσταση θα προκαλέσει ένα σφάλμα χρόνου μεταγλώττισης. Σε μια διαφορετική γλώσσα, η result2 θα μπορούσε να έχει έμμεσα δηλωθεί σαν μεταβλητή κινητής υποδιαστολής και η πρόσθεση θα μετέτρεπε έμμεσα τη x σε αριθμό κινητής υποδιαστολής. Συνήθως οι γλώσσες που υποστηρίζουν εξαγωγή τύπων στο βαθμό του παραπάνω παραδείγματος, δεν υποστηρίζουν τέτοιες έμμεσες μετατροπές τύπων. Σε αυτό το σημείο φαίνεται η διαφορά μεταξύ εξαγωγής τύπων, που δεν περιλαμβάνει μετατροπή τύπων, και έμμεσης μετατροπής τύπων (implicit type conversion), που άμεσα μετατρέπει τα δεδομένα σε έναν άλλο τύπο δεδομένων, συχνά χωρίς περιορισμούς.

Τυπική περιγραφή

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

Ο μεταγλωττιστής συλλέγει την απαραίτητη πληροφορία για την εξαγωγή ενός τύπου μιας έκφρασης, είτε σαν σύνολο (που έχει αναχθεί) από τις σημειώσεις τύπων των υποεκφράσεών της, είτε μέσω μιας έμμεσης συλλογιστικής των τύπων των διάφορων ατομικών τιμών (π.χ. true : Bool, 42 : Integer, 3.14159 : Real, κλπ.). Ένας μεταγλωττιστής μπορεί, μέσω αυτής της αναγωγής από τις τιμές στις εκφράσεις, να μεταγλωττίσει πλήρως ένα πρόγραμμα χωρίς σημειώσεις τύπων. Σε πολύπλοκες περιπτώσεις προγραμματισμού υψηλής τάξης και πολυμορφισμού, δεν είναι πάντα δυνατό ο μεταγλωττιστής να εξάγει όλη την απαραίτητη πληροφορία και ίσως χρειάζονται σημειώσεις τύπων σε σημεία του προγράμματος για να αποφεύγονται διφορούμενες καταστάσεις.

Παράδειγμα

Για παράδειγμα, έστω η συνάρτηση map της Haskell, που εφαρμόζει μια συνάρτηση σε κάθε στοιχείο μιας λίστας και μπορεί να οριστεί ως εξής:

map f [] = []
map f (first:rest) = f first : map f rest

Φαίνεται ότι η συνάρτηση map παίρνει μια λίστα σαν δεύτερο όρισμα, το πρώτο όρισμα f είναι συνάρτηση που μπορεί να εφαρμοστεί στον τύπο των στοιχείων της λίστας αυτής, και το αποτέλεσμα της map κατασκευάζεται σαν λίστα με στοιχεία που είναι αποτελέσματα της f. Υποθέτοντας τότε ότι μια λίστα περιέχει στοιχεία του ίδιου τύπου, μπορεί να κατασκευαστεί μια υπογραφή τύπου (type signature):

map :: (a -> b) -> [a] -> [b]

όπου η σύνταξη "a -> b" σημαίνει συνάρτηση που δέχεται κάτι τύπου a σαν παράμετρο και παράγει b. Η "a -> b -> c" είναι ισοδύναμη με την "a -> (b -> c)".

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

Αλγόριθμος εξαγωγής τύπων των Hindley–Milner

Ο αλγόριθμος που χρησιμοποιήθηκε αρχικά για την εξαγωγή τύπων αποκαλείται (άτυπα) σήμερα σαν "αλγόριθμος Hindley–Milner", αν και ο αλγόριθμος κανονικά θα έπρεπε να αποδίδεται στον Damas και τον Milner^[1], που τον ονόμασε "Αλγόριθμο W" ("Algorithm W").

Ο αλγόριθμος αυτός προέρχεται από τον αλγόριθμο εξαγωγής για τον λ-λογισμό με τύπους, που αναπτύχθηκε από τους Haskell Curry και Robert Feys το 1958. Το 1969 ο J. Roger Hindley τον επέκτεινε και απέδειξε ότι ο αλγόριθμος έβρισκε πάντα τον γενικότερο τύπο. Το 1978 ο Robin Milner,^[2] ανεξάρτητα από το Hindley, έδωσε έναν ισοδύναμο αλγόριθμο, τον Αλγόριθμο W. Το 1982 o Luis Damas^[1] απέδειξε τελικά ότι ο αλγόριθμος του Milner είναι πλήρης και τον επέκτεινε για να υποστηρίζει συστήματα με πολυμορφικές αναφορές (polymorphic references). Ο αλγόριθμος Hindley–Milner που περιγράφεται εδώ υποστηρίζει μια περιορισμένη έκδοση του Συστήματος F (System F).

Ο αλγόριθμος

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

Παραγωγή των εξισώσεων

Ο αλγόριθμος που χρησιμοποιείται για την παραγωγή των εξισώσεων μοιάζει με έναν κανονικό ελεγκτή τύπων (type checker), επομένως δίνεται ένας ελεγκτής τύπων για το λ-λογισμό με τύπους:

$e\,::=E\mid v\mid (\lambda v:\tau .e)\mid (e\,e)$

και

$\tau \,::=T\mid \tau \to \tau$

όπου η $E$ είναι μια πρωτογενής έκφραση (όπως η "3") και ο $T$ είναι ένας πρωτογενής τύπος (όπως ο Ακέραιος, "Integer").

Πρέπει να κατασκευαστεί μια συνάρτηση $f$ που να αντιστοιχεί ένα ζεύγος $(\epsilon ,t)$ , όπου το $\epsilon$ είναι περιβάλλον τύπων και ο $t$ είναι όρος, σε κάποιον τύπο $\tau$ . Θεωρείται ότι αυτή η συνάρτηση είναι ήδη ορισμένη για πρωτογενείς τύπους και όρους. Οι άλλες περιπτώσεις είναι:

$f(\epsilon ,v)=\tau$ όπου το $(v,\tau )$ ανήκει στο $\epsilon$
$f(\epsilon ,g\,e)=\tau$ όπου $f(\epsilon ,g)=\tau _{1}\to \tau$ και $f(\epsilon ,e)=\tau _{1}$
$f(\epsilon ,\lambda v:\tau .e)=\tau \to f(\epsilon _{1},e)$ όπου $\epsilon _{1}=\epsilon \cup (v,\tau )$

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

Στη συνέχεια αναπτύσσεται ένας πιο πολύπλοκος αλγόριθμος που μπορεί να χειριστεί μεταβλητές τύπων και περιορισμούς (constraints) σε αυτές. Το σύνολο T των πρωτογενών τύπων επεκτείνεται για να περιλαμβάνει ένα άπειρο σύνολο από μεταβλητές, που σημειώνονται με τα πεζά γράμματα $\alpha ,\beta ,...$

Δείτε το ^[3] για περισσότερες λεπτομέρειες.

Επίλυση των εξισώσεων

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

Η ενοποίηση του κενού συνόλου εξισώσεων είναι εύκολη: $u\,\emptyset =\mathbf {i}$ , όπου η $\mathbf {i}$ είναι η ταυτοτική αντικατάσταση.

Η ενοποίηση μιας μεταβλητής με έναν τύπο γίνεται ως εξής: $u\,([\alpha =T]\cup C)=u\,(C')\cdot (\alpha \mapsto T)$ , όπου ο $\cdot$ είναι ο τελεστής σύνθεσης αντικαταστάσεων και το $C'$ είναι το σύνολο των περιορισμών $C$ που παραμένουν, στο οποίο έχει εφαρμοστεί η νέα αντικατάσταση $\alpha \mapsto T$ .

Φυσικά, $u\,([T=\alpha ]\cup C)=u([\alpha =T]\cup C)$ .

Η πιο ενδιαφέρουσα περίπτωση είναι και αυτή που μένει $u\,([S\to S'=T\to T']\cup C)=u\,(\{[S=T],[S'=T']\}\cup C)$ .

Ένα απλό παράδειγμα είναι το a[i] = b[i] (έστω σε σύνταξη όπως της C). Αρχικά ο αλγόριθμος Hindley–Milner θα έβρισκε ότι η i πρέπει να είναι ακέραιου τύπου (int), στη συνέχεια ότι η 'a' πρέπει να είναι "πίνακας από $\alpha$ " και η 'b' πρέπει να είναι "πίνακας από $\beta$ ". Στη συνέχεια, επειδή υπάρχει ανάθεση από $\beta$ σε $\alpha$ , η $\alpha$ πρέπει να είναι του ίδιου τύπου με τη $\beta$ (αν δεν υπάρχει έμμεση μετατροπή τύπων). Ισχύει ότι τελικά η $\alpha$ πρέπει να είναι τουλάχιστον υπερτύπος της $\beta$ .

Αναφορές

↑ ^1,0 ^1,1 Damas, Luis; Milner, Robin (1982), «Principal type-schemes for functional programs», POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, σελ. 207–212, http://groups.csail.mit.edu/pag/6.883/readings/p207-damas.pdf
↑ Milner, Robin (1978), «A Theory of Type Polymorphism in Programming», Jcss 17: 348–375
↑ Pierce, Benjamin C. (2002), «Chapter 22», Types and Programming Languages, MIT Press, ISBN 0-262-16209-1

Εξωτερικοί σύνδεσμοι

e-mail του Roger Hindley, σχετικά με την ιστορία της εξαγωγής τύπων (Αγγλικά)
Δημοσίευση του Luca Cardelli, περιγράφει τον αλγόριθμο, περιλαμβάνει υλοποίηση σε Modula-2 (Αγγλικά)
Υλοποίηση της εξαγωγής Hindley-Milner σε Scala, του Andrew Forrest (πρόσβ. 30 Ιουλίου 2009) (Αγγλικά)
What is Hindley-Milner? (and why is it cool?) Εξηγεί τον αλγόριθμο Hindley-Milner, παραδείγματα σε Scala (Αγγλικά)

[Damas-and-Milner-1982-1] 1,0 ^1,1 Damas, Luis; Milner, Robin (1982), «Principal type-schemes for functional programs», POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, σελ. 207–212, http://groups.csail.mit.edu/pag/6.883/readings/p207-damas.pdf

[2] Milner, Robin (1978), «A Theory of Type Polymorphism in Programming», Jcss 17: 348–375

[3] Pierce, Benjamin C. (2002), «Chapter 22», Types and Programming Languages, MIT Press, ISBN 0-262-16209-1

[1]

[2]

[3]