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

Στην επιστήμη των υπολογιστών και την λογική, ένας **εξαρτώμενος τύπος** είναι ένας τύπος που εξαρτάται από μία τιμή. Οι εξαρτώμενοι τύποι διαδραματίζουν κεντρικό ρόλο στην Ιντουισιονιστική θεωρία τύπων και στον σχεδιασμό συναρτησιακών γλωσσών προγραμματισμού σαν την 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.

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

## Δείτε επίσης
*λ-λογισμός με τύπους

## Αναφορές


## Επιπλέον διάβασμα
*
* 
*
* Norell, Ulf. *[http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf 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" . 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 

Κατηγορία:Προγραμματισμός
Κατηγορία:Θεωρία τύπων