Haskell: Étiquetage un AST avec des informations de type en utilisant l'algorithme W

Question

Nous avons une définition AST:

data Term a 
    = Lam String a 
    | App a a 
    | Var String 
    deriving(Read,Show,Eq,Functor,Foldable,Traversable) 

et une F-algèbre pour l'inférence de type:

type Wrapped m a = Enviroment -> m a 
type Result m = Wrapped (Type,Substitution) 
w :: 
    (MonadState Int, MonadError TypeError) 
    => Term (Result m) 
    -> Result m 
w term env = ... 

Nous pouvons obtenir le résultat de en cours d'exécution en utilisant l'inférence cata:

infer :: 
    (MonadState Int, MonadError TypeError) 
    => Fix Term 
    -> Result m 
infer ast = cata hm ast 

Mais maintenant, je veux que le résultat soit le un AST d'origine nnotated avec des informations de type pour chaque expression, Alors maintenant infer' :: Fix Term -> Wrapped (Labeled Term Type).

1. Quelle est la structure des données dois-je utiliser pour annoter l'arbre (Cofree, Product, Fix avec une coutume Label)?
2. Comment puis-je l'implémenter en utilisant des schémas de récurrence, sans modifier la fonction w d'origine?

Answer 1

Cette réponse ne modifie la fonction w, mais il vise toujours à maintenir les fonctions « bête de somme » effilées de la machinerie récursivité régimes.

Gardons le type Term tel qu'il est, et supposons que nous avons un type E pour l'environnement qui est calculé vers le bas, et un type R pour l'annotation finale qui est calculée à partir des feuilles vers le haut.

Supposons aussi que nous avons ces deux fonctions:

calcEnv :: E -> Term x -> E -- calculates the environment which will be passed downwards 

calcResult :: E -> Term R -> IO R -- effectfully calculates the result flowing upwards 

J'utilise IO comme la monade pour la simplicité.

(Notez que je suppose que « le calcul de l'environnement » ne peut pas avoir des effets. Je ce n'est pas le cas, alors cette solution ne suffira pas.)

Nous travaillons en deux phases. Nous construisons d'abord un arbre dans lequel les nœuds ont été annotés avec leurs environnements. Nous utilisons un anamorphism, au lieu du "truc" de retourner une fonction d'un catamorphisme.

import qualified Control.Comonad.Trans.Cofree as COFREEF 

annotate :: E -> Fix Term -> Cofree Term E 
annotate = curry (ana coalg) 
    where 
    coalg :: (E, Fix Term) -> COFREEF.CofreeF Term E (E, Fix Term) 
    coalg (environment, Fix term) = 
     let environment' = calcEnv environment term 
     in environment COFREEF.:< fmap ((,) environment') term 

(Gardez à l'esprit que type instance Base (Cofree f a) = CofreeF f a. Voilà où le COFREEF.:<comes from. Il est essentiellement une paire d'une valeur pure et une autre valeur enveloppée dans foncteur.)

Et dans la phase suivante que nous consommons effectfully la arbre annotée des feuilles pour produire le résultat final arbre -a avec R annotations:

calculate :: Cofree Term E -> IO (Cofree Term R) 
calculate = cata alg 
    where 
    alg :: COFREEF.CofreeF Term E (IO (Cofree Term R)) -> IO (Cofree Term R) 
    alg (environment COFREEF.:< termio) = do 
     term :: Term (Cofree Term R) <- sequenceA termio 
     result :: R <- calcResult environment (fmap extract term) 
     return $ result :< term 

Je l'ai fait en deux phases parce que j'avais du mal à combiner le « retour d'un fonct ion "astuce avec retour d'un arbre annoté.

---

Un anamorphisme suivi d'un catamorphisme est connu comme hylomorphism.Nous pourrions définir la fonction composée en utilisant hylo, comme ceci:

together :: E -> Fix Term -> IO (Cofree Term R) 
together = curry (hylo alg coalg) 
    where 
    coalg (environment, Fix term) = ... 
    alg (environment COFREEF.:< termio) = ... 

---

Vous pouvez mettre sur pied calcEnv et calcResult sous la forme de l'algèbre originale comme ceci:

w :: Term (E -> IO R) -> E -> IO R 
w term environment = do 
    let downwards = calcEnv environment term 
    tr :: Term R <- sequenceA $ fmap ($ downwards) term 
    calcResult environment tr