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

Στον συναρτησιακό προγραμματισμό, ένας γενικευμένος αλγεβρικός τύπος δεδομένων (επίσης γνωστός ως 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.

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

Εφαρμογές

• Augustsson, Lennart; Petersson, Kent (September 1994). Silly type families. http://web.cecs.pdx.edu/~sheard/papers/silly.pdf. 
• Cheney, James; Hinze, Ralf (2003). «First-Class Phantom Types». Technical Report CUCIS TR2003-1901 (Cornell University). Πρότυπο:Hdl. 
• Xi, Hongwei; Chen, Chiyan; Chen, Gang (2003). «Guarded Recursive Datatype Constructors». Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'03) (ACM Press): 224–235. doi:10.1145/604131.604150. 
• Sheard, Tim; Pasalic, Emir (2004). «Meta-programming with built-in type equality». Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-languages (LFM'04), Cork. doi:10.1016/j.entcs.2007.11.012. 

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.

Επανακατασκευή τύπων

• Peyton Jones, Simon; Washburn, Geoffrey; Weirich, Stephanie (2004). «Wobbly types: type inference for generalised algebraic data types». Technical Report MS-CIS-05-25 (University of Pennsylvania). http://research.microsoft.com/en-us/um/people/simonpj/papers/gadt/MS-CIS-05-26.pdf. 
• Peyton Jones, Simon; Vytiniotis, Dimitrios; Weirich, Stephanie; Washburn, Geoffrey (2006). «Simple Unification-based Type Inference for GADTs». Proceedings of the ACM International Conference on Functional Programming (ICFP'06), Portland. http://research.microsoft.com/en-us/um/people/simonpj/papers/gadt/gadt-rigid-contexts.pdf. 
• Sulzmann, Martin; Wazny, Jeremy; Stuckey, Peter J. (2006). «A Framework for Extended Algebraic Data Types». Στο: Hagiya, M.; Wadler, P., επιμ. 8th International Symposium on Functional and Logic Programming (FLOPS 2006). Lecture Notes in Computer Science. 3945, pp. 46–64. 
• Schrijvers, Tom; Peyton Jones, Simon; Sulzmann, Martin; Vytiniotis, Dimitrios (2009). «Complete and Decidable Type Inference for GADTs». Proceedings of the ACM International Conference on Functional Programming (ICFP'09), Edinburgh. http://research.microsoft.com/en-us/um/people/simonpj/papers/gadt/implication_constraints.pdf. 
• Lin, Chuan-kai (2010). Practical Type Inference for the GADT Type System (PDF) (Διδακτορική διατριβή). Portland State University. Αρχειοθετήθηκε από το πρωτότυπο (PDF) στις 11 Ιουνίου 2016. Ανακτήθηκε στις 17 Ιουλίου 2012. 

Άλλα

• 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.

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

• Generalised Algebraic Datatype Page on the Haskell wiki (Αγγλικά)
• Generalised Algebraic Data Types in the GHC Users' Guide (Αγγλικά)
• Generalized Algebraic Data Types and Object-Oriented Programming (Αγγλικά)
• GADTs – Haskell Prime – Trac (Αγγλικά)
• Papers about type inference for GADTs, bibliography by Simon Peyton Jones (Αγγλικά)
• Type inference with constraints, bibliography by Simon Peyton Jones (Αγγλικά)