Changes between Version 17 and Version 18 of Plugins/TypeChecker/RowTypes/Coxswain/Notes


Ignore:
Timestamp:
May 24, 2018 6:43:20 PM (15 months ago)
Author:
nfrisby
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Plugins/TypeChecker/RowTypes/Coxswain/Notes

    v17 v18  
    263263The implicit variables must be removed. The "inflation" issue is just a quality of life concern and there's no clear right answer: should inferred contexts and error messages put as much information as possible into each constraint (thereby risking redundancies) or as little (compact but less transparent)?
    264264
    265 For the equality store, my rough plan is to handle both issues (preferring compactness over transparency) in one step: before writing out the equalities in the store, for each root (i.e. variable not in the domain of the substitution), I'll compact that root's equality constraints by finding a minimum spanning tree of the weighted fully connected graph in which each node is a variable in the substitution domain whose mapping extends that root and each weight is the total `typeSize` of the union of their extension minus the intersection of their extension and emit the MST's edges as the simplified equality constraints.
    266 
    267 I haven't considered the `Lacks` store yet.
     265For the equality store, my rough plan is to handle both issues (preferring compactness over transparency) in one step: before writing out the equalities in the store, for each implicit variable root, I'll compact that root's equality constraints by finding a minimum spanning tree of the weighted fully connected graph in which each node is a variable in the substitution domain whose mapping extends that root and each weight is the total `typeSize` of the union of their extension minus the intersection of their extension and emit the MST's edges as the simplified equality constraints. For explicit variable roots and the empty set root, no processing is strictly necessary, but the same algorithm would compact their representation, I think.
     266
     267I haven't considered the `Lacks` store yet. I haven't convinced myself that a greedy algorithm would find the minimal way to express a set form.