Comment est-ce que j'utilise le système de type de Haskell pour appliquer la correction tout en étant capable de faire correspondre le modèle?

Question

Disons que j'ai un HAA représentant une sorte de structure arborescente:

data Tree = ANode (Maybe Tree) (Maybe Tree) AValType 
      | BNode (Maybe Tree) (Maybe Tree) BValType 
      | CNode (Maybe Tree) (Maybe Tree) CValType 

Pour autant que je sais qu'il n'y a aucun moyen de correspondance de modèles contre les constructeurs de type (ou les fonctions correspondantes se serait pas un type?) mais je voudrais toujours utiliser le système de type compile-time pour éliminer la possibilité de retourner ou d'analyser le mauvais 'type' du noeud Tree. Par exemple, il se peut que CNode ne puisse être que des parents d'ANODE. Je pourrais avoir

parseANode :: Parser (Maybe Tree) 

en fonction de l'analyse syntaxique parsec qui s'est utilisé dans le cadre de mon analyseur Nœuds-C:

parseCNode :: Parser (Maybe Tree) 
parseCNode = try (
        string "<CNode>" >> 
        parseANode >>= \maybeanodel -> 
        parseANode >>= \maybeanoder -> 
        parseCValType >>= \cval -> 
        string "</CNode>" 
        return (Just (CNode maybeanodel maybeanoder cval)) 
      ) <|> return Nothing 

Selon le système de type, parseANode pourrait finir par revenir un Maybe Nœuds-C, un bnode Peut-être , ou un ANODE peut-être, mais je veux vraiment m'assurer qu'il ne renvoie qu'un ANODE Peut-être. Notez que ce n'est pas une valeur de schéma de données ou d'exécution - vérifiez ce que je veux faire - Je suis en train d'essayer de vérifier la validité de l'analyseur que j'ai écrit pour un schéma d'arbre particulier. IOW, je n'essaie pas de vérifier les données analysées pour l'exactitude du schéma, ce que j'essaie vraiment de faire est de vérifier mon analyseur pour l'exactitude du schéma - Je voudrais juste m'assurer que je ne bâcle pas parseANode un jour pour renvoyer autre chose qu'une valeur ANode.

J'espérais que peut-être si j'apparié contre le constructeur de valeur dans la variable de liaison, que le type inférences serait comprendre ce que je voulais dire:

parseCNode :: Parser (Maybe Tree) 
parseCNode = try (
        string "<CNode>" >> 
        parseANode >>= \(Maybe (ANode left right avall)) -> 
        parseANode >>= \(Maybe (ANode left right avalr)) -> 
        parseCValType >>= \cval -> 
        string "</CNode>" 
        return (Just (CNode (Maybe (ANode left right avall)) (Maybe (ANode left right avalr)) cval)) 
      ) <|> return Nothing 

Mais cela a beaucoup de problèmes, et non la moins que ce parseANode n'est plus libre de retourner Nothing. Et cela ne fonctionne pas de toute façon - il semble que cette variable de liaison est traitée comme une correspondance de modèle et l'exécution se plaint de la correspondance de modèle non exhaustive lorsque parseANode renvoie Nothing ou Maybe BNode ou quelque chose.

je pouvais faire quelque chose dans ce sens:

data ANode = ANode (Maybe BNode) (Maybe BNode) AValType 
data BNode = BNode (Maybe CNode) (Maybe CNode) BValType 
data CNode = CNode (Maybe ANode) (Maybe ANode) CValType 

mais ce genre de suce, car il suppose que la contrainte est appliquée à tous les nœuds - je ne pourrais pas être intéressé à le faire - il pourrait en effet être juste CNodes qui ne peuvent être que des ANodes parentales. Donc je suppose que je pourrais le faire:

data AnyNode = AnyANode ANode | AnyBNode BNode | AnyCNode CNode 

data ANode = ANode (Maybe AnyNode) (Maybe AnyNode) AValType 
data BNode = BNode (Maybe AnyNode) (Maybe AnyNode) BValType 
data CNode = CNode (Maybe ANode) (Maybe ANode) CValType 

mais cela rend beaucoup plus difficile à motif match contre son * Noeud - en fait, il est impossible parce qu'ils sont juste complètement types distincts. Je pourrais faire une classe de types où je voulais motif match, je suppose que

class Node t where 
    matchingFunc :: t -> Bool 

instance Node ANode where 
    matchingFunc (ANode left right val) = testA val 

instance Node BNode where 
    matchingFunc (BNode left right val) = val == refBVal 

instance Node CNode where 
    matchingFunc (CNode left right val) = doSomethingWithACValAndReturnABool val 

En tout cas, cela semble juste sorte de désordre. Quelqu'un peut-il penser à une façon plus succincte de le faire?

Answer 1

Je ne comprends pas votre objection à votre solution finale. Vous pouvez toujours match de modèle contre AnyNode s, comme ceci:

f (AnyANode (ANode x y z)) = ... 

Il est un peu plus bavard, mais je pense qu'il a les propriétés techniques que vous voulez.

Answer 2

Je voudrais encore utiliser le système de type compilation pour éliminer la possibilité de retourner ou de l'analyse du mauvais « type » du nœud de l'arbre

Cela ressemble à un cas d'utilisation pour GADTs.

{-# LANGUAGE GADTs, EmptyDataDecls #-} 
data ATag 
data BTag 
data CTag 

data Tree t where 
    ANode :: Maybe (Tree t) -> Maybe (Tree t) -> AValType -> Tree ATag 
    BNode :: Maybe (Tree t) -> Maybe (Tree t) -> BValType -> Tree BTag 
    CNode :: Maybe (Tree t) -> Maybe (Tree t) -> CValType -> Tree CTag 

Maintenant, vous pouvez utiliser Tree t lorsque vous ne se soucient pas du type de noeud, ou Tree ATag quand vous faites.

Answer 3

Une extension de la réponse de keegan: encoder les propriétés d'exactitude des arbres rouges/noirs est une sorte d'exemple canonique. Ce fil a le code montrant à la fois la solution de type de données GADT et imbriquée: http://www.reddit.com/r/programming/comments/w1oz/how_are_gadts_useful_in_practical_programming/cw3i9