This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.
Components:
* assignments (passive data structure).
Now: just a map from unification vars to types (pb: what about partial types?)
maybe just local assignments (allow only vars as children of pair(α,β))
* constraint propagation: (buch of constraints) → (new constraints * assignments)
* sub-component: constraint selector (worklist / dynamic queries)
* sub-sub component: constraint normalizer: remove dupes and give structure
right now: union-find of unification vars
later: better database-like organisation of knowledge
* sub-sub component: lazy selector (don't re-try all selectors every time)
For now: just re-try everytime
* sub-component: propagation rule
For now: break pair(a, b) = pair(c, d) into a = c, b = d
* generalizer
For now: ?
Workflow:
Start with empty assignments and structured database
Receive a new constraint
For each normalizer:
Use the pre-selector to see if it can be applied
Apply the normalizer, get some new items to insert in the structured database
For each propagator:
Use the selector to query the structured database and see if it can be applied
Apply the propagator, get some new constraints and assignments
Add the new assignments to the data structure.
At some point (when?)
For each generalizer:
Use the generalizer's selector to see if it can be applied
Apply the generalizer to produce a new type, possibly with some ∀s injected
