[racket] `assert', `and' and `or' in Typed Racket

From: Richard Lawrence (richard.lawrence at berkeley.edu)
Date: Tue May 24 14:16:37 EDT 2011

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







Posted on the users mailing list.