@lambdageek how do I reuse generic implementations for functorised ASTs?
ie:
data Expr a = Var a (Name (Expr a))
| Other Constructors
I'd like Alpha
to ignore the annotations (a). However, writing a manual implementation to the class is tedious (given there are 6 methods that need to be written) if I only need to change 1-2 cases. Is there a way to default to the generic implementation in other cases?
Hey, sorry I didn't notice your message @xldenis . All the methods have default implementations provided that Expr a
is an instance of Generic
, so you can just change the ones you want. If you want to call down to the generic impl, you would need to do something like
(GHC.Generics.to . gopen ctx pat . GHC.Generics.from) subTerm
The various g*
functions are defined in Unbound.Generics.LocallyNameless.Alpha
. If you can stand a newtype, what I usually do is something like
newtype Annot a = Annot {getAnnot :: a }
deriving ({- everything -})
and then write an instance for Annot a
that just uses (==)
and compare
and is the identity for functions like open
and close
and then populate your AST with Annot a
values
fv
as (Alpha a, Typeable b) => Fold a (Name b)
in the sense of the lens libary's Fold. What that means, roughly is that given some syntax structure a
(which is an instance of Alpha
) you can use fv
to iterate over free variables Name b
that occur within it and summarize them using some kind of Monoid
very similar to how the Foldable
typeclass works. More concretely, if you have some Expr
type that has variables of type Name Expr
in it, you can do toListOf fv :: Expr -> [Name Expr]
(using the definition of toListOf
from lens
, or the one in Unbound.Generics.LocallyNameless.Internal.Fold
) more generally foldMapOf fv :: Monoid r => (Name Expr -> r) -> Expr -> r
lets you use some other monoid to summarize the free variables. One that I find useful all the time, for example, is Data.Set.Lens.setOf fv :: Expr -> Data.Set.Set (Name Expr)
(setOf
is in lens
and Data.Set.Set
is from containers
)
fv
and lenses more generally, this is one of the ways I frequently use fv
: checking whether a variable is in the free variables of another term:import Control.Lens (noneOf)
import Data.Typeable (Typeable)
import Unbound.Generics.LocallyNameless
-- This uses lenses because unbound-generic's fv supports lenses!
-- fv is a Getter combinator that gets the free variables of a structure, and
-- noneOf lets us fold over that structure, checking that none of them are (== t)
notInFreeVars :: (Alpha a, Typeable a) => Name a -> a -> Bool
notInFreeVars t t1 = noneOf fv (== t) t1
unbind2
or lunbind2
. If you have Lam (Bind Var Expr)
in your datatype definition, and Lam b1
and Lam b2
, you can do
something like this in the Fresh m
monad: Just (v1, e1, _, e2) <- unbind e1 e2
to get at the subexpressions. If you are in LFresh m
, then lunbind b1 b2 $ \(Just (v1, e1, _, e2) -> ... )
will work.
Lam (Bind (Var, Embed Type) Expr)
- ie, the pattern portion of the Bind
is more complicated than just a single variable, you will want to hold on to both sides when you unbind2
. something like Just (p1, e1, p2, e2) <- unbind b1 b2
. And then unpack p1 and p2 - the variables will be renamed when unbinding so that they are same, but the Embed
ed types may differ.
Subst Term Term
instances that do a little bit of structural analysis in the subst
function to do the $[\alpha]P N / [\alpha]P$ substitution and delegate to gsubst
for the generic case. But of course that defeats the purpose of the library somewhat. :D
Terms
and Command
where variables x stand for Terms, and mu variables \alpha "stand" for Commands. So you have instance Subst Term Term
with a normal definition of isvar
that does the usual structural substitution. And an instance Subst Command Term
that treats the term Box alpha p
(ie [\alpha]P) as a variable and uses isCoerceVar
to return a SubstCoerce alpha (\n -> Box alpha (subst p n)
. I think that will have the right behavior
data Term = V (Name Term) | App Term Term | Lambda (Bind (Name Term) Term) | Mu (Bind (Name Command) Command)
and data Command = Box (Name Command) Term
is the syntax representation
StrSubst
and GStrSubst
typeclasses, where the equivalent of subst
was strubst :: Name b -> (b -> b) -> a -> a
, so you could give it a function to tell it what to do when it gets to the named term $[\alpha]P$. In the case above, the equivalent strubst function would be \x -> App x P
.