¿Cómo puedo recuperar compartir en un GADT?

Question

En Type-Safe Observable Sharing in Haskell Andy Gill muestra cómo recuperar el intercambio que existía en el nivel de Haskell, en una DSL. Su solución se implementa en el data-reify package. ¿Se puede modificar este enfoque para que funcione con GADT? Por ejemplo, dada esta GADT:

data Ast e where 
    IntLit :: Int -> Ast Int 
    Add :: Ast Int -> Ast Int -> Ast Int 
    BoolLit :: Bool -> Ast Bool 
    IfThenElse :: Ast Bool -> Ast e -> Ast e -> Ast e 

me gustaría compartir recuperarse mediante la transformación de la AST arriba para

type Name = Unique 

data Ast2 e where 
    IntLit2 :: Int -> Ast2 Int 
    Add2 :: Ast2 Int -> Ast2 Int -> Ast2 Int 
    BoolLit2 :: Bool -> Ast2 Bool 
    IfThenElse2 :: Ast2 Bool -> Ast2 e -> Ast2 e -> Ast2 e 
    Var :: Name -> Ast2 e 

por la forma de una función

recoverSharing :: Ast -> (Map Name, Ast2 e1, Ast2 e2) 

(I' m no estoy seguro sobre el tipo de recoverSharing.)

Tenga en cuenta que no me importa presentar un nuevo bindin gs a través de una construcción let, pero solo en la recuperación del intercambio que existía en el nivel Haskell. Es por eso que tengo recoverSharing devuelva un Map.

Si no se puede hacer como paquete reutilizable, ¿al menos se puede hacer para GADT específico?

Answer 1

¡Rompecabezas interesante! Resulta que puedes usar data-reify con GADTs. Lo que necesitas es un envoltorio que oculte el tipo en un elemento existencial. El tipo puede recuperarse posteriormente mediante la coincidencia de patrones en el tipo de datos Type.

data Type a where 
    Bool :: Type Bool 
    Int :: Type Int 

data WrappedAst s where 
    Wrap :: Type e -> Ast2 e s -> WrappedAst s 

instance MuRef (Ast e) where 
    type DeRef (Ast e) = WrappedAst 
    mapDeRef f e = Wrap (getType e) <$> mapDeRef' f e 
    where 
     mapDeRef' :: Applicative f => (forall b. (MuRef b, WrappedAst ~ DeRef b) => b -> f u) -> Ast e -> f (Ast2 e u) 
     mapDeRef' f (IntLit i) = pure $ IntLit2 i 
     mapDeRef' f (Add a b) = Add2 <$> (Var Int <$> f a) <*> (Var Int <$> f b) 
     mapDeRef' f (BoolLit b) = pure $ BoolLit2 b 
     mapDeRef' f (IfThenElse b t e) = IfThenElse2 <$> (Var Bool <$> f b) <*> (Var (getType t) <$> f t) <*> (Var (getType e) <$> f e) 

getVar :: Map Name (WrappedAst Name) -> Type e -> Name -> Maybe (Ast2 e Name) 
getVar m t n = case m ! n of Wrap t' e -> (\Refl -> e) <$> typeEq t t' 

Aquí está todo el código: https://gist.github.com/3590197

Editar: me gusta el uso de Typeable en la otra respuesta. Así que hice una versión de mi código con Typeable también: https://gist.github.com/3593585. El código es significativamente más corto. Type e -> se reemplaza por Typeable e =>, que también tiene una desventaja: ya no sabemos que los tipos posibles están limitados a Int y Bool, lo que significa que tiene que haber una restricción de Typeable e en IfThenElse.

Answer 2

Intentaré mostrar que esto se puede hacer para GADTs específicos, usando su GADT como ejemplo.

Usaré el paquete Data.Reify. Esto requiere que defina una nueva estructura de datos en la cual las posiciones recusivas son reemplazadas por un parámetro.

data AstNode s where 
    IntLitN :: Int -> AstNode s 
    AddN :: s -> s -> AstNode s 
    BoolLitN :: Bool -> AstNode s 
    IfThenElseN :: TypeRep -> s -> s -> s -> AstNode s 

Tenga en cuenta que elimino mucha información de tipo que estaba disponible en el GADT original. Para los primeros tres constructores, está claro cuál fue el tipo asociado (Int, Int y Bool). Para el último recordaré el tipo usando TypeRep (disponible en Data.Typeable). La instancia para MuRef, requerida por el paquete reify, se muestra a continuación.

instance Typeable e => MuRef (Ast e) where 
    type DeRef (Ast e)  = AstNode 
    mapDeRef f (IntLit a) = pure $ IntLitN a 
    mapDeRef f (Add a b) = AddN <$> f a <*> f b 
    mapDeRef f (BoolLit a) = pure $ BoolLitN a 
    mapDeRef f (IfThenElse a b c :: Ast e) = 
    IfThenElseN (typeOf (undefined::e)) <$> f a <*> f b <*> f c 

Ahora podemos usar reifyGraph para recuperar compartir. Sin embargo, se perdió mucha información de tipo. Intentemos recuperarlo.Alteré su definición de AST2 ligeramente:

data Ast2 e where 
    IntLit2 :: Int -> Ast2 Int 
    Add2 :: Unique -> Unique -> Ast2 Int 
    BoolLit2 :: Bool -> Ast2 Bool 
    IfThenElse2 :: Unique -> Unique -> Unique -> Ast2 e 

El gráfico del paquete Reify se parece a esto (donde e = AstNode):

data Graph e = Graph [(Unique, e Unique)] Unique  

Le permite hacer una nueva estructura de datos del gráfico, donde podemos almacenar Ast2 Int y Ast2 Bool por separado (por lo tanto, donde se ha recuperado la información del tipo):

data Graph2 = Graph2 [(Unique, Ast2 Int)] [(Unique, Ast2 Bool)] Unique 
      deriving Show 

Ahora sólo tenemos que encontrar una función de AstNode Gráfico (el resultado de reifyGraph) a Graph2:

recoverTypes :: Graph AstNode -> Graph2 
recoverTypes (Graph xs x) = Graph2 (catMaybes $ map (f toAst2Int) xs) 
            (catMaybes $ map (f toAst2Bool) xs) x where 
    f g (u,an) = do a2 <- g an 
        return (u,a2) 

    toAst2Int (IntLitN a) = Just $ IntLit2 a 
    toAst2Int (AddN a b) = Just $ Add2 a b 
    toAst2Int (IfThenElseN t a b c) | t == typeOf (undefined :: Int) 
         = Just $ IfThenElse2 a b c 
    toAst2Int _   = Nothing 

    toAst2Bool (BoolLitN a) = Just $ BoolLit2 a 
    toAst2Bool (IfThenElseN t a b c) | t == typeOf (undefined :: Bool) 
          = Just $ IfThenElse2 a b c 
    toAst2Bool _   = Nothing 

Vamos a hacer un ejemplo:

expr = Add (IntLit 42) expr 

test = do 
    graph <- reifyGraph expr 
    print graph 
    print $ recoverTypes graph 

Impresiones:

let [(1,AddN 2 1),(2,IntLitN 42)] in 1 
Graph2 [(1,Add2 2 1),(2,IntLit2 42)] [] 1 

La primera línea nos muestra que reifyGraph ha recuperado correctamente el uso compartido. La segunda línea nos muestra que solo se han encontrado Ast2 Int tipos (que también es correcto).

Este método es fácilmente adaptable para otras GADT específicas, pero no veo cómo podría hacerse completamente genérico.

El código completo se puede encontrar en http://pastebin.com/FwQNMDbs.