On Sun, May 11, 2014 at 4:10 PM, Alexander D. Knauth
<alexan...@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
>
____________________
Racket Users list:
http://lists.racket-lang.org/users
