Κατασκευαστής τύπων

Στην περιοχή της μαθηματικής λογικής και της επιστήμης των υπολογιστών γνωστής ως θεωρία τύπων, ένας κατασκευαστής τύπων είναι ένα χαρακτηριστικό μιας τυπικής γλώσσας με τύπους, το οποίο δημιουργεί νέους τύπους από παλιούς. Οι τυπικοί κατασκευαστές τύπων που συναντώνται είναι οι τύποι γινομένου, οι τύποι συναρτήσεων, οι power types και οι τύποι λίστας. Οι βασικοί τύποι θεωρούνται κατασκευαστές τύπων τάξης μηδέν. Νέοι τύποι μπορούν να οριστούν συνθέτοντας αναδρομικά κατασκευαστές τύπων

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

Αφηρημένα, ένας κατασκευαστής τύπου είναι ένα τελεστής τύπων τάξης n που δέχεται ως όρισμα μηδέν ή περισσότερους τύπους, και επιστρέφει έναν άλλον τύπο. Χρησιμοποιώντας το currying, οι τελεστές τύπων τάξης n μπορούν να (ξανα)γραφούν ως μια ακολουθία εφαρμογών μοναδιαίων τελεστών τύπων. Ως εκ τούτου, μπορούμε να δούμε τους τελεστές τύπων ως λ-λογισμός με απλούς τύπους, ο οποίος έχει μόνο έναν βασικό τύπο που συνήθως συμβολίζεται με *,και προφέρεται "τύπος", ο οποίος είναι ο τύπος όλων των τύπων στην γλώσσα, οι όποίοι ονομάζονται σωστοί τύποι για να τους διακρίνουμε από τους τύπους των τύπων των τελεστών τύπων στον δικό τους λογισμό, που ονομάζονται kinds.

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

Δείτε επίσης

• Αλγεβρικός τύπος δεδομένων

Παραπομπές

• Pierce, Benjamin (2002). Types and Programming Languages. MIT Press. ISBN 0-262-16209-1. , chapter 29, "Type Operators and Kinding"
• P.T. Johnstone, Sketches of an Elephant, p. 940