Let-aliased variables of plain Map lookups should update original map
Key details
Description
Problem
Let-aliasing means we completely rely on the original binding's type to find the type for locals derived from lookups on it. If occurrence typing doesn't update the original binding, then even very simple control flow does not register.
For example, in core.typed 0.3.7, the following code registers e as an alias of (Key :foo)m.
(fn [m :- (Map Any Str)] :- String
(let [e (:foo m)]
(if e e "asdf")))
;; ^
;; Expected Str, actual (U nil Str)
e contains the correct propositions and object, however updateignores propositions that update non-HMap types.
So in the test position, m is still of type (Map Any Str), which means path-type infers Any for its aliased object (above). (Note: path-type should infer slightly better types here, eg., this should return (U nil Str)).
Solution
The update case for keyword invocations on non-HMaps need to intersect its known HMap type.
We now make it an error to assign an object to the result of looking up a possibly-mutable map. ie.,
(fn [a :- Any] (:foo a))
has no object.
Correspondingly, update will throw an error if told to update via a keyword lookup on a map type that is not a subtype of (U nil (Map Any Any)).
We cannot have objects that might be wrong — the formalism asserts that in
G |- e : t ; v+ | v- ; o}}, where G |- p and p |- e || v, that o = empty, or p(o) = v.
That means looking up an object o of an expression e must always result in exactly its evaluation v. If we gave an object to
(fn [a :- Any] (:foo a))
that means two invocations of
((fn [a :- Any] (:foo a)) m)
must return exactly the same value — for a mutable m this is clearly false.
Interestingly, this has worked fine in practice until let-aliasing, by compensating in the update function. We basically only update types that are immutable, checked at the last minute in update.
Briefly, to handle this idea of "temporarily fake" objects, we probably need a predicate to validate whether an object should be taken "seriously" as an actual, immutable, path. Then the formalism might read:
G |- e : t ; v+ | v- ; o}}, where G |- p and p |- e || v, that o = empty, or if serious(o) then p(o) = v.
9608027bfaf4be268cfa12486c5ae6615d8517f1 is the first bad commit commit 9608027bfaf4be268cfa12486c5ae6615d8517f1 Author: Ambrose Bonnaire-Sergeant <...@gmail.com> Date: Sat Jan 3 00:05:23 2015 +0000
Blocker
Problem
Let-aliasing means we completely rely on the original binding's
type to find the type for locals derived from lookups on it. If
occurrence typing doesn't update the original binding, then even
very simple control flow does not register.
For example, in core.typed 0.3.7, the following code registers
eas an alias of(Key :foo)m.(fn [m :- (Map Any Str)] :- String (let [e (:foo m)] (if e e "asdf"))) ;; ^ ;; Expected Str, actual (U nil Str)econtains the correct propositions and object, howeverupdateignores propositions that update non-HMap types.So in the test position,
mis still of type(Map Any Str), which means path-typeinfers
Anyfor its aliased object (above). (Note:path-typeshould infer slightly bettertypes here, eg., this should return
(U nil Str)).Solution
The update case for keyword invocations on non-HMaps
need to intersect its known HMap type.
We now make it an error to assign an object to the result of looking up
a possibly-mutable map. ie.,
(fn [a :- Any] (:foo a))has no object.
Correspondingly,
updatewill throw an error if told to update via a keyword lookupon a map type that is not a subtype of
(U nil (Map Any Any)).We cannot have objects that might be wrong — the formalism asserts that in
G |- e : t ; v+ | v- ; o}}, where G |- p and p |- e || v, that o = empty, or p(o) = v.That means looking up an object
oof an expressionemust alwaysresult in exactly its evaluation
v. If we gave an object to(fn [a :- Any] (:foo a))that means two invocations of
((fn [a :- Any] (:foo a)) m)must return exactly the same value — for a mutable
mthis is clearly false.Interestingly, this has worked fine in practice until let-aliasing, by compensating
in the
updatefunction. We basically only update types that are immutable, checkedat the last minute in
update.Briefly, to handle this idea of "temporarily fake" objects, we probably need a predicate to validate
whether an object should be taken "seriously" as an actual, immutable, path. Then the formalism
might read:
G |- e : t ; v+ | v- ; o}}, where G |- p and p |- e || v, that o = empty, or if serious(o) then p(o) = v.More information
Discussion here: https://groups.google.com/d/msg/clojure-core-typed/WO8dpY63N2Q/7UWBViNiIYEJ
git bisectcode(do (require '[clojure.core.typed :as t]) (t/cf (t/fn [m :- (t/Map t/Kw String)] :- String (or (:foo m) "asdf"))))This stopped type checking after https://github.com/clojure/core.typed/commit/9608027bfaf4be268cfa12486c5ae6615d8517f1
bisect result:
9608027bfaf4be268cfa12486c5ae6615d8517f1 is the first bad commit
commit 9608027bfaf4be268cfa12486c5ae6615d8517f1
Author: Ambrose Bonnaire-Sergeant <...@gmail.com>
Date: Sat Jan 3 00:05:23 2015 +0000
enable aliasing support
Pull request:
CTYP-241
Rebased
Waiting on
CTYP-255
Patch:
Commmit:
Release: