In Type-Safe Observable Sharing in Haskell Andy Gill shows how to recover sharing that existed on the Haskell level, in a DSL. His solution is implemented in the data-reify package. Can this approach be modified to work with GADTs? For example, given this 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
I'd like to recover sharing by transforming the above AST to
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
by the way of a function
recoverSharing :: Ast -> (Map Name, Ast2 e1, Ast2 e2)
(I'm not sure about the type of recoverSharing
.)
Note that I don't care about introducing new bindings via a let construct, but only in recovering the sharing that existed on the Haskell level. That's why I have recoverSharing
return a Map
.
If it can't be done as reusable package, can it at least be done for specific GADT?
Interesting puzzle! It turns out you can use data-reify with GADTs. What you need is a wrapper that hides the type in an existential. The type can later be retrieved by pattern matching on the Type
data 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'
Here's the whole code: https://gist.github.com/3590197
Edit: I like the use of Typeable
in the other answer. So I did a version of my code with Typeable
too: https://gist.github.com/3593585. The code is significantly shorter. Type e ->
is replaced by Typeable e =>
, which also has a downside: we no longer know that the possible types are limited to Int
and Bool
, which means there has to be a Typeable e
constraint in IfThenElse
.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With