Γενικευμένος αλγεβρικός τύπος δεδομένων

Στον συναρτησιακό προγραμματισμό, ένας γενικευμένος αλγεβρικός τύπος δεδομένων (επίσης γνωστός ως GADT και πρώτης τάξεως τύπος φάντασμα) είναι μια γενίκευση του αλγεβρικού τύπου της Haskell και της ML, εφαρμοσμένου πάνω σε παραμετρικούς τύπους.

Με αυτή την επέκταση, οι παράμετροι του τύπου επιστροφής ενός κατασκευαστή τύπων μπορούν να επιλεχθούν ελεύθερα όταν δηλώνεται ο κατασκευαστής, ενώ για αλγεβρικούς τύπους στην Haskell 98, η παράμετρος τύπου της τιμής επιστροφή συμπεραίνεται από τους τύπους των παραμέτρων. Οι γενικευμένοι αλγεβρικοί τύποι δεδομένων είναι υλοποιημένοι στον μεταγλωττιστή GHC σαν μια επέκταση, η οποία χρησιμοποιείται, μεταξύ άλλων, από τον Pugs και τον Darcs. Η γλώσσα προγραμματισμού Ωμέγα επεκτείνει τη Haskell με γενικευμένους αλγεβρικούς τύπους δεδομένων.

Μια πρώιμη εκδοχή των γενικευμένων αλγεβρικών τύπων δεδομένων είχε δοθεί από τους Augustsson και Petersson το 1994 και βασιζόταν στο ταίριασμα προτύπων στον ALF.

Οι Sulzmann, Wazny και Stuckey εισήγαγαν τους επεκτεταμένους γενικευμένους τύπους δεδομένων οι οποίοι συνδυάζουν τους γενικευμένους αλγεβρικούς τύπους δεδομένων με τον υπαρξιακό τύπο και τους περιορισμούς τύπων κλάσεων που εισήγαγαν οι Perry, Laufer και Odersky.

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

Εφαρμογές

Επεξεργασία

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

Αφηρημένη σύνταξη υψηλότερης τάξης

Επεξεργασία

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

data Lam :: * -> * where
  Lift :: a                     -> Lam a
  Tup  :: Lam a -> Lam b        -> Lam (a, b)
  Lam  :: (Lam a -> Lam b)      -> Lam (a -> b)
  App  :: Lam (a -> b) -> Lam a -> Lam b
  Fix  :: Lam (a -> a)          -> Lam a

Και μία συνάρτηση υπολογισμού:

eval :: Lam t -> t
eval (Lift v)    = v
eval (Tup e1 e2) = (eval e1, eval e2)
eval (Lam f)     = \x -> eval (f (Lift x))
eval (App e1 e2) = (eval e1) (eval e2)
eval (Fix f)     = (eval f) (eval (Fix f))

Η συνάρτηση παραγοντικού μπορεί πλέον να γραφτεί ως:

fact = Fix (Lam (\f -> Lam (\y -> Lift (if eval y == 0 then 1 else eval y * (eval f) (eval y - 1)))))

Θα είχαμε συναντήσει προβλήματα αν χρησιμοποιούσαμε συνηθισμένους αλγεβρικούς τύπους δεδομένων. Η μη χρήση της παραμέτρου τύπου θα έκανε τους ανελιγμένους βασικούς τύπους υπαρξιακά ποσοτικοποιημένους, καθιστώντας το αδύνατο να γραφτεί η συνάρτηση υπολογισμού. Με κάποια παράμετρο τύπου, θα ήμασταν περιορισμένοι σε έναν μοναδικό βασικό τύπο. Επιπλέον, κακώς ορισμένες εκφράσεις όπως App (Lam (\x -> Lam (\y -> App x y))) (Lift True) θα μπορούσαν να κατασκευαστούν, ενώ εμφανίζουν σφάλμα τύπων με GADTs.

Σημειώσεις

Επεξεργασία


Επιπλέον Υλικό

Επεξεργασία
Εφαρμογές
Semantics
  • Patricia Johann and Neil Ghani (2008). "Foundations for Structured Programming with GADTs".
  • Arie Middelkoop, Atze Dijkstra and S. Doaitse Swierstra (2011). "A lean specification for GADTs: system F with first-class equality proofs". Higher-Order and Symbolic Computation.
Επανακατασκευή τύπων
Άλλα
  • Andrew Kennedy and Claudio V. Russo. "Generalized algebraic data types and object-oriented programming". In Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications. ACM Press, 2005.

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

Επεξεργασία