Re: [racket] Unsafe version of require/typed?

[Vincent St-Amour]

At Fri, 20 Mar 2015 16:10:45 -0500,
Robby Findler wrote:
> 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.

I agree 200%.


On the more general topic of unsafe modes for TR:

I agree that we need these kinds of escape hatches. There's a number of
possible designs: `unsafe-require/typed`, `#lang typed/racket/unsafe`,
`unsafe-provide` (provides unsafe version only), `provide/unsafe`
(provides both safe and unsafe versions).

Then there's the possibility of turning off the optimizer (makes most
sense for the `#lang` design), which would compromise by avoiding
contracts, but remain as safe as `#lang racket`. There's already a way
to turn off the optimizer (`#:no-optimize`), so that may be redundant.

Any thoughts?

Vincent

[Robby Findler]

I also struggle with this in the context of the contract system in
general, when it isn't being used for TR/R interop. We have option
contracts, and I think they are a piece of the puzzle but we need
something that's a bit more built-in somehow. Perhaps we can find a
way to make these pieces all work together.

Robby

[Matthias Felleisen]

On Mar 23, 2015, at 1:37 PM, Vincent St-Amour <stam...@ccs.neu.edu> wrote:

> At Fri, 20 Mar 2015 16:10:45 -0500,
> Robby Findler wrote:
>> 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.
>
> I agree 200%.

This statement is so general that everyone can agree to it, including C++ hackers. So I agree with it at the 300% level? Anyone wants to bid me higher? :-)

More when I have time to catch up with last week's email -- Matthias

>
>
> On the more general topic of unsafe modes for TR:
>
> I agree that we need these kinds of escape hatches. There's a number of
> possible designs: `unsafe-require/typed`, `#lang typed/racket/unsafe`,
> `unsafe-provide` (provides unsafe version only), `provide/unsafe`
> (provides both safe and unsafe versions).
>
> Then there's the possibility of turning off the optimizer (makes most
> sense for the `#lang` design), which would compromise by avoiding
> contracts, but remain as safe as `#lang racket`. There's already a way
> to turn off the optimizer (`#:no-optimize`), so that may be redundant.
>
> Any thoughts?
>
> Vincent
>

> --
> You received this message because you are subscribed to the Google Groups "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Matthias Felleisen]

On Mar 20, 2015, at 5:10 PM, Robby Findler <ro...@eecs.northwestern.edu> wrote:

> 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.

I think these statements paint an image in broad brushstrokes that
some people appreciate properly and some don't.

Yes, ffi/unsafe makes Racket programs unsafe. They may introduce
causes for segfaults beyond the Racket engine itself. That's not
a good thing but ffi/unsafe suggests this problem by its name and
I think we try to stick this to a layer where we know it's potentially
problematic.

Otherwise the goal is to smother the unsafety of the existing software
infrastructure. If we don't have such a minimal goal, why bother with
Racket (at least from a research perspective)?

;; ----------------------------------------------------------------------

On Mar 23, 2015, at 1:37 PM, Vincent St-Amour <stam...@ccs.neu.edu> wrote:

> Then there's the possibility of turning off the optimizer (makes most
> sense for the `#lang` design), which would compromise by avoiding
> contracts, but remain as safe as `#lang racket`. There's already a way
> to turn off the optimizer (`#:no-optimize`), so that may be redundant.

This is an acceptable and pragmatic alternative. It gives the programmer
some of the advantages of types (checking, documentation, hooks for tools).
And it does not lower the level of safety that Racket aims for.

On a more general note: It also exposes the Reynolds insight that types
are an inherent part of the meaning (static). As such, compiling uses of
first in

(: f (-> [List X Y Z] X))

to not check the listness of the argument is intrinsic to __compilation__,
not __optimization__. I think the strict use of this guideline would establish
another point in our language spectrum.


-- Matthias

[Robby Findler]

Just to be sure we are on the same page, my comments were in the
context of push back that came for reasons that are unclear to me, but
I think had something to do with the thought that we shouldn't
compromise the type system. My comments were meant to be in that
context, trying to point out what the real value of a type system is;
that is, to give a judgment we can use as a basis for design decisions
here.

As for smothering: the cost of contracts is "observable enough" (you
know what I mean) that we cannot just ignore it, as I'm sure you
agree. And since we do not have an acceptable solution we should
explore generalizing our support for unsafe operations that we already
have. It seems to fit very naturally to think of parallel libraries,
the safe and the unsafe version.

I also like Vincent's idea about coupling the optimizer to the
contracts as a point worth pragmatic exploration. We shouldn't kid
ourselves, however, it is still unsafe and programs that turn it on
can behave in arbitrarily weird ways (when an error is skipped over).

Robby

[michael.ballantyne]

I've started using Typed Racket several times recently only to flip the switch to #lang typed/racket/no-check or remove types entirely. Something like Vincent suggests with an option to write with types and have them checked but turn off the type-driven optimizer and skip contract checking at typed/untyped boundaries would be fantastic.

Having the option to flip this switch either from the code doing the requiring or at package installation time seems important, regardless of whether the author of the typed code wrote with that in mind. When I wanted to use the tr-pfds package from untyped code I had to modify it to use #lang typed/racket/no-check because the performance hit of contract checks was massive.

A raco option to compile and install a package without Typed Racket optimizations or contracts might be another piece of the solution.

[Matthias Felleisen]

What I'd much prefer at the moment over speculative solutions are reports of actual performance bottlenecks. -- Matthias

[Neil Toronto]

Your preferences are my command. :)


**** Actual Performance Bottlenecks (and Workarounds) ****


