Πολυμορφισμός υποτύπων

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

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

Οι συναρτησιακές γλώσσες προγραμματισμού συχνά επιτρέπουν τη λειτουργία υποτύπων σε εγγραφές. Κατά συνέπεια, ο λ-λογισμός με απλό σύστημα τύπων επεκτεταμένος με τύπους εγγραφών είναι ίσως το πιο απλό θεωρητικό πλαίσιο στο οποίο μπορεί να οριστεί και να μελετηθεί κάποια χρήσιμη έννοια υποτύπου. Επειδή ο προκύπτων λογισμός επιτρέπει όρους που έχουν περισσότερους από έναν τύπο, δεν είναι πλέον μία "απλή" θεωρία τύπων. Δεδομένου ότι οι συναρτησιακές γλώσσες προγραμματισμού εξ' ορισμού υποστηρίζουν ανώνυμες συναρτήσεις, που μπορούν επίσης να αποθηκεύονται σε εγγραφές, οι εγγραφές εφοδιασμένες με τη λειτουργία υποτύπου παρέχουν ορισμένα από τα χαρακτηριστικά του αντικειμενοστρεφούς προγραμματισμού (εκτός αν προστεθούν στη γλώσσα αναφορές, αυτά τα "αντικείμενα" είναι αμετάβλητα). Συνήθως, οι συναρτησιακές γλώσσες προγραμματισμού παρέχουν επίσης κάποια, συνήθως περιορισμένη, μορφή παραμετρικού πολυμορφισμού. Σε ένα θεωρητικό πλαίσιο, είναι σκόπιμο να μελετήσει κανείς την αλληλεπίδραση των δύο χαρακτηριστικών. Ένα κοινό θεωρητικό πλαίσιο είναι το σύστημα F_<:. Διάφοροι λογισμοί που επιχειρούν να συλλάβουν τις θεωρητικές ιδιότητες του αντικειμενοστρεφούς προγραμματισμού μπορεί να προκύψουν από το σύστημα F_<:.

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

Προέλευση

Η έννοια των υποτύπων στις γλώσσες προγραμματισμού χρονολογείται από τη δεκαετία του 1960. Εισήχθη στη Simula και τους απογόνους της. Οι πρώτες τυπικές αναλύσεις των υποτύπων δόθηκαν από τον John C. Reynolds το 1980, ο οποίος χρησιμοποίησε θεωρία κατηγοριών για την τυποποίηση της έμμεσης μετατροπής, και τον Luca Cardelli (1985).

Η έννοια των υποτύπων έχει αποκτήσει μεγαλύτερη αναγνωρισιμότητα (και συνωνυμία με τον πολυμορφισμό σε μερικούς κύκλους) με την ευρύτατη υιοθέτηση του αντικειμενοστρεφούς προγραμματισμού. Στο πλαίσιο αυτό, η αρχή της ασφαλούς υποκατάστασης συχνά ονομάζεται αρχή της υποκατάστασης κατά Liskov, προς τιμή της Barbara Liskov η οποία την έκανε δημοφιλή σε μία εναρκτήρια ομιλία της σε συνέδριο για τον αντικειμενοστρεφή προγραμματισμό το 1987. Επειδή πρέπει να λάβει υπόψη τη μεταβλητότητα των αντικειμένων, η ιδανική έννοια του υποτύπου όπως ορίζεται από τη Liskov και τη Jeannette Wing και ονομάζεται συμπεριφορική σχέση υποτύπου είναι υπερβολικά ισχυρή για να μπορέσει να υλοποιηθεί σε έναν ελεγκτή τύπων. (Δείτε το τμήμα σχετικά με τους τύπους συναρτήσεων για λεπτομέρειες.)

Παραδείγματα

Παράδειγμα υποτύπων: "πουλί" είναι ο υπερτύπος και όλοι οι άλλοι είναι υποτύποι, όπως υποδεικνύεται από το βέλος στη σημειογραφία της UML.

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

