AST with unbound + recussion schemes for transformations

[csabahruska]

Does unbound semantics allow to create the shape functor for the AST? It would help a lot to implement the AST transformations using recursion schemes. I.e. in this short closure conversion tutorial It would be useful example to have the same thing but with unbound.

[sweirich]

RepLib/Unbound does not have the facility to do this now. The only way to define new datatypes based on existing ones (i.e. the shape functor) is using TemplateHaskell. RepLib already uses TH to construct representation types; it would be possible to extend this to also construct shape functors too.

However, you might be able to replace your uses of cata with datatype-generic functions. For example, Unbound defines a generic version of the free variable function.

[csabahruska]

Is it possible to create the shape functor manually for a recursive data type that uses unbound? Or would it break unbound semantics? I.e. to write

data Term a = Var (Name a)
          | App a a
          | Lam (Bind (Name a) a)

instead of

data Term = Var (Name Term)
          | App Term Term
          | Lam (Bind (Name Term) Term)

[sweirich]

So, this doesn't work directly. It's fine to define the shape functor

type Var = Name Term
data TermF a = VarF Var
          | AppF a a
          | LamF (Bind [Var] a)

But the problem is that TermF is not actually a functor. In the LamFcase, we need to decompose the binding, but to do that we need a and b to be in the Alpha class. Furthermore, to make sure that we have a suitably fresh variable, this should also be in the context of a freshness monad.

instance Functor TermF where
    fmap :: (a -> b) -> TermF a -> TermF b
    fmap f (VarF n)     = VarF n
    fmap f (AppF a1 a2) = AppF (f a1) (f a2)
    fmap f (LamF bnd)   = undefined
      -- can't do anything here

Instead, we need to work we new recursion schemes that include the monadic traversal of the term.

So imagine that we had these definitions

fmapM :: (Alpha a, Alpha b, LFresh m) => (a -> m b) -> TermF a -> m (TermF b)
fmapM f (VarF n)     = return $ VarF n
fmapM f (AppF a1 a2) = AppF <$> (f a1) <*> (f a2)
fmapM f (LamF bnd)   = lunbind bnd $ \ (x,a1) -> f a1 >>= \ b1 -> return $ LamF (bind x b1)

cataM :: forall a m.  (Alpha a, LFresh m) => (TermF a -> m a) -> Term -> m a
cataM f x = fmapM (cataM f) (project x) >>= f  where

Then your closure conversion function can be defined using cataM

closConv :: (LFresh m) => [Var] -> Term -> m Term
closConv globals t = avoid (map AnyName globals) $ cataM folder t
  where folder (LamF bnd) =
            let vars = fv (LamF bnd) `without` globals in
            lunbind bnd $ \(vs,a) -> return $ (Lam (bind (vars ++ vs) a)) `applyTo` vars
        folder e = return $ embed e

[csabahruska]

fmapM :: (Alpha a, Alpha b, LFresh m) => (a -> m b) -> TermF a -> m (TermF b)

is pretty similar to mapM

class (Functor t, Foldable t) => Traversable t where
    mapM :: Monad m => (a -> m b) -> t a -> m (t b)

Is TermF a Traversable (but not a Functor)? If so why should Traversable t must be Functor t also if TermF works just fine?

[sweirich]

TermF is neither a Functor nor Traversable. The version of fmapM that I used is less general than mapM due to the constrained polymorphism.

On Aug 16, 2017, at 6:56 PM, Csaba Hruska [email protected] wrote:

fmapM :: (Alpha a, Alpha b, LFresh m) => (a -> m b) -> TermF a -> m (TermF b) is pretty similar to mapM

class (Functor t, Foldable t) => Traversable t where mapM :: Monad m => (a -> m b) -> t a -> m (t b) Is TermF a Traversable (but not a Functor)? If so why should Traversable t must be Functor t also if TermF works just fine?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/sweirich/replib/issues/43#issuecomment-322921993, or mute the thread https://github.com/notifications/unsubscribe-auth/ACAZdhbgvb9l92tQ9q_ywmRRjtPKibDFks5sY3OEgaJpZM4OuZwW.