Evaluation d'un AST (comme GADT) avec des flèches comme valeurs atomiques

Le programme suivant de type-chèques et compile:Evaluation d'un AST (comme GADT) avec des flèches comme valeurs atomiques

import Control.Arrow 

data Ns = Na | Nb | Nc | Nd deriving Show 

data Net a where 
    Uni :: a -> Net a 
    Serial :: Net a -> Net a -> Net a 
    Branch :: Show a => Net a -> Net (Net a, Net a) 

deriving instance Show a => Show (Net a) 

eval :: (Arrow a) => Net c -> a b (Net c) 
eval (Uni m) = arr (const (Uni m)) 
eval (Serial m n) = eval m >>> eval n 
--eval (Branch m) = eval m &&& eval m 

example = Serial (Serial (Uni Na) (Uni Nb)) (Serial (Uni Nc) (Uni Nd)) 

main = do 
    putStrLn $ show (app (eval example, Na))

Cependant, lorsque je tente d'ajouter un cas pour eval (Branch m), vérification de type bombes sur. Quelque chose de type

Arrow a => a b (Net d)

est prévu, mais bien sûr, la façon dont je l'ai est

Arrow a => a b (c',c'')

Quelqu'un at-il une suggestion pour savoir comment écrire eval (Branch m)?

EDIT Je

En réponse à @sabauma commentaires, je pense que la signature de type pour eval devra changer, mais je ne suis pas sûr de ce qu'il devrait être.

EDIT II

Voici un exemple de ce qui devrait se produire:

branch = Branch example 
app (eval branch, Na)

devrait donner,

Uni (Uni Na,Uni Na)

C'est ce que la proposition de @sabauma fait.

Source

2013-03-13 lafras

Etes-vous sûr que le type de code affiché est vérifié? Même avec le dernier cas commenté, je reçois toujours une erreur de type impliquant la signature que vous mettez sur 'eval'. GHC déduit le type 'eval :: Flèche a => Net a -> a (Net a) (Net a)'. – sabauma

@sabauma J'ai corrigé la déclaration de type pour 'eval'. Au moins, je l'ai changé comme je l'avais avant d'essayer d'ajouter 'eval (Branch m)' – lafras

Vous devriez certainement ajouter quelques exemples avec des sorties attendues, ou des explications supplémentaires sur la sémantique.Il est très difficile de deviner ce que 'eval' devrait faire exactement, étant donné les informations que vous avez fournies. – phg

Une possibilité est

eval :: (Arrow a) => Net c -> a b (Net c) 
eval (Uni m)  = arr (const (Uni m)) 
eval (Serial m n) = eval m >>> eval n 
eval (Branch m) = (eval m &&& eval m) >>> arr Uni

Je ne sais pas si cela a le comportement souhaité, mais il typable et n'est pas la solution triviale. Cela vous permet de partir sans changer la signature du type.

Source

2013-03-13 14:39:35 sabauma

Cela semble juste. 'eval (Branch (Uni Na))' me donne ce que j'attends, c'est-à-dire 'Uni (Uni Na, Uni Na)'. Je dois juste réfléchir à la sémantique pour un peu. – lafras

Bien que je ne suis pas tout à fait sûr de l'objectif de votre code, et cela pourrait ne pas être ce que vous êtes après, les typable suivants:

eval :: Arrow a => Net c -> a b (Net c) 
eval (Uni m)  = arr (const (Uni m)) 
eval (Serial m n) = eval m >>> eval n 
eval (Branch m) = arr (const (Branch m))

bien sûr, arr . const, ouvrages trivialement pour eval, mais maintenant je suis presque sûr que ce n'est pas ce que tu voulais.

Source

2013-03-13 14:18:43 cdk

Je pense serait de redifine Branch de prendre deux arguments (puisque ramification implique en quelque sorte pour moi):

data Net a where 
    Uni :: a -> Net a 
    Serial :: Net a -> Net a -> Net a 
    Branch :: Show a => Net a -> Net a -> Net (Net a, Net a)

conduisant à

eval :: (Arrow a) => Net c -> a b (Net c) 
eval (Uni m) = arr (const $ Uni m) 
eval (Serial m n) = eval m >>> eval n 
eval (Branch l r) = (eval l) &&& (eval r) >>> arr (uncurry Branch)

Mais je ne peux pas dire si ce changement a du sens pour vous. Vous devriez probablement expliquer comment votre type serait utilisé.

Source

2013-03-13 14:51:52 phg

Evaluation d'un AST (comme GADT) avec des flèches comme valeurs atomiques

Répondre

Questions connexes