Σε ένα πιο πρακτικό παράδειγμα, μια γλώσσα μπορεί να επιτρέπει σε τιμές κινητής υποδιαστολής (Float) να χρησιμοποιούνται όπου αναμένεται ακέραια τιμή (Integer) (Float<:Integer), ή μπορεί να καθορίσει ένα γενικό τύπο αριθμού (Number) ως κοινό υπερτύπο των ακεραίων και των πραγματικών αριθμών. Στη δεύτερη αυτή περίπτωση, έχουμε μόνο Integer <: Number and Float <: Number, αλλά οι τύποι Integer και Float δεν είναι υποτύποι ο ένας του άλλου.

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

function max (x as Number, y as Number) is
  if x < y then
    return y
  else
    return x
end

Αν ακέραιοι και πραγματικοί είναι και οι δύο υπότυποι του Number, και ο τελεστής σύγκρισης με έναν αυθαίρετο αριθμό ορίζεται για τους δύο τύπους, τότε μπορούν να περαστούν στη συνάρτηση τιμές και των δύο τύπων. Ωστόσο, η ίδια η δυνατότητα εφαρμογής ενός τέτοιου τελεστή περιορίζει σε μεγάλο βαθμό τον τύπο Number (για παράδειγμα, ένας ακέραιος δεν μπορεί να συγκριθεί με έναν μιγαδικό αριθμό), και στην πραγματικότητα έχει νόημα μόνο η σύγκριση ακεραίου με ακέραιο και πραγματικού με πραγματικό. Το να ξαναγράψει κανείς αυτή τη συνάρτηση ώστε να δέχεται μόνο 'x' και 'y' του ίδιου τύπου απαιτεί αναδρομικά φραγμένο πολυμορφισμό.

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

Είδη υποτύπων

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

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

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

Τύποι εγγραφών

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

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

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

Η δεύτερη μέθοδος, που ονομάζεται σχέση υποτύπου κατά βάθος, αντικαθιστά τα διάφορα πεδία με κάποιον υποτύπο τους. Δηλαδή, τα πεδία του υποτύπου είναι υποτύποι των πεδίων του υπερτύπου. Δεδομένου ότι κάθε λειτουργία που υποστηρίζεται από ένα πεδίο στον υπερτύπο υποστηρίζεται και για τους υποτύπους του, κάθε λειτουργία εφαρμόσιμη στον υπερτύπο εγγραφής θα υποστηρίζεται και από τον υποτύπο εγγραφής. Η σχέση υποτύπου κατά βάθος έχει νόημα μόνο για αμετάβλητες εγγραφές: για παράδειγμα, μπορείτε να αναθέσετε την τιμή 1,5 στο πεδίο 'x' ενός πραγματικού σημείου (μια εγγραφή με δύο πεδία πραγματικών αριθμών), αλλά δεν μπορείτε να κάνετε το ίδιο στο πεδίο 'x' ενός ακέραιου σημείου (το οποίο, όμως, είναι ένας κατά βάθος υποτύπος του τύπου πραγματικού σημείου), επειδή το 1,5 δεν είναι ακέραιος.

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

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

Τύποι συναρτήσεων

Αν Τ₁ → Τ₂ είναι ένας τύπος συνάρτησης, τότε κάθε τύπος συνάρτησης S₁ → S₂ με την ιδιότητα ότι η T₁ <:S₁ και S₂<:Τ₂ είναι υποτύπος του. Ο τύπος του ορίσματος της S₁ → S₂ λέγεται ότι είναι ανταλλοίωτος επειδή η σχέση υποτύπου αντιστρέφεται για αυτό, ενώ ο τύπος επιστροφής είναι συναλλοίωτος (ανεπίσημα, αυτή η αντιστροφή συμβαίνει επειδή ο πιο εκλεπτυσμένος τύπος συνάρτησης είναι "πιο ελεύθερος" στους τύπους που δέχεται και "πιο συντηρητικός" στον τύπο που επιστρέφει).

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

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

Εξαναγκασμός

