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

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

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

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

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

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

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

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


```haskell
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
```


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


```haskell
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))
```


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


```haskell
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.

## Εξωτερικοί σύνδεσμοι
* 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 

Κατηγορία:Προγραμματισμός
Κατηγορία:Θεωρία τύπων
Κατηγορία:Τύποι δεδομένων