core.typed

Propositional subtyping should consider the lexical type environment

Details

Description

Problem

Subtyping between propositions could be improved, especially when mixing positive and
negative type propositions.

Take the following function.

; Type Error (clojure/core/typed/test/core.clj:1293:14) Expected result with filter {:then (is Number a__#0), :else tt}, ; got filter {:then (! (t/U nil false) a__#0), :else (is (t/U nil false) a__#0)}
; in: a              |
;                    v
    (is-tc-e (fn [a] a)
             [(U nil Number) -> Any :filters {:then (is Number 0)}])

The subtyping test for the {then} proposition fails because

(! (U nil false) a)

is not a subtype of

(is Number a)

However in the context of the current lexical environment,

{a (U nil Number)}

combined with the actual then proposition

(! (U nil false) a)

implies

(is Number a)
.

Approach

Every {FilterSet} should also carry the {PropEnv} in which it was created. (We should take care that this
environment is substituted properly when we eg. substitute function parameters for de Bruijn indices).

Then we can check to see if the contained environment for the actual proposition set satisfies the
supertype proposition.

Test case:

(is-tc-e (fn [a] a)
             [(U nil Number) -> Any :filters {:then (is Number 0)}])

Notes

This test case should pass: let-filter-unscoping-test.

Code review:
Patch:

Activity

Hide
Ambrose Bonnaire-Sergeant added a comment -

Very vague, would require something like refinement types which is a huge job.

Show
Ambrose Bonnaire-Sergeant added a comment - Very vague, would require something like refinement types which is a huge job.

People

Vote (0)
Watch (0)

Dates

  • Created:
    Updated:
    Resolved: