[racket] occurrence typing for case?

On Sun, May 11, 2014 at 4:10 PM, Alexander D. Knauth
<alexander at knauth.org> wrote:
> 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.
The issue is that there is a temporary variable that has the same
value as x and TR cannot see that they point to the same location.
Your implementation of case/type has the same problem. I thought there
was a bug filed for it but couldn't find it so just filed one.
http://bugs.racket-lang.org/query/?cmd=view&pr=14502

>
> 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?

Use this:
#lang typed/racket
(require typed/rackunit)

(define-syntax-rule
  (case/type y x-expr
    [t1 body ...] ...)
  (let ([y x-expr])
    (cond [((make-predicate t1) y) body ...] ...))
  )

(define (my-length x)
  (case/type y x
    [String (string-length y)]
    [(Listof Any) (length y)]
#;
    [VectorTop (vector-length y)]
    ))
(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)

There is currently an issue with generating the predicate for VectorTop.

>
> By the way why is length polymorphic?
Not sure if there is any reason, most list functions are so likely
because the original author was just writing a bunch of them at once.


>
>
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
>