Uploaded image for project: 'core.typed'
  1. CTYP-241

Let-aliased variables of plain Map lookups should update original map




      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 ignores 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)).


      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.

      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 <...@gmail.com>
      Date: Sat Jan 3 00:05:23 2015 +0000

      enable aliasing support

      Pull request:





            • Assignee:
              overthink Mark Feeney
            • Votes:
              0 Vote for this issue
              0 Start watching this issue


              • Created: