[racket] Unsafe version of require/typed?

From: Alexander D. Knauth (alexander at knauth.org)
Date: Sat Mar 21 09:46:49 EDT 2015

If you look here at typed/syntax/stx.rkt:
https://github.com/racket/typed-racket/blob/master/typed-racket-more/typed/syntax/stx.rkt
You’ll see something that looks sort of similar to an unsafe require/typed.

But if you look here: 
https://github.com/plt/racket/blob/f3dba3eb6bf44685cb2290d48204e81a84fc09a6/pkgs/typed-racket-pkgs/typed-racket-more/typed/syntax/stx.rkt
And at the history here:
https://github.com/plt/racket/commits/f3dba3eb6bf44685cb2290d48204e81a84fc09a6/pkgs/typed-racket-pkgs/typed-racket-more/typed/syntax/stx.rkt
And here:
http://bugs.racket-lang.org/query/?debug=&database=default&cmd=view+audit-trail&cmd=view&pr=14561

Because of some confusion about whether (Syntaxof t) represented a syntax object with a syntax->datum result of t or one with a syntax-e result of t, there were wrong types for syntax-objects, syntax-e, stx->list, stx-car, etc. (inconsistent with each other)

And because they didn’t use contracts, bugs like these stay there for a lot longer than they would if there were contracts guarding them.  

And it’s not like the people who made this were “new users.”  
But I think it’s just that easy to introduce bugs like this when things aren’t guarded by contracts, even for very experienced programmers.


On Mar 20, 2015, at 4:45 PM, Robby Findler <robby at eecs.northwestern.edu> wrote:

> I think we should think the best of our users and not assume that we
> know better than they do about what they need to do their work.
> 
> In this particular case, they can always opt out of tr entirely, lets
> not forget.
> 
> Robby
> 
> On Fri, Mar 20, 2015 at 3:41 PM, Alexis King <lexi.lambda at gmail.com> wrote:
>> This has been discussed before, and I think it’s a good idea, but I also think any such feature should be well-hidden. I’m sure that new users would use it frequently just to make the typechecker “shut up” when really their programs are unsound.
>> 
>>> On Mar 20, 2015, at 12:30, Hendrik Boom <hendrik at topoi.pooq.com> wrote:
>>> 
>>> On Fri, Mar 20, 2015 at 03:20:38PM -0400, Eric Dong wrote:
>>>> It would be nice if we could have an unsafe version of require/typed, which
>>>> doesn't generate a contract, but simply "lies" to the type system about the
>>>> type. This, of course, breaks the type system's guarantees, and causes UB
>>>> if optimizations are one, but in some cases contracts cannot be generated
>>>> (for example, for the "object-name" function), but one can create a safe
>>>> type for it.
>>>> 
>>>> Why can't there be a "require/typed/unsafe" form? It could save a lot of
>>>> unnecessary asserts and casts, and unnecessary contract overhead.
>>> 
>>> Perhaps this model can provide guidance:
>>> 
>>> If I recall correctly, Modula 3, another garbage-collected, strongly
>>> typed language, has unsafe interfaces and, separately, unsafe
>>> implementations.
>>> 
>>> You can implement a safe (i.e., ordinary) interface with an unsafe
>>> implementation.  This means that it is the implementer's
>>> (not  the compiler's) responsibility to make sure that the the module
>>> will perform all necessary run-time checks to make sure that it can
>>> only be used safely, but the implementation can use unsafe language
>>> features.
>>> 
>>> An unsafe interface, on the other hand, can only be used in an unsafe
>>> implementation.
>>> 
>>> -- hendrik
>>> ____________________
>>> Racket Users list:
>>> http://lists.racket-lang.org/users
>> 
>> 
>> ____________________
>>  Racket Users list:
>>  http://lists.racket-lang.org/users
> 
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users



Posted on the users mailing list.