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

On 4/1/13 11:16 AM, Robby Findler wrote:
> You could change the ellipsis to Integer. :)

Or no-check could bind ellipsis to some type.  This would be useful for 
sketching types out in no-check and then refining them to actual types 
in TR.

David


> Robby
>
>
> On Mon, Apr 1, 2013 at 8:23 AM, Eli Barzilay <eli at barzilay.org
> <mailto:eli at barzilay.org>> wrote:
>
>     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!
>     _________________________
>        Racket Developers list:
>     http://lists.racket-lang.org/dev
>
>
>
>
> _________________________
>    Racket Developers list:
>    http://lists.racket-lang.org/dev
>