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

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