Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
    Xavier Denis
    @xldenis

    @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?

    Xavier Denis
    @xldenis
    I'd also like GHC to not require a Alpha a context
    Aleksey Kliger (λgeek)
    @lambdageek

    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

    Valentin Robert
    @Ptival
    Hi @lambdageek , I'm having trouble understanding the type of fv, could you provide a little explanation?
    Aleksey Kliger (λgeek)
    @lambdageek
    @Ptival you can think of the type of 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)
    Jake Zimmerman
    @jez
    Super late to the convo on this one, but since I just recently got a grasp for 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
    Aleksey Kliger (λgeek)
    @lambdageek
    Very nice! I'm glad it turned out to be useful. (This is kind of what I hoped it would be useful for, but I never quite found a need for it in my own code - always seemed prudent to just use toListOf or toSetOf)
    Mark Lemay
    @marklemay
    Sorry if this is a dumb question:
    I have a simple lambda language and I want to do equality checking on it . I can't figure out how to unpack 2 lambda's simultaneously so they get the same De Bruijn index. or alternatively how to pick a new free var from the 2 expressions that I can apply to both.
    Any thoughts?
    Aleksey Kliger (λgeek)
    @lambdageek
    @marklemay You want 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.
    In a more general setting (for example if your have 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 Embeded types may differ.
    Mark Lemay
    @marklemay
    Thanks!
    David Davies
    @david-davies
    Hia @lambdageek , is there support for structural substitution, like in the λμ calculus?
    By which I mean reductions for control style operators:
    (μα.M)Nμα.M[[α]PN/[α]P] (\mu\alpha.M)N \longrightarrow \mu\alpha.M\big[ [\alpha] PN / [\alpha] P \big]. i.e. every subterm of the form [α]P[\alpha]P is replaced by [α]PN[\alpha]PN
    Aleksey Kliger (λgeek)
    @lambdageek
    @david-davies The default (generics-based) substitution just substitutes terms for variables. You can probably make your own 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
    Aleksey Kliger (λgeek)
    @lambdageek
    To be honest over the past few years I think of the library as primarily providing names and alpha-renaming/equivalence in a general sense of "name" that includes variables, symbols, channels (in the sense of the mu-calculus), etc, and working under binders for these things. The substitution support is nice for quick experiments, but it never really meshed with most of the stuff I tried to use the library for - I seemed to always be writing reductions by hand and almost never relying on any Subst instances.
    Aleksey Kliger (λgeek)
    @lambdageek
    @david-davies thinking about it a little more, I think you can probably do something. Since the \mu-variables like \alpha are a different syntactic class than ordinary term variables, what you can do is define two types 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
    where 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
    David Davies
    @david-davies
    @lambdageek Thanks! I didn't think of making a call to subst within the coerce -- nice one. I did realise though that I needed multiple different structural reductions (e.g. the one above but NN on the left), so I made 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 [α]P[\alpha]P . In the case above, the equivalent strubst function would be \x -> App x P.
    Thanks so much for a speedy response as well! :)