Hi everyone,
I've been starting out learning Typed Racket, which I've enjoyed quite a
lot -- thanks!
I've run into a snag several times now that I wanted to ask the experts
about: does TR know about short-circuiting `and' and `or'? (If not, why
not?) If so, how do they interact with `assert'?
Here's the example I'm working with:
#lang typed/racket
(: try-read ((U String Regexp PRegexp) Input-Port -> (U String False)))
(define (try-read re ip)
(let* ([m (regexp-try-match re ip)]
[v (and m (car m))]
[s (and v (bytes->string/utf-8 v))])
(and (assert s string?)
(not (string=? s ""))
s))) ;^ type check fails here
This example fails to type check, with the message "Expected String, but
got (U String False) in: s". I would have thought that TR would be able
to infer that, if the `(not ...)' form is reached, `s' must be a string,
due to the short-circuiting nature of `and'.
[pause for some tinkering...]
Curiously, if I change `(assert s string?)' to `(string? s)', the
example passes the type check. So I guess maybe the short-circuiting
nature of `and' and `or' is a red herring here, and what I don't
understand is something about `assert'. What makes for the difference
between `(assert s string?)' and `(string? s)'?
I thought that the difference was that `(assert s string?)' performs a
type check at macro expansion time on the type of the expression `s', in
addition to performing the dynamic check that `(string? s)' does at
runtime. But if that's right, then why doesn't the type check fail on
the `assert' form in the `and' expression, rather than on the second
form? That is, if the type of `s' is known to be (U String False) by
the time the second form is type checked, why doesn't the assertion in
the first form fail the type check?
Thanks!
Richard
_________________________________________________
For list-related administrative tasks:
http://lists.racket-lang.org/listinfo/users
