Destructive Update με γραμμικούς τύπους

Abstract

Σκοπός της παρούσας εργασίας είναι η χρήση των γραμμικών τύπων για τον ορισμό και την υλοποίηση μιας γλώσσας που υλοποιεί τις εγγραφές σε πίνακα καταστροφικά με ασφαλή τρόπο. Θέλουμε ο προγραμματιστής να γράφει κώδικα χωρίς επισημειώσεις τύπων με πίνακες χρησιμοποιώντας ένα αγνά συναρτησιακό interface, και ο μεταγλωττιστής, εφόσον είναι ασφαλές, να υλοποιεί τις εγγραφές in-place. Στο πλάισιο της εργασίας ορίστηκε τυπικά, η σύνταξη, το σύστημα τύπων και η λειτουργική σημασιολογία της ενδιάμεσης γλώσσας letdo η οποία βασίζεται σε ένα γραμμικό σύστημα τύπων. Οι γραμμικοί τύποι προσφέρουν την ιδιότητα ότι κάθε πίνακας θα χρησιμοποιηθεί ακριβώς μία φορά. Για να προσαρμόσουμε την γλώσσα στο ζητούμενο συναρτησιακό interface, προσθέτουμε στην γλώσσα το letdo construct που υποστηρίζει πρόσβαση μόνο για ανάγνωση στον πίνακα χωρίς όμως να προσθέτει περιορισμούς στην γλώσσα. Ορίζουμε έναν semantics-preserving μετασχηματισμό που λαμβάνει κώδικα στην αρχική γλώσσα και τον μετασχηματίζει σε κώδικα letdo. Έπειτα, ορίσαμε και υλοποιήσαμε έναν αλγόριθμο συμπερασμού τύπων για την γλώσσα letdo που λειτουργεί παράγωντας και επιλύοντας περιορισμούς σε δύο στάδια. Έχουμε κατασκευάσει έναν μεταγλωττιστή που λαμβάνει κώδικα στην αρχική γλώσσα τον μετασχηματίζει στην γλώσσα letdo και έπειτα γίνεται συμπερασμός των τύπων. Εάν το πρόγραμμα περάσει τον έλεγχο τύπων είναι ασφαλές οι εγγραφές σε πίνακες να γίνουν destructively.