Ne peut pas détruire le type transitif

Question

Dire que j'ai la GADT suivante:

data Stage a b where 
    Comb :: Stage a b -> Stage b c -> Stage a c 
    FMap :: (a -> b) -> Stage a b 

Je veux maintenant une fonction qui fonctionne comme ceci:

run (a `Comb` b) = (a,b) 
run (FMap f)  = (FMap f,FMap id) 

Comment pourrais-je construire une telle fonction?

J'ai essayé différentes manières de lier les types mais je n'ai pas réussi. Y at-il une extension qui me manque qui permet des liaisons de type plus étendues?

Voici le message d'erreur:

Couldn't match type `t' with `(Stage t1 b, Stage b t2)' 
    `t' is a rigid type variable bound by 
     the inferred type of run :: Stage t1 t2 -> t at <interactive>:11:5 
In the expression: (a, b) 
In an equation for `run': run (a Comb b) = (a, b) 

Une description de ce que je veux accomplir: Je veux concevoir un DSL et une piste de fonction qui peut essayer d'exécuter un code de la LIS dans un couple de différentes manières (j'ai plusieurs fonctions d'exécution différentes pour chaque voie). La fonction d'exécution essaiera d'exécuter autant de code que possible, puis indiquera quel code elle n'a pas pu être exécutée et quel sera le résultat du code qu'elle pourrait exécuter.

Answer 1

Vous aurez besoin d'une signature de type pour run, car vous effectuez une correspondance de modèle sur un GADT. La correspondance de modèle sur GADT nécessite un raffinement de type, et cela ne fonctionne généralement que s'il y a une signature de type.

Mais la signature du type n'est pas claire. Si la valeur d'entrée est

a `Comb` b :: Stage x y 

puis vous revenez (a, b), où

a :: Stage x b 
b :: Stage b y 

pour une b inconnue. C'est un type existentiel qui s'échappe. Vous ne pouvez pas écrire

run :: Stage x y -> (State x b, Stage b y) 

car cela signifierait qu'il faudrait travailler pour tousb, mais il ne fonctionne que pour certains (inconnu) b.

Malheureusement, il n'est pas clair pourquoi vous voulez écrire une fonction comme run. Pourquoi produire une paire? Que voulez-vous faire avec cette paire plus tard? Le constructeur Comb est défini pour combiner deux étapes qui ont un type intermédiaire inconnu, de sorte que cette version de run fonctionnerait:

run :: Stage a b -> Stage a b 
run (a `Comb` b) = a `Comb` b 
run (FMap f)  = FMap f `Comb` FMap id 

Ou vous pouvez définir un type de données plus spécifique ne permettant une « paire » de deux étages avec inconnu type intermédiaire:

data PairStages a b where 
    PairStages :: Stage a b -> Stage b c -> PairStages a c 

Et puis:

run :: Stage a b -> PairStages a b 
run (a `Comb` b) = PairStages a b 
run (FMap f)  = PairStages (FMap f) (FMap id) 

Mais il me semble étrange encore que run renvoie une paire. Comme je l'ai dit, on ne sait pas ce que vous voulez faire avec le résultat de run. Il semblerait plus utile d'avoir une fonction récursive qui combine en quelque sorte les résultats de l'exécution des composants dans le cas Comb.Par exemple, comme ceci:

run :: Stage a b -> (a -> b) 
run (a `Comb` b) = run b . run a 
run (FMap f)  = f