(1) Plot's sending of `snip%` instances from untyped to typed code made
them so slow that they were unresponsive. I got around it by making
helper functions to create the snips, and inserting their types directly
into the base type environment using the
`typed-racket/base-env/extra-env-lang` language. (See
"plot-gui-lib/plot/private/gui/lazy-snip-typed.rkt".)

(2) Again in Plot, I needed to give types to `dc` (from `pict`), and
helper functions to create `pdf-dc%`, etc., instances. To keep rendering
plots using those targets from taking $MANY MB memory each (I think it
was in the range 7-14 MB), I inserted the helper functions' types
directly into the base type environment. (See
"plot-lib/plot/private/no-gui/evil.rkt".)

(3) In Pict3D, see "pict3d/private/gui/pict3d-bitmap.rkt" and
"pict3d/private/gui/pict3d-canvas.rkt" for more examples of the same.
Using `require/typed` would have forced me to favor either typed or
untyped use of Pict3D for rendering on canvases and bitmaps. Using
`extra-env-lang` is a little dangerous, but favors both.

(4) Again in Pict3D: Racket's FFI doesn't have a typed interface, so I
wrote a subset of it using the `extra-env-lang` language. I couldn't
have used `require/typed` because `memcpy` and similar functions have
cases that can't be distinguished by arity.

(5) I did the same for OpenGL. I could have used `require/typed`, but
speed tests showed I would get at most 5000 OpenGL calls per 60Hz frame
that way, which is too few to do anything serious. Using
`extra-env-lang` to insert the types into the base type environment, the
upper bound is around 60000 OpenGL calls per frame, which is plenty.

(6) Anything polymorphic takes a lot of time to cross the boundary,
especially if it's higher-order. One higher-order example is using
`math/array` from untyped code: operations on newly created arrays take
over 50x the time they do in typed code. Jens Axel and Ryan Culpepper
have worked around it by wrapping matrices (which are arrays) with
something like

(struct matrix ([value : (Matrix Real)]) #:transparent)

or some concrete type other than `Real`. Then they create wrapper
functions for `math/matrix` exports. The `matrix?` contract is O(1), so
`matrix` instances cross over cheaply.

(7) Untyped Pict3D users wouldn't tolerate a deep check of all shapes in
a scene every time it crosses the contract boundary. (Complex scenes
have thousands of shapes, and scenes cross over a lot.) But I also want
users to eventually be able to extend Pict3D with new kinds of shapes.
So scene functions that with polymorphism would look like this:

(: add-shape (All (A) (-> (Scene A) A (Scene A))))

look like this instead:

(: add-shape (-> Scene Shape Scene))

where `Shape` is a struct type that new shapes must inherit from.


**** General Observations ****


(A) The contract boundary makes objects very slow and very memory-heavy.

(B) Using `extra-env-lang` to work around (A) doesn't seem to be
terribly dangerous.

(C) The contract boundary makes operations on polymorphic data types
slow, and for higher-order data, they stack. For polymorphic,
first-order data, they're O(n), where n is the size of the data. For
polymorphic, higher-order data, operations are O(n*k), where k is the
number of crossings.

(D) Tricks (6,7) for getting around performance bottlenecks in (C) don't
generalize to full polymorphism.

(E) I've used `extra-env-lang` to insert types into the base type
environment a lot. But I've often been able to avoid using it by
changing the types of data (e.g. polymorphic to monomorphic), or by
moving or shrinking an abstraction boundary. In the examples I gave,
changing types or boundaries wouldn't work or would be too invasive (2),
or would change an existing user-facing API in a backward-incompatible
way (1).

(F) Some applications (5) are ridiculously sensitive to contract
overhead, even fast first-order contracts.

(G) There are functions that `require/typed` can't deal with because it
can't generate contracts for them (4). This isn't usually a problem when
you're writing both the typed and untyped code, but it's a problem when
the untyped code you want to use in TR isn't yours and has been in
widespread use for over a decade.


**** Comments and Speculation ****


I'll assume speculation is more OK now that we have examples. :)

It's in our nature to want to tackle (G) first because it's
well-defined. But it's also the least pressing. (You can always write an
untyped wrapper and use `require/typed` to import the wrapper. I know
this goes against TR's goals, but the workaround is easy and obvious.)
Here's how I would prioritize:

1. Polymorphic, first-order data
2. Polymorphic, higher-order data
3. Class contracts
4. Contracts for weird functions like `memcpy`

In the meantime, throw us a bone like `require/typed/unsafe` to replace
`extra-env-lang`. I would love to have something like it, if only to
avoid creating two new files and remembering all the crazy incantations
when I have to use `extra-env-lang`.

Neil ⊥

[Michael Ballantyne]

I'm delighted to offer both. Here's a particularly pathological test case:

https://github.com/michaelballantyne/typed-racket-performance

Using a typed/racket/no-check variant of the tr-pfds package makes my
untyped code run 1275x faster. The feature-profile tool reports that
in the TR variant "Contracts account(s) for 0.49% of total running
time", but I'm not sure I believe it.

[Neil Toronto]

Submit a bug report, because that number is obviously false. (Or you've
misunderstood how to use it, in which case the documentation probably
needs work. :D)

The problem is that first-order polymorphic contracts are O(n) in the
size of the data. See my other, much, much longer reply to Matthias.

It's a shame, because TR is such a nice language to write data
structures in.

Neil ⊥

[michael.ballantyne]

To offer another speculative solution, perhaps there could be a variant of Typed Racket structs that are opaque to untyped Racket. If only Typed Racket code is capable of constructing these objects, the types of their contents needn't be checked as they pass between typed and untyped code.