Logic subtyping and overloading

[auht]

2025-02-26 TODO:

• Add spaces like a civilized person
• Check intersections for WFedness
• Remove assumption that only the first argument needs disjointness
  • Deal with nested dss
• Support generalization (update collectTVs)
• Add records (for now use temporary syntax fun foo: ["x": Int, "y": Int])

2025-03-06 TODO:

• don't duplicate when LB is TV on same or higher level, in which case you can make both vars bound each other (same level) or the other one bound the LB
• properly update type simplifier (and remove kludge)
• remove use of nondeterministic collections

Later:

• During simplification, take UBs into account to reduce things

2025-03-13 TODO:

Later:

• use different propagation rules for TVs of same level
• add an option to enable/disable :logicSub

[LPTK]

wat

[auht]

The { x: 1 } is elaborated to a Tup with an ascription ["x": 1].
It is typed as id("x") since the ascription is ignored.

[LPTK]

I wonder why this happens. Are you sure it's an ascription? It should elaborate to a RecordField

[auht]

It is a Fld with the field asc set as Some(1).
Similarly, id of { x: 1, y: 2 } reports incorrect number of arguments. It is an error in basic/Records.mls originally.

[LPTK]

Ok I'll look into it.

[LPTK]

Actually it's working "as intended". Currently, curly braces are equivalent to an indented block. Here one would need normal parentheses instead

id of (x: 1)

[LPTK]

For patmat without default cases, can't we just implicitly add a case that matches the negations of all previous patterns and constrains the scrutinee to be Bot?

[LPTK]

(This inferred type scheme, like the original one from BbML, misinterprets the patmat as being exhaustive, thus allowing 'x = ~Int as a – spurious – solution.)

[LPTK]

🤔

[LPTK]

Any reason why you use a record on the LHS and tuples on the RHS? Why are the RHS' treated like records? They should be one-element arrays. Remember that [ fst: Tru, snd: Tru ] is syntax sugar for [ (fst: Tru, snd: Tru) ].

[LPTK]

How come this type checks? Shouldn't it be Prod[Tru | Fls, Tru | Fls]?

[auht]

Because classes are merged in union. It is actually Prod[Tru | Fls, Tru | Fls] here.
The example using record does not type check.
The original paper uses tuple and type checks: $(y(\lambda x.x), y(\lambda x.x)): (True \times True) \lor (False \times False)$

[LPTK]

Wait why does it type check in the original paper, then? Do they merge the union?

[auht]

If I understand correctly, it is because both $y$ are applied on the same argument $\lambda x.x$, and thus have the same return type.

[LPTK]

Wow... that seems a bit crazy. Do they keep track of equalities between terms at the type level? Or what other sorcery do they use? It sounds very expensive.

[auht]

I think they use the maximal sharing canonical forms to do the type checking, so the expression is something like

bind a = y in
bind b = x => x in
bind c = a(b) in
bind d = (c, c) in
d

Where c can be either True or False.

[LPTK]

Ah, right; I remember seeing this. Presumably, we could do the same thing, but that would probably not be worth it. Please document this as comments on the test case.