[racket] help with typed racket function?

Two minutes ago, Danny Yoo wrote:
> I'm trying to make a function that can discriminate typed boxes: I
> tried the following in Typed Racket:
> 
> (: ensure-number-box (Any -> (Boxof Number)))
> (define (ensure-number-box x)
>   (if (and (box? x) (number? (unbox x)))
>       x
>       (error 'ensure-number-box "~s" x)))
> 
> Unfortunately, I can't convince the type checker that x is a (Boxof
> number).  I'm not quite sure how to use the occurrence typing
> properly to get this to type correctly.

You can't.  Here's something I wrote for my class, and revised it just
last week, so it might have some bugs:

The lack of any subtype relations between (Boxof T) and (Boxof S)
regardless of S and T can roughly be explained as follows.

First, a box is a container that you can pull a value out of -- which
makes it similar to lists.  In the case of lists, we have:

    if:           S   subtype-of          T
    then: (Listof S)  subtype-of  (Listof T)

This is true for all such containers that you can pull a value out of:
if you expect to pull a T but is given a container of a subtype S, then
things are still fine.  Such "containers" include functions that produce
a value -- for example:

    if:         S  subtype-of       T
    then:  Q -> S  subtype-of  Q -> T

However, functions also have the other side, where things are different
-- instead of a side of some *produced* value, it's the side of the
*consumed* value.  There, we get the opposite rule:

    if:    T       subtype-of  S
    then:  S -> Q  subtype-of  T -> Q

To see why this is right, use `Number' and `Integer' for S and T:

    if:    Integer      subtype-of  Number
    then:  Number -> Q  subtype-of  Integer -> Q

so -- if you expect a function that takes a number is a *subtype* of one
that takes an integer; in other words, every function that takes a
number is also a function that takes an integer, but not the other way.

Now, a (Boxof T) is a producer of T when you pull a value out of the
box, but it's also a consumer of T when you put such a value in it.
This means that -- using the above analogy -- the T is on both sides of
the arrow.  This means that

    if:    S subtype-of T  *and*  T subtype-of S
    then:  (Boxof S) subtype-of (Boxof T)

which is actually:

    if:           S   is-the-same-type-as         T
    then:  (Boxof S)  is-the-same-type-as  (Boxof T)

A different way to look at this conclusion is to consider the function
type of (A -> A): when is it a subtype of some other (B -> B)?  Only
when A is a subtype of B and B is a subtype of A, which means that this
happens only when A and B are the same type.

(Side note: this is related to the fact that in logic, `P => Q' is
roughly equivalent to `not(P) or Q' -- so the left side, `P', is inside
a negation.  It also explains why in ((S -> T) -> Q) the S obeys the
first rule, as if it was on the right side -- because it's negated
twice.)

The following piece of code makes the analogy to function types more
formally.  Boxes behave as if their contents is on both sides of a
function arrow -- on the right because they're readable, and on the left
because they're writeable, which the conclusion that a (Boxof A) type is
a subtype of itself and no other (Boxof B).

  #lang pl

  ;; a type for a "read-only" box
  (define-type (Boxof/R A) = (-> A))
  ;; Boxof/R constructor
  (: box/r : (All (A) (A -> (Boxof/R A))))
  (define (box/r x) (lambda () x))
  ;; we can see that (Boxof/R T1) is a subtype of (Boxof/R T2) if T1 is
  ;; a subtype of T2 (this is not surprising, since these boxes are
  ;; similar to any other container, like lists):
  (: foo1 : Integer -> (Boxof/R Integer))
  (define (foo1 b) (box/r b))
  (: bar1 : (Boxof/R Number) -> Number)
  (define (bar1 b) (b))
  (test (bar1 (foo1 123)) => 123)

  ;; a type for a "write-only" box
  (define-type (Boxof/W A) = (A -> Void))
  ;; Boxof/W constructor
  (: box/w : (All (A) (A -> (Boxof/W A))))
  (define (box/w x) (lambda (new) (set! x new)))
  ;; in contrast to the above, (Boxof/W T1) is a subtype of (Boxof/W T2)
  ;; if T2 is a subtype of T1, *not* the other way (and note how this is
  ;; related to A being on the *left* side of the arrow in the `Boxof/W'
  ;; type):
  (: foo2 : Number -> (Boxof/W Number))
  (define (foo2 b) (box/w b))
  (: bar2 : (Boxof/W Integer) Integer -> Void)
  (define (bar2 b new) (b new))
  (test (bar2 (foo2 123) 456))

  ;; combining the above two into a type for a "read/write" box
  (define-type (Boxof/RW A) = (A -> A))
  ;; Boxof/RW constructor
  (: box/rw : (All (A) (A -> (Boxof/RW A))))
  (define (box/rw x) (lambda (new) (let ([old x]) (set! x new) old)))
  ;; this combines the above two: `A' appears on both sides of the
  ;; arrow, so (Boxof/RW T1) is a subtype of (Boxof/RW T2) if T1 is a
  ;; subtype of T2 (because there's an A on the right) *and* if T2 is a
  ;; subtype of T1 (because there's another A on the left) -- and that
  ;; can happen only when T1 and T2 are the same type.  So this a type
  ;; error:
  ;;   (: foo3 : Integer -> (Boxof/RW Integer))
  ;;   (define (foo3 b) (box/rw b))
  ;;   (: bar3 : (Boxof/RW Number) Number -> Number)
  ;;   (define (bar3 b new) (b new))
  ;;   (test (bar3 (foo3 123) 456) => 123)
  ;;   ** Expected (Number -> Number), but got (Integer -> Integer)
  ;; And this a type error too:
  ;;   (: foo3 : Number -> (Boxof/RW Number))
  ;;   (define (foo3 b) (box/rw b))
  ;;   (: bar3 : (Boxof/RW Integer) Integer -> Integer)
  ;;   (define (bar3 b new) (b new))
  ;;   (test (bar3 (foo3 123) 456) => 123)
  ;;   ** Expected (Integer -> Integer), but got (Number -> Number)
  ;; The two types must be the same for this to work:
  (: foo3 : Integer -> (Boxof/RW Integer))
  (define (foo3 b) (box/rw b))
  (: bar3 : (Boxof/RW Integer) Integer -> Integer)
  (define (bar3 b new) (b new))
  (test (bar3 (foo3 123) 456) => 123)

-- 
          ((lambda (x) (x x)) (lambda (x) (x x)))          Eli Barzilay:
                    http://barzilay.org/                   Maze is Life!