Recherche…


Utilisation de base

Lorsque l'extension GADTs est activée, outre les déclarations de données régulières, vous pouvez également déclarer les types de données algébriques généralisés comme suit:

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

Une déclaration GADT répertorie les types de tous les constructeurs d'un type de données, explicitement. Contrairement aux déclarations de type de données habituelles, le type de constructeur peut être toute fonction N-aire (y compris la fonction null) qui aboutit au type de données appliqué à certains arguments.

Dans ce cas, nous avons déclaré que le type DataType a trois constructeurs: Constr1 , Constr2 et Constr3 .

Le constructeur Constr1 n'est pas différent de celui déclaré en utilisant une déclaration de données régulière: data DataType a = Constr1 Int a (Foo a) | ...

Constr2 exige cependant que d' a a une instance de Show , et ainsi lors de l' utilisation du constructeur l'instance aurait besoin d'exister. D'un autre côté, lors de la mise en correspondance d'un motif, le fait que a soit une instance de Show entre dans le champ d'application, vous pouvez donc écrire:

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

Notez que l' Show a contrainte n'apparaît pas dans le type de la fonction et n'est visible que dans le code situé à droite de -> .

Constr3 a le type DataType Int , ce qui signifie que chaque fois qu'une valeur de type DataType a est une Constr3 , il est connu que a ~ Int . Cette information peut également être récupérée avec une correspondance de modèle.



Modified text is an extract of the original Stack Overflow Documentation
Sous licence CC BY-SA 3.0
Non affilié à Stack Overflow