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

On Tue, May 24, 2011 at 11:16 AM, Richard Lawrence
<richard.lawrence at berkeley.edu> wrote:
>
> 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?

(assert x p?) is equivalent to (if (p? x) x (error ...)) except that
the result is known to have the appropriate type (here `String').
Nothing is done at macro expansion time, and `assert' doesn't change
the typechecking of anything.  It's just a function with a particular
type.

I would rewrite your expression like this:

  (and (string? s) (string=? s "") s)

which I think is what you did, and which is how I'd write the program
in Racket as well.
-- 
sam th
samth at ccs.neu.edu