Est-il possible de stocker un GADT à l'intérieur d'un transformateur de monade d'État ?

Question

Disons que j'ai un GADT comme celui-ci :

data Term a where
  Lit    :: a -> Term a
  Succ   :: Term Int -> Term Int
  IsZero :: Term Int -> Term Bool
  If     :: Term Bool -> Term a -> Term a -> Term a

Est-il possible de stocker Succ (Lit 2) y IsZero (Succ (Lit 2)) dans le transformateur de la monade State, en tant que valeur de l'état interne ?

Le problème ici est que ces deux-là sont de types différents, et je ne sais pas comment le s de StateT s m a doivent être tapés.

Edit : ATerm a résolu la question initiale de savoir comment stocker différentes GADT dans l'état, le problème maintenant est que depuis que le type est perdu, il semble impossible de comparer l'ancien et le nouvel état.

Edit : Réponse finale.

Après avoir échangé avec @luqui, voici l'extrait de code complet qui répond à cette question.

N'hésitez pas à le faire. repl et faire un essai.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}

import Data.Typeable

data Term a where
  Lit    :: a -> Term a
  Succ   :: Term Int -> Term Int
  IsZero :: Term Int -> Term Bool
  If     :: Term Bool -> Term a -> Term a -> Term a

deriving instance (Eq a) => Eq (Term a)

data ATerm where
  ATerm :: (Typeable a, Eq a) => Term a -> ATerm

instance Eq ATerm where
    ATerm t == ATerm u
        | Just t' <- cast t = t' == u
        | otherwise = False

main :: IO ()
main = return ()

Answer 1

Oui, vous pouvez utiliser un existentiel

data ATerm where
   ATerm :: Term a -> ATerm

qui est un monotype qui stocke "un Term de tout type".

Cependant, vous devez savoir que vous perdre les informations sur le type, ce qui, j'en suis sûr, ne posera pas de problème dans votre cas. Si vous avez besoin de le récupérer, vous devrez ajouter des informations de type Typeable ou une autre astuce - difficile à dire sans plus de contexte sur ce que vous faites.

EDITAR

Pour récupérer les informations sur le type, vous devez les inclure dans le fichier ATerm

data ATerm where
    ATerm :: (Typeable a, Eq a) => Term a -> ATerm

Malheureusement, ce changement pourrait causer Typeable pour infecter une bonne partie de votre code. C'est comme ça que ça se passe. Nous incluons également Eq a puisque si nous comparons ATerms et constatent que leurs types sont les mêmes, nous devrons comparer sur ce type.

Ensuite, pour comparer deux ATerm vous devez d'abord comparer leurs types, puis leurs valeurs. Cela peut être fait avec la fonction Typeable bibliothèque.

instance Eq ATerm where
    ATerm t == ATerm u
        | Just t' <- cast t = t' == u
        | otherwise = False

Heureusement, votre Term GADT ne cache aucun type. Si vous aviez un cas comme, par exemple

data Term a where
    ...
    Apply :: Func a b -> Term a -> Term b

vous devez ajouter Typeable également à toutes les variables cachées (variables qui n'apparaissent pas dans le type de résultat)

    Apply :: (Typeable a) => Func a b -> Term a -> Term b

En gros, si vous voulez comparer des types, vous devez avoir un Typeable contrainte sur eux quelque part.