AmpersandTarski / Ampersand

Build database applications faster than anyone else, and keep your data pollution free as a bonus.
http://ampersandtarski.github.io/
GNU General Public License v3.0
40 stars 8 forks source link

Disambiguation #1417

Open stefjoosten opened 1 year ago

stefjoosten commented 1 year ago

The type system of Ampersand is sometimes more restricting than necessary. See, for example, issue #1147. Besides, the Haskell code for disambiguation is so terse that we decided (many years ago) that @sjcjoosten is the only person allowed to touch that code. Hence, the code for disambiguation is not maintainable.

@sjcjoosten has some ideas to simplify the algorithm, making it easier to understand and more maintainable. We hope to lessen the dependency on @sjcjoosten for maintaining that code. Besides, we expect it to disambiguate more than we do now. That solves, for example, issue #1147.

A complication is the vulnerability of the current code. We cannot afford to introduce new errors in it. Therefore, the theory is being developed entirely in Isabelle/HOL, to get a theory that is proven sound before we start implementing things.