Haskell Language
Tipi di dati algebrici generalizzati

Uso di base

Quando l'estensione GADTs è abilitata, oltre alle normali dichiarazioni di dati, puoi anche dichiarare i tipi di dati algebrici generalizzati come segue:

data DataType a where
    Constr1 :: Int -> a -> Foo a -> DataType a
    Constr2 :: Show a => a -> DataType a
    Constr3 :: DataType Int

Una dichiarazione GADT elenca i tipi di tutti i costruttori che un tipo di dati ha, esplicitamente. A differenza delle normali dichiarazioni dei tipi di dati, il tipo di un costruttore può essere qualsiasi funzione N-ari (incluso null) che alla fine si traduce nel tipo di dati applicato ad alcuni argomenti.

In questo caso abbiamo dichiarato che il tipo DataType ha tre costruttori: Constr1 , Constr2 e Constr3 .

Il costruttore Constr1 non è diverso da quello dichiarato utilizzando una dichiarazione dati regolare: data DataType a = Constr1 Int a (Foo a) | ...

Tuttavia, Constr2 richiede che a abbia un'istanza di Show , e quindi quando si usa il costruttore l'istanza dovrebbe esistere. D'altra parte, quando il pattern-matching su di esso, il fatto che a è un'istanza di Show entra in ambito, così puoi scrivere:

foo :: DataType a -> String
foo val = case val of
    Constr2 x -> show x
    ...

Nota che Show a vincolo non appare nel tipo di funzione, ed è visibile solo nel codice a destra di -> .

Constr3 ha tipo DataType Int , il che significa che ogni volta che un valore di tipo DataType a è un Constr3 , è noto che a ~ Int . Anche questa informazione può essere recuperata con una corrispondenza di modello.