Σε συστήματα με εξαναγκαστική μετατροπή τύπων, οι υποτύποι ορίζονται από κρυφές συναρτήσεις μετατροπής τύπου από τον υποτύπο στον υπερτύπο. Για κάθε σχέση υποτύπου (S<:Τ) παρέχεται μια συνάρτηση εξαναγκασμού εξαναγκασμός_S→Τ, και κάθε αντικείμενο s τύπου S θεωρείται ως το αντικείμενο εξαναγκασμός_S→Τ(s) τύπου Τ. Μια συνάρτηση εξαναγκασμού τύπου μπορεί να ορίζεται ως σύνθεση: αν S<:Τ και Τ<:U τότε το s μπορεί να θεωρηθεί ως αντικείμενο του τύπου U μέσω του σύνθετου εξαναγκασμού (εξαναγκασμός_Τ→U ∘ εξαναγκασμός_S→Τ). Ο εξαναγκασμός από έναν τύπο στον εαυτό του εξαναγκασμός_Τ→Τ είναι η ταυτοτική συνάρτηση id_Τ.

Οι συναρτήσεις εξαναγκασμού τύπου για υποτύπους εγγραφών και ενώσεων μπορεί να ορίζονται ανά στοιχείο. Στην περίπτωση εγγραφών που επεκτείνονται κατά πλάτος, ο εξαναγκασμός τύπου απλώς απορρίπτει τα στοιχεία που δεν ορίζονται στον υπερτύπο. Ο εξαναγκασμός τύπου για τύπους συναρτήσεων μπορεί να δοθεί από τον f'(S) = εξαναγκασμός_{S2 →Τ2} (f(μετατροπή_{Τ1 → S1}(t))), αντανακλώντας έτσι την ανταλλοιωτική λειτουργία των ορισμάτων και συναλλοιωτική λειτουργία των τιμών επιστροφής.

Η συνάρτηση εξαναγκασμού είναι μοναδικά ορισμένη για δεδομένο υποτύπο και υπερτύπο. Έτσι, όταν ορίζονται πολλαπλές σχέσεις υποτύπων, πρέπει να είμαστε προσεκτικοί για να εγγυηθούμε ότι όλες οι συναρτήσεις εξαναγκασμού τύπων είναι συνεπείς. Για παράδειγμα, αν ένας ακέραιος όπως 2: int μπορεί να μετατραπεί σε αριθμό κινητής υποδιαστολής (π.χ., 2,0: float), τότε δεν είναι παραδεκτό να μετατρέψουμε το 2,1:float σε 2: int, επειδή ο σύνθετος εξαναγκασμός μετατροπή_{float → float} που δίνεται από τη σύνθεση εξαναγκασμός_{int → float} ∘ εξαναγκασμός_{float → int} θα ήταν διαφορετικός από τον ταυτοτικό εξαναγκασμό id_float.

Τύποι τομής και ένωσης

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

Δείτε επίσης

• Παραμετρικός πολυμορφισμός
• Πολυμορφισμός (επιστήμη υπολογιστών)
• Πολυμορφισμός στον αντικειμενοστρεφή προγραμματισμό για μια πιο ήπια εισαγωγή σε αυτή την έννοια

Αναφορές

Textbooks

• Pierce, Benjamin C. (2002). Types and programming languages. Cambridge, Mass.: MIT Press. ISBN 0262162091. , Κεφάλαιο 15 (subtyping of record types), Ενότητα 19.3 (nominal vs. structural types and subtyping), and Ενότητα 23.2 (varieties of polymorphism).
• Szyperski, Clemens (2002). Component software : beyond object-oriented programming (2nd έκδοση). New York: ACM Press. ISBN 0201745720.  (γενική παρουσίαση στοχευμένη σε χρήστες γλωσσών προγραμματισμού)

Papers

• Reynolds, John C. (1980). «Using category theory to design implicit conversions and generic operators». Semantics-Directed Compiler Generation: 211–258. doi:https://doi.org/10.1007/3-540-10250-7_24.  (που επίσης εμφανίστηκε στο Gunter, Carl A.· Mitchell, John C. (1994). Theoretical aspects of object-oriented programming : types, semantics, and language design. Cambridge, Mass.: MIT Press. ISBN 9780262071550. )
• Cardelli, Luca (1988). «A semantics of multiple inheritance». Information and Computation 76 (2): 138–164. doi:https://doi.org/10.1016/0890-5401(88)90007-7. 

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

• John C. Reynolds, Theories of programming languages, Cambridge University Press, 1998, ISBN 0521594146, chapter 16.
• Martín Abadi, Luca Cardelli, A theory of objects, Springer, 1996, ISBN 0387947752. Section 8.6 contrast the subtyping of records and objects.