-
Notifications
You must be signed in to change notification settings - Fork 7
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Simplifying Silver's possibly-decorated type inference semantics #751
Comments
Initial thoughts:
👍
Maybe a new kind of pattern that
Using
Firmly in the "future planning" category, but if we do, it'd be nice to leave the syntax open to specifying a "deriving strategy". Haskell's ended up having a few of these, and in the Rust world, user libraries can provide their own as derive macros. At least in the Rust world, this has reduced the need for an equivalent to GHC.Generics quite a lot, and probably fits with our extensible-languages goals better. |
Well, there are a bunch of syntactic ambiguities (and potential confusion) if we have both |
Current status: I've made the changes to implement the new semantics, which was relatively straightforward. I'm currently in the middle of refactoring Silver to be able to build itself again. |
A couple notes from doing the refactoring in Silver:
|
The above is still pretty much the plan, except that unique references are being removed entirely, and the syntax for the |
As was discussed offline about a month ago, removing |
The current state of affairs is that whether a reference to a decorable child or local1 gets a decorated type is inferred through a "fun trick" in the type system. This can be confusing2, and we also make it far too easy IMO to un-decorating a tree that has already been decorated. Since we want to make only decorating something in one place the new normal, one should need to be explicit by writing
new
when they actually do wish to copy a tree.Background
As a quick refresher, a type is decorable when it is:
The "base type" of a decorable type is the
nt
inDecorated! nt with i
for a unique reference type, or else just the nonterminal/type constant.The way it currently works is that a use of a child or local declared with a reference type gets a possibly-decorated type (
ntOrDecType
is the name of the production, but it doesn't have syntax or appear in error messages.) AntOrDecType
for base typent
is permitted to unify withnt
,Decorated nt with i
orDecorated! nt with i
, and after unification the type gets replaced with what it was specialized to - thentOrDecType
constructor has an extra hidden type variable to track this.ntOrDecType
s that are still unspecialized after unification default toDecorated nt with {}
.This does pose a problem when we write e.g.
x == y
wherex
andy
are both possibly-decoratednt
s, where there is an instance forEq nt
. Sinceeq :: (Boolean ::= a a)
is polymorphic, we never specializex
andy
to be undecorated, and get the defaultDecorated nt with {}
, which doesn't have anEq
instance. As a gross workaround for this, I made function application check if the applied function type has any type constraints that are only satisfiable if specialized to an undecorated type, and if so does the specialization.We also have special semantics for "lexical local variables", which are anything bound in a let/pattern match. Anything bound with a decorated type is permitted to implicitly undecorate, meaning these also get an
ntOrDecType
type. We do want to disallow casting betweenDecorated
types with different sets of inherited attributes, thus thentOrDecType
constructor also has anInhSet
type member to control what the reference set should effectively be when unifying with aDecorated
/Decorated!
type.This state of affairs almost always does the right thing, but can lead to some truly perplexing behavior for someone who doesn't understand what is going on behind the scenes. Having separate top-level types for
Decorated
andDecorated!
is also suboptimal, e.g. we need bothnew :: (a ::= Decorated a with i)
andnewUnique :: (a ::= Decorated! a with i)
.Proposal
First,
Decorated
andDecorated!
are combined into a single top-level type constructorDecorated :: (Uniqueness -> InhSet -> * -> *
. Uniqueness is determined by a new kindUniqueness
, which has types!
for unique and~
3 for not unique. The current syntax can stay as syntactic sugar, i.e.Decorated a with i
forwards toDecorated<~ i a>
andDecorated! a with i
forwards toDecorated<~ i a>
.Now for any use of a child/local
x
bound with a decorable base typent
, we infer the typeDecorated<u i nt>
. This can unify with a unique reference type (as when writing@x
), unify with a non-unique reference type, or remain unspecialized (as in the case of an attribute access onx
.) Any unspecializedUniqueness
type var would default to~
, and any unspecializedInhSet
type var would still default to{}
, for the purposes of the the flow/uniqueness analyses.To get a fresh undecorated version of a child/local, e.g. in a functor attribute equation or strategy attribute rewrite rule, one now would need to write
new(x)
. In unique contexts such as forward and local equations one would typically write@x
.Pattern variables would also be always decorated by default, so you would also sometimes need to write
new
when pattern matching. Similarly, let-bindings would lose their auto-undecoration behavior and just always give the bound type - this was always a bit weird and mostly an artifact of how pattern matching is implemented.Discussion
One downside of this is that strategy attribute rewrite rules get a bit more verbose, as one frequently wishes to copy a subtree. That's probably fine, the user should be aware that they are potentially causing a tree to be re-decorated anyway.
Getting decorated types for "data" nonterminals by default is quite unfortunate, e.g. if a production/function has a
Maybe<a>
child/parameter. The fix for this is probably introducing some sort of non-decorable variant of nonterminal as @remexre has suggested (#556). This wouldn't permit inherited attributes, but probably could still have synthesized attributes with empty flow types. As an optimization the synthesized attributes could be cached on the undecorated term. This would also mean things like theEnv
nonterminal in Silver/ableC could be used as justEnv
and notDecorated Env
.Note that deriving equality by propagating
compareTo
andisEqual
would no longer work for data nonterminals, but this was already broken for "record nonterminals" using annotations. We might consider adding a more classic deriving extension forEq
andOrd
that just does pattern matching and does compare annotations.Sometimes we write helper functions for constructing trees, where we don't really want to decorate the parameters in the first place. Needing to undecorate them is already problematic in case the operands contain unique references. The solution to this is probably to actually finish #454, adding concise function syntax which doesn't decorate the parameters.
Overall this would be a pretty significant breaking change for Silver, but would reap significant benefits for future maintainers/users. I am in favor of starting on this as soon as decoration site flow projections (and potentially also forward production attributes) are complete, which would be a good point for another Silver release. It would also be good to finish moving ableC and extensions to use origin tracking before merging another major breaking change.
Footnotes
By local I really mean local or production attribute in this writeup. ↩
Citation: @remexre complaining about "decoration inference", which is really just part of the type system and not its own thing, but I digress. ↩
I don't love that syntax, I just needed something to use for now. The first idea I had was
*
but that could cause confusion with kind*
. I'm open to suggestions. ↩The text was updated successfully, but these errors were encountered: