Re: [racket-dev] Purpose of typed/racket/no-check
An hour and a half ago, David Van Horn wrote: > On 4/1/13 11:16 AM, Robby Findler wrote: > > You could change the ellipsis to Integer. :) The time that I'd spend explaining why I wrote `Integer' makes the comment route more appealing... > 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. Well, I used "..." in the natural sense of "some stuff". Having it bound to some type sounds cute, but definitely too much work than it's worth. (At least IMO.) -- ((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
Re: [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 mailto:e...@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 _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Purpose of typed/racket/no-check
You could change the ellipsis to Integer. :) Robby On Mon, Apr 1, 2013 at 8:23 AM, Eli Barzilay 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
Re: [racket-dev] Purpose of typed/racket/no-check
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
Re: [racket-dev] Purpose of typed/racket/no-check
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. > While `define-predicate` can't work in that sense, > we could just make `cast` always succeed, which I think would be > helpful. > > I only use no-check to take a file that won't typecheck due to some > problem I hope to fix, and just run it. I think what you're > suggesting would reduce its usefulness for some of those cases, and > increase it in others. > > On Sun, Mar 31, 2013 at 5:44 PM, Eric Dobson wrote: >> There have been a couple recent bug reports because certain features >> need a type, such as cast and define-predicate. >> >> I was wondering whether TR/no-check should check that the types are >> well formed, but not check that the expressions are well typed? I'm >> thinking this would be less surprising to users, but wondering whether >> users would expect that type definition errors to still work in >> TR/no-check. >> _ >> Racket Developers list: >> http://lists.racket-lang.org/dev > _ > Racket Developers list: > http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Purpose of typed/racket/no-check
My expectation when using typed/racket/no-check is that I won't get any type errors. While `define-predicate` can't work in that sense, we could just make `cast` always succeed, which I think would be helpful. I only use no-check to take a file that won't typecheck due to some problem I hope to fix, and just run it. I think what you're suggesting would reduce its usefulness for some of those cases, and increase it in others. On Sun, Mar 31, 2013 at 5:44 PM, Eric Dobson wrote: > There have been a couple recent bug reports because certain features > need a type, such as cast and define-predicate. > > I was wondering whether TR/no-check should check that the types are > well formed, but not check that the expressions are well typed? I'm > thinking this would be less surprising to users, but wondering whether > users would expect that type definition errors to still work in > TR/no-check. > _ > Racket Developers list: > http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Purpose of typed/racket/no-check
I have proposed that before and I support it. Please do it! On Mar 31, 2013, at 5:44 PM, Eric Dobson wrote: > There have been a couple recent bug reports because certain features > need a type, such as cast and define-predicate. > > I was wondering whether TR/no-check should check that the types are > well formed, but not check that the expressions are well typed? I'm > thinking this would be less surprising to users, but wondering whether > users would expect that type definition errors to still work in > TR/no-check. > _ > Racket Developers list: > http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
