Getting rid of nil from Option type

[Mark Feeney]

Hi there.

This is probably a noob question, but I am trying to get the type checker to recognize that a particular binding is not nil:

(t/cf

  (t/fn [[x y] :- '[String (t/Option Number)]] :- (t/U '[String] '[String Number])

    ;;(if (number? y) ;; works!

    ;;(if-not (nil? y) ;; doesn't work

    (if y ;; doesn't work

      [x y]

      [x])))

Type Error (:30:5) Type mismatch:

Expected:       (t/U (t/HVec [String]) (t/HVec [String Number]))

Actual:         (t/HVec [String (t/U nil Number)])

in: [x y]

This is a simplification of a more complex case where I don't have a function like number? available.

Is there a way to prove to the checker that something is definitely not nil? (or a better overall approach I should look at)

Thanks!

Mark

[Ambrose Bonnaire-Sergeant]

That would be a bug in the let-aliasing implementation.

Please make a JIRA issue.

Thanks,

Ambrose

[Ambrose Bonnaire-Sergeant]

Actually, looks like a problem with updating HVec's. This fails too, thinks it can return nil:

(fn [v :- '[(U nil Num)]] :- Num

  (if (first v)

    (first v)

    1))

[Mark Feeney]

Hi Ambrose.

Created http://dev.clojure.org/jira/browse/CTYP-232 (sorry for the awful formatting, couldn't figure out how to edit in JIRA)

Thanks for your very quick reply on this, and for all your work on core.typed.  It's a really cool system and I think an important project.  

Let me know if there's anything I can do to help with this issue.

[Mark Feeney]

Also, can you (or anyone) think of a work-around for this, or will I have to :no-check?

Thanks,

Mark

[Ambrose Bonnaire-Sergeant]

Perhaps try an inline assertion or cast via t/pred.

[Mark Feeney]

FWIW I've found a work-around using let/ann-form.  It requires repeated annotations, but it's something.

(t/fn [v :- '[(t/U nil t/Num)]] :- t/Num

  (t/let [v' :- (t/U nil t/Num) (first v)]

    (if v'

      v'

      1)))

[Ambrose Bonnaire-Sergeant]

Yes that makes sense. The relationship between v and v' is lost with an ann-form.

Thanks,

Ambrose