unbound-generics v0.4.0 Release Notes
Release Date: 2018-09-18 // over 5 years ago-
- ๐ 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 beneathIgnore
. 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 onName a
for alla
, 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 theIgnore 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
orisCoerceVar
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 asMetaVar "u" [("x", 10)]
, we may want to substitute aMeta ("x" + "x")
for"u"
to get10 + 10
(that is, we replace"u"
by the expression"x" + "x"
and immediately apply the substitution10
for"x"
).Now suppose we have an expression
e2
defined asMetaVar "v" [("y", e1)]
(that is, an occurrence of meta var "v" together with a substitution ofe1
from above for"y"
). If we again try to substituteMeta ("x" + "x")
for"u"
ine2
, we would expect to getMetaVar "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, soe1
becomes10 + 10
as before).The bug in previous versions of
unbound-generics
was that we would incorrectly leaveMetaVar "v" [("y", e1)]
unchanged as soon as we saw thatisCoerceVar (MetaVar "v" [("y", e1)])
returnedJust (SubstCoerce "u" ...)
where"u" /= "v"
.Thanks Reed Mullanix (TOTWBF) for finding and fixing this issue. https://github.com/lambdageek/unbound-generics/issues/26
- ๐ New binding specification type