How to use union types?

Questions & Answers
1

If I try

(: foo (-> (U Positive-Exact-Rational Negative-Exact-Rational) Positive-Exact-Rational
           (U Positive-Exact-Rational Negative-Exact-Rational)))
(define (foo a b) (* a b))

I get type mismatch.

But both

(: foo (-> Positive-Exact-Rational Positive-Exact-Rational
           (U Positive-Exact-Rational Negative-Exact-Rational)))
(define (foo a b) (* a b))

and

(: foo (-> Negative-Exact-Rational Positive-Exact-Rational
           (U Positive-Exact-Rational Negative-Exact-Rational)))
(define (foo a b) (* a b))

checked fine.

Is it a bug in checker, or should I somehow tell it to union the types for *?

2

The existing type of * does not include your desired combination:

> (:query-type/result * (U Positive-Exact-Rational Negative-Exact-Rational))
(case->
 (-> Negative-Exact-Rational  Negative-Exact-Rational   Negative-Exact-Rational   Negative-Exact-Rational)
 (-> Positive-Exact-Rational Negative-Exact-Rational Negative-Exact-Rational)
 (-> Negative-Exact-Rational Positive-Exact-Rational Negative-Exact-Rational)
 (-> Negative-Exact-Rational Negative-Exact-Rational Positive-Exact-Rational)
 (-> Negative-Exact-Rational Negative-Exact-Rational)
 (-> Positive-Exact-Rational * Positive-Exact-Rational))

Conjecture: Our * may yield a variant of ‘zero (according to the type checker). And indeed, if you add Zero to the result type of your first expression, the checker verifies the theorem:

#lang typed/racket

(: foo (-> (U Positive-Exact-Rational Negative-Exact-Rational) Positive-Exact-Rational
           (U Positive-Exact-Rational Negative-Exact-Rational Zero)))
(define (foo a b) (* a b))

(To someone who knows numerics well: Is it possible that multiplying two numbers of the given type yields something close to 0 with exact rationales? My reasoning says ‘no’ and we could change the type of * to include the desired outcome.)

3

It has

(-> Negative-Exact-Rational Positive-Exact-Rational Negative-Exact-Rational)

and

(-> Positive-Exact-Rational * Positive-Exact-Rational)

So last can be specified to

(-> Positive-Exact-Rational Positive-Exact-Rational Positive-Exact-Rational)

From

(-> Negative-Exact-Rational Positive-Exact-Rational Negative-Exact-Rational)
(-> Positive-Exact-Rational Positive-Exact-Rational Positive-Exact-Rational)

one can derive, that

(-> (U Negative-Exact-Rational Positive-Exact-Rational) Positive-Exact-Rational 
      (U Negative-Exact-Rational Positive-Exact-Rational ))
4

This works:

(: foo (-> (U Positive-Exact-Rational Negative-Exact-Rational) Positive-Exact-Rational
           (U Positive-Exact-Rational Negative-Exact-Rational)))
(define (foo a b) 
  (if (> a 0)
      (* a b)
      (* a b)))

But excessive conditional looks very ugly...

1 Like
5

This works too

(: foo (-> (U Positive-Exact-Rational Negative-Exact-Rational) (U Positive-Exact-Rational Negative-Exact-Rational)
           (U Positive-Exact-Rational Negative-Exact-Rational)))
(define (foo a b) 
  (if (> a 0)
      (if (> b 0)
          (* a b)
          (* a b))
      (if (> b 0)
          (* a b)
          (* a b))))
1 Like
6

Zero in PLs are weird:

(: x (U Positive-Exact-Rational Negative-Exact-Rational))
(define x 0)