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

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

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

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

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

Συστήματα του λάμδα κύβου

Ο Henk Barendregt επινόησε τον λάμδα κύβο σαν ένα μέσο κατηγοριοποίησης των συστημάτων τύπων πάνω σε 3 άξονες. Κάθε μία από τις 8 κορυφές του παραγόμενου διαγράμματος κυβικού σχήματος αντιστοιχεί σε ένα σύστημα τύπων με τον λ-λογισμό με τύπους και τον λογισμό των κατασκευών στην λιγότερο και περισσότερο εκφραστική κορυφή του κύβου αντίστοιχα. Οι τρεις άξονες του κύβου αντιστοιχούν σε τρεις διαφορετικές επεκτάσεις του λ-λογισμού με απλούς τύπους: την προσθήκη εξαρτώμενων τύπων, την προσθήκη πολυμορφισμού και την προσθήκη κατασκευαστών τύπων υψηλότερης τάξης (π.χ. συναρτήσεις από τύπους σε τύπους). Ο λάμδα κύβος γενικεύεται περαιτέρω από τα αμιγή συστήματα τύπων,

Θεωρία εξαρτώμενων τύπων πρώτης τάξης

Το σύστημα $\lambda \Pi$ των αγνών εξαρτώμενων τύπων πρώτης τάξεως, που αντιστοιχεί στο [LF]], παράγεται από την γενίκευση του τύπου του χώρου συναρτήσεων του λ-λογισμού με απλούς τύπου στον τύπο του εξαρτημένου γινομένου????

Η έκφραση $\Pi n:{\mathbb {N} }.{\mbox{Vec}}({\mathbb {R} },n)$, όπου γράφουμε ${\mbox{Vec}}({\mathbb {R} },n)$ για τις ν-άδες πραγματικών αριθμών, αποτελεί την τύπο των συναρτήσεων οι οποίες δεδομένου ενός φυσικού αριθμού n επιστρέφουν μια ν-άδα από πραγματικούς αριθμούς. Ο συνήθης χώρος συναρτήσεων προκύπτει σαν μια ειδική περίπτωση όταν το πεδίο τιμών δεν εξαρτάται από την είσοδο, π.χ. ο τύπος $\Pi n:{\mathbb {N} }.{\mathbb {R} }$ είναι ο τύπος των συναρτήσεων από φυσικούς αριθμούς σε πραγματικούς αριθμούς, γραμμένος σαν ${\mathbb {N} }\to {\mathbb {R} }$ στον λ-λογισμό με απλούς τύπους.

Θεωρία εξαρτώμενων τύπων δευτέρας τάξης

Το σύστημα $\lambda \Pi 2$ των εξαρτώμενων τύπων δευτέρας τάξης παράγεται από το $\lambda \Pi$ επιτρέποντας ποσοδείκτες πάνω στους κατασκευαστές τύπων. Σε αυτή τη θεωρία, ο τελεστής εξαρτώμενου γινομένου εμπεριέχει τόσο τον τελεστή $\to$ από τον λ-λογισμό με απλούς τύπους όσο και τον ποσοδείκτη $\forall$ του συστήματος F.

Πολυμορφικός λ-λογισμός με εξαρτώμενους τύπους υψηλής τάξης

Το υψηλής τάξης σύστμα $\lambda \Pi \omega$ επεκτείνει το $\lambda \Pi 2$ σε όλες τις δυνατές κατευθύνσεις του λάμδα κύβου: συναρτήσεις από όρους σε όρους, τύπους σε τύπους, τύπους σε όρους και όρους σε τύπους. Το σύστημα αυτό αντιστοιχεί στον λογισμό των κατασκευών, από τον οποίο παράγεται ο λογισμός των επαγωγικών κατασκευών που αποτελεί το σύστημα πίσω από τον βοηθό αποδείξεων Coq.

Αντικειμενοστραφής προγραμματισμός

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

Δείτε επίσης

• λ-λογισμός με τύπους

Επιπλέον διάβασμα

• Barendregt, Henk (1992). «Lambda calculi with types». Στο: S. Abramsky, D. Gabbay and T. Maibaum. Handbook of Logic in Computer Science. Oxford Science Publications. 
• McBride, Conor; McKinna, James (January 2004). «The view from the left». Journal of Functional Programming 14 (1): 69–111. http://strictlypositive.org/view.ps.gz. 
• Altenkirch, Thorsten; McBride, Conor; McKinna, James (April 2005). Why dependent types matter. http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf. 
• Norell, Ulf. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Goteborg, Sweden, September 2007.
• Oury, Nicolas and Swierstra, Wouter (2008). "The Power of Pi" Αρχειοθετήθηκε 2015-10-02 στο Wayback Machine.. Accepted for presentation at ICFP, 2008.
• Norell, Ulf (2008). Dependently Typed Programming in Agda.

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

• Dependently Typed Programming 2008 (Αγγλικά)
• Dependently Typed Programming 2010 (Αγγλικά)
• Dependently Typed Programming 2011 (Αγγλικά)
• "Dependent type" at the Haskell Wiki (Αγγλικά)