haskell - que - no puedo compartir publicaciones en mi pagina de facebook

¿Cómo puedo recuperar el compartir en un GADT?

Question

En el uso compartido observable de tipo seguro en Haskell, Andy Gill muestra cómo recuperar el intercambio que existía en el nivel de Haskell, en un DSL. Su solución se implementa en el paquete data-reify . ¿Se puede modificar este enfoque para trabajar con GADTs? Por ejemplo, dado este 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 recuperar el intercambio transformando el AST anterior a

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)

(No estoy seguro sobre el tipo de recoverSharing .)

Tenga en cuenta que no me importa la introducción de nuevos enlaces a través de una construcción de dejar, sino solo en la recuperación de la compartición que existía en el nivel de Haskell. Es por eso que tengo que recoverSharing un Map .

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

Answer 1

Intentaré demostrar que esto se puede hacer para GADT específicos, utilizando su GADT como ejemplo.

Usaré el paquete Data.Reify . Esto requiere que defina una nueva estructura de datos en la que las posiciones recusivas sean 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 era 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 el intercambio. Sin embargo, se perdió mucha información de tipo. Tratemos de recuperarlo. Cambié un poco tu definición de Ast2 :

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 tiene este aspecto (donde e = AstNode ):

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

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

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

Ahora solo necesitamos encontrar una función de Graph AstNode (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

Huellas dactilares:

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 se ha recuperado correctamente compartiendo. La segunda línea nos muestra que solo se han encontrado tipos Ast2 Int (lo que también es correcto).

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

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

Answer 2

Rompecabezas interesante! Resulta que se pueden usar datos reificados con GADTs. Lo que necesita es una envoltura que oculte el tipo de una forma existencial. El tipo se puede recuperar más adelante mediante la coincidencia de patrones en el Type datos Tipo.

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á el código completo: https://gist.github.com/3590197

Edit: 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 -> es reemplazado por Typeable e => , que también tiene un inconveniente: ya no sabemos que los tipos posibles están limitados a Int y Bool , lo que significa que debe haber una restricción Typeable e en IfThenElse .