[racket] Unsafe version of require/typed?

On Fri, Mar 20, 2015 at 4:06 PM, Alexis King <lexi.lambda at gmail.com> wrote:
> The difference is that avoiding TR entirely means (1) you can’t break the soundness of other things in Typed Racket and (2) all unsafe operations need to be explicitly marked as such.
>
> Allowing people to bypass the typechecker means all unsoundness could lead to segfaults (due to the optimizer) and malicious (or just shoddy) code could actually make other TR programs that depend on them unstable.

Well, that's already the case if you use the FFI (which lots and lots
of Racket programs do).

Fundamentally the typechecker is a tool that programmers can choose to
use to make their programs better. It should not try to be more than
that.

Robby

>> On Mar 20, 2015, at 13:45, 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
>