[racket-dev] Purpose of typed/racket/no-check

From: Eli Barzilay (eli at barzilay.org)
Date: Mon Apr 1 09:23:08 EDT 2013

20 minutes ago, Matthias Felleisen wrote:
> 
> On Mar 31, 2013, at 9:32 PM, Sam Tobin-Hochstadt wrote:
> 
> > My expectation when using typed/racket/no-check is that I won't
> > get any type errors.
> 
> To me, the words "no check" mean just that: do not type-check the
> module. But I think it is okay to parse the types. I doubt people
> use this option when they wish to avoid a parse error in the type
> expressions.

As a semi-random data point, I sometime use my no-check language
(which is built on top of TR's) to show how things work in class
without getting all the types right (or when there's some problem with
the types).  In these cases I sometime use bogus type declarations
like "(All (A B) ...)", which IIUC wouldn't work anymore.  It's just
technically simpler and clearer to still use `:' instead of going back
to comments.  (But it's obviously a weak point.)

-- 
          ((lambda (x) (x x)) (lambda (x) (x x)))          Eli Barzilay:
                    http://barzilay.org/                   Maze is Life!

Posted on the dev mailing list.