core-typed 2022-10-01 | Slack Archive

Francesco Arena15:10:38

Hi everyone! I was playing with occurrence typing and something doesn't add up to me. Take the following nonsensical function:

(t/fn [x :- (t/U String Number nil)]
            (if (string? x)
              nil
              (if (number? x) 
                (str x)
                "nil")))

The type of this function can be easily inferred as [(t/U String Number nil) -> (t/U String nil) . However the inferred type of t/cf is the following:

[[(t/U Number String nil) -> (t/U String nil)
  :filters {:then (& (is (t/U Number nil) 0) (! t/Str 0)), 
            :else (is (t/U Number String) 0)}]
 {:then tt, :else ff}]

If I understand correctly, the :else proposition tells that, if the return value of the function is a false value, then we can refine the type of x to be (t/U Number String) . The problem is that the only case the function returns a false value is when x is of type String . Can anyone tell me what am I missing?

ambrosebs00:10:26

I don't think you're missing anything, except perhaps that (U Number String) is an overapproximation of String so it's technically still a correct :else proposition, but could be more useful.

2022-10-01

Channels