[racket] Unsafe version of require/typed?

From: Eric Dong (yd2dong at uwaterloo.ca)
Date: Sat Mar 21 11:55:56 EDT 2015

As far as I know, yes.

On Sat, Mar 21, 2015 at 11:02 AM, Robby Findler <robby at eecs.northwestern.edu
> wrote:

> Re-reading this, just to clarify: the only time when the optimizer
> could cause problems is when the contracts would have signaled an
> error, right? So, in other words, the difference between the fx+ from
> racket/base and the unsafe-fx+ from racket/unsafe/ops is exactly the
> same difference as using (require/typed ...) and (require/typed/unsafe
> ...).
>
> Robby
>
>
> On Fri, Mar 20, 2015 at 4:10 PM, Robby Findler
> <robby at eecs.northwestern.edu> wrote:
> > 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
> >>
>
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20150321/6743f002/attachment.html>

Posted on the users mailing list.