Disambiguation

[stefjoosten]

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.