[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!