Skip to content

Version 0.4.0

Compare
Choose a tag to compare
@lambdageek lambdageek released this 18 Sep 01:52

This release brings a bug fix that may be a breaking change for some ASTs, and a new combinator.

  • 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.
    #26

  • 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.