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 <ro...@eecs.northwestern.edu> wrote: > On Fri, Mar 20, 2015 at 4:06 PM, Alexis King <lexi.lam...@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 <ro...@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.lam...@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 <hend...@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
