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

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

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

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

```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, που τον ονόμασε "Αλγόριθμο W" ("Algorithm W").

Ο αλγόριθμος αυτός προέρχεται από τον αλγόριθμο εξαγωγής για τον λ-λογισμό με τύπους, που αναπτύχθηκε από τους Haskell Curry και Robert Feys το 1958.
Το 1969 ο J. Roger Hindley τον επέκτεινε και απέδειξε ότι ο αλγόριθμος έβρισκε πάντα τον γενικότερο τύπο.
Το 1978 ο Robin Milner, ανεξάρτητα από το Hindley, έδωσε έναν ισοδύναμο αλγόριθμο, τον Αλγόριθμο W.
Το 1982 o Luis Damas απέδειξε τελικά ότι ο αλγόριθμος του 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, ...

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

#### Επίλυση των εξισώσεων
Η επίλυση των εξισώσεων προχωρά μέσω ενοποίησης (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.

## Αναφορές


## Εξωτερικοί σύνδεσμοι
* 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 

Κατηγορία:Θεωρία τύπων
Κατηγορία:Λογική για Υπολογιστές