Instead of constantly making these updates, let's just remove the year
since things are stored in git anyways, and this is not an actual modern
legal risk anymore.
We forgot to omit looking deeper into private struct fields. I don't
know why we didn't catch this earlier, I can only assume some subtlety
changed, since we've previously used many of the resources this would
fail on. Maybe golang broke some API that they didn't consider stable?
This also adds a new test for this, and ensures each resource can be
inspected too!
This adds a modern type unification algorithm, which drastically
improves performance, particularly for bigger programs.
This required a change to the AST to add TypeCheck methods (for Stmt)
and Infer/Check methods (for Expr). This also changed how the functions
express their invariants, and as a result this was changed as well.
This greatly improves the way we express these invariants, and as a
result it makes adding new polymorphic functions significantly easier.
This also makes error output for the user a lot better in pretty much
all scenarios.
The one downside of this patch is that a good chunk of it is merged in
this giant single commit since it was hard to do it step-wise. That's
not the end of the world.
This couldn't be done without the guidance of Sam who helped me in
explaining, debugging, and writing all the sneaky algorithmic parts and
much more. Thanks again Sam!
Co-authored-by: Samuel Gélineau <gelisam@gmail.com>
This adds the core unification helper functions that do the core work of
solving the invariants. This includes the actual Unify, OccursCheck, and
Extract which is sometimes known as "zonk".
A few other small functions are also included.
Co-authored-by: Samuel Gélineau <gelisam@gmail.com>
This adds a unification optimizations API, and uses it to optimize the
embedded provisioner. With these turned on, type unification drops from
around 1m45s to 2.5s which is a 40x speedup.
This is a bit of a hack until we improve the GAPI a bit, but will let us
shut down type unification a bit faster if we want to interrupt a long
running operation. Hopefully our future algorthmic performance
improvements will obliviate the need for this to be a common issue.
With the recent merging of embedded package imports and the entry CLI
package, it is now possible for users to build in mcl code into a single
binary. This additional permission makes it explicitly clear that this
is permitted to make it easier for those users. The condition is phrased
so that the terms can be "patched" by the original author if it's
necessary for the project. For example, if the name of the language
(mcl) changes, has a differently named new version, someone finds a
phrasing improvement or a legal loophole, or for some other
reasonable circumstance. Now go write some beautiful embedded tools!
We were skipping over being fully consistent with all of the generator
invariants when running the solver. This allowed us to miss some of the
conditions that a generator might impose. Usually this caused us to be
"solved" when in fact we had an invalid program.
We want to add the equality to the main list of equalities in case it is
needed somewhere else. This doesn't have any effect on any of our test
cases, but it doesn't seem to be harmful, and it could conceivably be
useful in the future. This is a separate commit in case we want to check
if this behaviour still holds true well into the future.
These two vars are used pretty deeply through this code, so rename them
to prevent any confusion.
We also switch from a range loop to a counter so that the loop list can
be changed while it's looping.
The set of initial invariants that we see might include:
?8 = func(inputs []int, function ?4) ?3
?8 = func(inputs []int, function ?10) ?9
?8 = func arg0 []int, arg1 ?6) ?7
From this we can infer that since they are all equal, that we also know
that ?4, ?10 and ?6 must also be equal. The same is true of ?3, ?9 and
?10. Those new equalities are sometimes necessary in order to complete
the full unification.
The second interesting aspect is when we have dissimilar equalities:
?2 = func(x ?1) str
?4 = func(a int) ?5
?10 = func(a int) ?11
In this example we also have an additional equality:
?6 = ?2
From this and the above we can determine that ?2, ?4, ?6 and ?10 are all
equal. We only know about ?4, ?6, and ?10 from the direct relationship,
and we add in ?2 from the indirect (graph) relationship. These
relationships let us determine new information that ?5 and ?11 are both
str and that ?1 is an int.
Two important reminders:
1) Arg names don't have to match. It would impossible to build such a
system where this was both possible, but also let us name our
functions sanely.
2) None of this guarantees we won't find an inconsistency in our
solution. If this is found, it simply means that someone wrote code
which does not type check.
When we were running our partial unification to compare similar looking
function invariants, we would sometimes learn new information, even if
it didn't entirely solve that invariant. When this new information was
learned, it's important that we globally mark it as solved so that
others can use it to complete their invariants. When it was a critical
piece of information, this would result in new information, which would
eventually lead to that original partial invariant that we learned that
information from to becoming solved.
This presents things in a more formal way for those who are more
familiar with standard type unification syntax.
Patch created by Sam, and cleaned up by James.
It's important that during unification that function types can unify
even if their arg names are different. (Their actual unnamed types must
be identical of course.) This adds a test to make sure we preserve this
behaviour.
This adds a new interpretation of the EqualityWrapFuncInvariant that can
combine two into one if their Expr1 fields are the same. We might know
different partial aspects of multiple functions. This also includes a
test. The test does not pass before this commit which adds it.
There were a bunch of packages that weren't well documented. With the
recent split up of the lang package, I figured it would be more helpful
for new contributors who want to learn the structure of the project.
This extends our simple solver so that it can understand the new
invariants. For the Value holding invariants, it doesn't do much-- those
are expected to be used within the execution of the GeneratorInvariant
so they are passed through untouched. For the GeneratorInvariant it must
actually try running this periodically to see if it produces new
invariants that are helpful for the whole solution. Since this could get
expensive quickly, the logic is to only try running these once we've
entered steady state, but before we've tried to reach for the
ExclusiveInvariant's. The exclusives are the most expensive so we run
these last, and the generators are run late because they won't usually
produce anything helpful unless some of the basic solving has already
happened. If they could produce useful things right away, then there
wouldn't be a need for them!
We should probably move these into the central interfaces package so
that these can be used from multiple places. They don't have any
dependencies, and it doesn't make sense to have the solver code mixed in
to the same package. Overall the interface being implemented here could
probably be improved, but that's a project for another day.
This ensures that docstring comments are wrapped to 80 chars. ffrank
seemed to be making this mistake far too often, and it's a silly thing
to look for manually. As it turns out, I've made it too, as have many
others. Now we have a test that checks for most cases. There are still a
few stray cases that aren't checked automatically, but this can be
improved upon if someone is motivated to do so.
Before anyone complains about the 80 character limit: this only checks
docstring comments, not source code length or inline source code
comments. There's no excuse for having docstrings that are badly
reflowed or over 80 chars, particularly if you have an automated test.
This adds a giant missing piece of the language: proper function values!
It is lovely to now understand why early programming language designers
didn't implement these, but a joy to now reap the benefits of them. In
adding these, many other changes had to be made to get them to "fit"
correctly. This improved the code and fixed a number of bugs.
Unfortunately this touched many areas of the code, and since I was
learning how to do all of this for the first time, I've squashed most of
my work into a single commit. Some more information:
* This adds over 70 new tests to verify the new functionality.
* Functions, global variables, and classes can all be implemented
natively in mcl and built into core packages.
* A new compiler step called "Ordering" was added. It is called by the
SetScope step, and determines statement ordering and shadowing
precedence formally. It helped remove at least one bug and provided the
additional analysis required to properly capture variables when
implementing function generators and closures.
* The type unification code was improved to handle the new cases.
* Light copying of Node's allowed our function graphs to be more optimal
and share common vertices and edges. For example, if two different
closures capture a variable $x, they'll both use the same copy when
running the function, since the compiler can prove if they're identical.
* Some areas still need improvements, but this is ready for mainstream
testing and use!
The simple type unification algorithm suffered from some serious
performance and memory problems when used with certain code bases. This
adds some crucial optimizations that improve performance drastically.
This is an initial implementation of the mgmt language. It is a
declarative (immutable) functional, reactive, domain specific
programming language. It is intended to be a language that is:
* safe
* powerful
* easy to reason about
With these properties, we hope this language, and the mgmt engine will
allow you to model the real-time systems that you'd like to automate.
This also includes a number of other associated changes. Sorry for the
large size of this patch.
