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
{{update}} (link: https://github.com/clojure/core.typed/blob/master/module-check/src/main/clojure/clojure/core/typed/update.clj#L308-L315 text: ignores propositions) that update non-HMap types.
So in the test position, {{m}} is still of type {{(Map Any Str)}}, which means (link: https://github.com/clojure/core.typed/blob/master/module-check/src/main/clojure/clojure/core/typed/path_type.clj#L71-L72 text: 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 (link: https://github.com/clojure/core.typed/blob/master/module-check/src/main/clojure/clojure/core/typed/update.clj#L308-L315 text: 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.
More information
Discussion here: https://groups.google.com/d/msg/clojure-core-typed/WO8dpY63N2Q/7UWBViNiIYEJ
{{git bisect}} code
(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 [email protected]
Date: Sat Jan 3 00:05:23 2015 +0000
enable aliasing support
Pull request:
-(link: https://github.com/typedclojure/core.typed/pull/26 text: CTYP-241)-
(link: https://github.com/typedclojure/core.typed/pull/42 text: Rebased)
* Waiting on
* (link: http://dev.clojure.org/jira/browse/CTYP-255 text: CTYP-255)
Patch:
Commmit:
Release:
