It seems like case doesn’t do occurrence typing, when it seems like it would be
easiest for case, because of singleton types.
For example:
#lang typed/racket
(define (f x)
(case x
[(thing) (g x)]
))
(: g ('thing -> 'thing))
(define (g x) x)
Gives me this:
. Type Checker: type mismatch
expected: 'thing
given: Any in: x
This isn’t much of a problem (I can easily just do a cast), but It just seems
like it should be really easy for typed racket to figure out that x has the
type ‘thing if it gets into that clause.
By the way is there something like case/type that would be something like this?:
(case/type x
[Type-1 body …]
[Type-2 body …]
…
)
And would use (make-predicate Type) to do it so that it would do occurrence
typing? Maybe something like this:
(define-syntax-rule
(case/type x-expr
[t body …] …)
(let ([x x-expr])
(cond [((make-predicate t) x) body …] …))
)
I tried it, but it didn’t work like I expected it to do with occurrence typing:
#lang typed/racket
(require typed/rackunit)
(define-syntax-rule
(case/type x-expr
[t1 body ...] ...)
(let ([x x-expr])
(cond [((make-predicate t1) x) body ...] ...))
)
(define (my-length x)
(case/type x
[String (string-length x)]
[(Listof Any) ((inst length Any) x)]
[VectorTop (vector-length x)]
))
(check-equal? (my-length "12345") 5)
(check-equal? (my-length '(1 2 3 4 5)) 5)
(check-equal? (my-length #(1 2 3 4 5)) 5)
It gave me these errors:
. Type Checker: type mismatch
expected: String
given: Any in: x
. Type Checker: type mismatch
expected: (Listof Any)
given: Any in: x
. Type Checker: type mismatch
expected: VectorTop
given: Any in: x
So I guess it didn’t do occurrence typing for that either, even though it uses
make-predicate. Is there anything I can do to help it do occurrence typing for
this?
By the way why is length polymorphic?
____________________
Racket Users list:
http://lists.racket-lang.org/users
