« Changelog History


unbound-generics v0.4.1 Release Notes

Release Date: 2020-05-11 // almost 4 years ago

    • ➕ Add MonadFail instances for LFreshMT and FreshMT

    • 🏗 Builds with GHC 8.10


Previous changes from v0.4.0

    • 🆕 New binding specification type Ignore.

    Any two Ignore T terms will always be alpha-equivalent to each other, will be considered to contain no variables, and will not have any substitution apply beneath Ignore. Useful for attaching annotation terms to your AST.

        import Text.Parsec.Pos (SourcePos)

    data Expr =
       ...
       | Lambda (Ignore SourcePos) (Bind (Name Expr) Expr)

    As expected, any two Lambda expressions will be considered alpha-equivalent even if they differ in source position.

    Note that the Ignore will block operations on Name a for all a, which can be a little unexpected:

        data Ty =
      TyVar (Name Ty)
      | TyArr Ty Ty

    instance Subst Ty Ty where
      ...

    data Expr =
      ...
      | Var (Name Expr)
      | Lambda (Ignore Ty) (Bind (Name Expr) Expr)

     instance Subst Ty Expr

    Applying a substitution of a type for a free type variable to a Lambda will not descend into the Ignore Ty.

    Thanks Reed Mullanix (TOTWBF) for the new operation.

    • 🛠 Fix an issue in substitution where traversal would not continue in an AST node for which isvar or isCoerceVar is defined to return non-Nothing but which had additional structure.

    For example, in a language with meta variables and explicit substitutions:

         data Expr =
       ...
         -- normal variables that stand for expressions
       | Var (Name Expr)
          -- a meta variable occurrence and an explicit substitution
          -- of expressions to substitute in for the free variables
       | MetaVar (Name Meta) [(Name Expr, Expr)]
     -- a meta variable stands for an expression with some free term vars
     data Meta = MetaVar Expr

     -- substitution for a meta in an expression
     instance Subst Expr Meta where
       isCoerceVar (MetaVar u sub) = Just (SubstCoerce u (Just . applyExplicitSubst sub))
     applyExplicitSubst :: [(Name Expr, Expr)] -> Meta -> Expr
     applyExplicitSubst s (MetaVar e) = substs s e

    Given an expression e1 defined as MetaVar "u" [("x", 10)], we may want to substitute a Meta ("x" + "x") for "u" to get 10 + 10 (that is, we replace "u" by the expression "x" + "x" and immediately apply the substitution 10 for "x").

    Now suppose we have an expression e2 defined as MetaVar "v" [("y", e1)] (that is, an occurrence of meta var "v" together with a substitution of e1 from above for "y"). If we again try to substitute Meta ("x" + "x") for "u" in e2, we would expect to get MetaVar "v" [("y", 10 + 10)] (that is, since "v" is not equal to "u", we leave the meta var alone, but substitute for any occurrences of "u" in the explicit substitution, so e1 becomes 10 + 10 as before).

    The bug in previous versions of unbound-generics was that we would incorrectly leave MetaVar "v" [("y", e1)] unchanged as soon as we saw that isCoerceVar (MetaVar "v" [("y", e1)]) returned Just (SubstCoerce "u" ...) where "u" /= "v".

    Thanks Reed Mullanix (TOTWBF) for finding and fixing this issue. https://github.com/lambdageek/unbound-generics/issues/26