[racket] Unsafe version of require/typed?

From: Alexis King (lexi.lambda at gmail.com)
Date: Fri Mar 20 16:41:05 EDT 2015

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



Posted on the users mailing list.