transient semantics

[bennn]

trafficstars

Goal: add a new way to run typed/racket programs. The new types are weaker against untyped code, but should run faster.

2021-11-01: This PR is the main development. ~For now, this PR is a preview of the main development at https://github.com/bennn/typed-racket/tree/transient . I'm planning to keep a todo list here, listen to feedback, and push changes once I have them. Eventually, I want to merge this branch.~

Notes for code review

• utils/transient-rewrite.rkt ~defender/defender.rkt~ rewrites expanded, unoptimized typed code with flat contract checks everywhere that an untyped value can enter at runtime.

• private/type-contract.rkt has a new function type->static-contract/transient that turns a type into a flat contract

• cast and other exports from base-env/prims-contract.rkt come in multiple versions with different semantics (Deep, Shallow, Optional)

• Other changes follow the type-enforcement-mode? box from utils/tc-utils.rkt. This new piece of state gets instantiate like the typed-context? box. It decides how to compile types to runtime checks.

RESOLVED Design questions

Q. Transient code should be able to use typed/rackunit macros, but in general we can't allow guarded macros in non-guarded code. I propose using unsafe-provide for macros that are safe in transient (DONE https://github.com/bennn/rackunit/commit/32495bff0badecf6d1d3eea5c7be476fc3c7fcb1).

Q. define-typed/untyped-identifier should probably take a 3rd optional argument. Here's the problem: Transient needs to (require/typed plot (plot-pict ....)) with a huge type because plot defines that as a typed/untyped id and so Transient gets an untyped identifier (it can't use the guarded one). That huge type should be defined once and for all with a require/typed on the library side. Sounds good? (YES, DO IT)

Q. The type environment files have changes to let the defender know whether transient can trust the results of a base-env function. These annotations are not enough for higher-order library functions; for example, make-do-sequence returns a function that we need to trust because TR's types are not dependent enough. For now, I have a hack to trust that function --- should we keep the hack for now, or try changing the type-rep to encode transient trust? (KEEP FOR NOW)

Issues / TODO

• [x] write an RFC for the transient & erasure modes (#952 )
• [x] add #langs ... instead of #lang typed/racket #:transient want #lang typed/racket/transient so we can use a repl and so module+ is no longer unsound
• [x] ~add "expected" results to any typed-racket-test/succeed and ..../fail files that have a different outcome on transient; change the tester to run each file on each mode (ditto for other tests)~ 2021-09-20: to keep this PR moving, I made a new folder typed-racket-test/fail/transient/ ; the tester changes look difficult
• [x] in the defender review all "ignore" expressions ... maybe transient rewriting should never ignore code EDIT 2021-09-20: yes indeed, transient rewriting should not ignore expressions but rather dive into them looking for typed code
• [x] all tests pass
• [x] rename typed/racket/shallow/base to typed/racket/base/shallow etc. so that "how to enforce types" is always the last modifier (just like how no-check works)
• [x] docs for the new languages
  • add reference pages for Shallow and Optional, similar to the no-check page
  • consider splitting ref. section 2 (special forms) into typechecking & runtime forms; extend the docs for runtime forms
  • consider documenting the shape / "transient view" of static types alongside the type ... and maybe do the same for Deep
  • decide how to update the guide
• [ ] measure performance once things are in shape
  • might want to implement a cheap and/c to avoid racket/contract inside transient

Future

Long-term issues for Transient. Record these on a project page?

• Transient-specific optimizations to avoid checks and/or improve their representation.
• Deep can optimize the contracts on exports to Shallow (need to change typecheck/renamer.rkt with another arg.)
  • integer? = no contract
  • (-> integer? integer?) = no contract
  • (-> integer? (vectorof integer?)) = (-> any (vectorof integer?))
• edit: DONE ~Instead of keeping a "Transient env" of identifiers that don't need a result check (e.g. map), store that info IN the type itself. That way, a function can return a trusted function (e.g. (negate void?)).~

[jackfirth]

Eagerly awaiting the RFC, since this sounds extremely cool but I don't understand it at all 🎉

[bennn]

quick update: my dissertation is in and this pull request is now a top priority

I'll work on making the test suite reusable first, then get to working on this branch.

[bennn]

Right now, Shallow code (transient) exports ids using basically the same renamer strategy as normal Deep code. If a Shallow export appears in Shallow or untyped code, it expands to the plain id. In Deep code, it expands to a contract-wrapped id.

The downside of this approach is that a Shallow module needs to prepare the same kinds of contracts that Deep does. Same goes for Optional (unsound) modules.

I wonder if this could work differently. Maybe all Shallow exports can be plain identifiers with some syntax-local-value info ... or something ... that Deep code can look for. Then if a Deep module sees one of these ids, it uses the require/typed method to add a contract.

EDIT: hang on, this 2nd strategy might be worse. If N Deep modules import one Shallow module, they're going to make N copies of the contract code. Unlike require/typed, this duplication isn't going to be easy to spot.

[mfelleisen]

The question you need to ask is who should know of the existence of Shallow.

The introduction of Deep (TR) could not make Untyped Modules work in a different way, just because there's a new #lang in the ecosystem. This design rule applies here too.

[bennn]

The change I'm wondering about wouldn't affect programmers. Deep modules get to use (require typed.rkt) no matter what variant of typed/racket that file decides to use.

[mfelleisen]

[[ If I had used the word "who" in the classroom, the other half of me would have cringed (at least). ]]

I do not mean people. I mean "semantics of TR types", and that should definitely be referred to with "it" and "which". Sorry for the confusion.

So why should Deep know to attach contracts to things that come from Shallow? Or does it simply not know where it comes from at all and treats all such imports uniformly?

[bennn]

Ah, okay.

Right now, Deep doesn't know where imports come from and treats them all uniformly.

Deep should know because those contracts are Deep's business, to protect itself. The current implementation is arguably backwards: a Shallow module has to prepare Deep contracts, which means that it will error when imported by a Deep client if there's a problem making the contracts.

Then again, the error only happens during a require. And the current implementation has the (major?) benefit that it creates one copy of those Deep contracts instead of one per Deep client. I'm leaning toward keeping things as they are.

[mfelleisen]

OK, I haven't thought this thru completely, but based on the diss, every semantics of Types in TR can protect itself w/o knowing what other semantics exists, other than that they mess up the global invariants. If this is correct, I agree that changing it would be 'the right thing'. [[ If I am wrong, we need to work this out. ]]

I do wonder whether this generalizes to a spectrum of grad type sem.

[bennn]

The latest test failure is on CS only, and seems to be a regression https://github.com/racket/racket/issues/4030 EDIT: issue closed

[racket-discourse-github-bot]

This pull request has been mentioned on Racket Discussions. There might be relevant details there:

https://racket.discourse.group/t/managing-cast-performance-penalty/905/3

[racket-discourse-github-bot]

This pull request has been mentioned on Racket Discussions. There might be relevant details there:

https://racket.discourse.group/t/managing-cast-performance-penalty/905/27

[bennn]

@samth @capfredf (and anyone else!) the tests are passing & I don't have any other changes planned. Please look this over & send comments and questions.

Major highlights:

• In rep/type-rep.rkt , the Arrow rep has a boolean flag to let Shallow TR know that it does not need to check the result of calls to this arrow. Because of the new flag, there are lots of changes to base types. I used a syntax parameter to change the default from "no" to "yes" in some files to lower the number of edits, but there are still a lot.
• Another big diff is in base-env/prims-contract.rkt . It makes weaker versions of cast, require/typed, etc. for Shallow and Optional TR.
• The biggest new block of code is private/shallow-rewrite.rkt. Shallow TR uses this to add runtime checks in well-typed code. (If you know Retic. Python / Transient, it's a Transient pass.)
• Most other changes use the new parameter current-type-enforcement-mode to decide how to compile based on the #lang at hand. In normal (Deep) TR, we do same thing as before. In Shallow TR and Optional TR, we do something weaker. For example, the optimizer does fewer optimizations on Shallow code and doesn't run at all on Optional code.

[jackfirth]

Hey @bennn just a heads up: I added Resyntax pull request reviews to this repository and I'm not sure how well it will handle a huge delta like this. If you rebase your branch I'm pretty sure it will trigger a Resyntax run. If that happens and Resyntax does something weird because of the huge diff, let me know.

[bennn]

ping @samth @capfredf , time to merge?

ps Jack, resyntax seems to work fine on this PR!

[capfredf]

Sorry for the delay. Reviewing this pr is on my to-do list, but somehow I forgot it. I will take a look asap this week

[bennn]

Thanks @capfredf ! I left a few clarifying comments. For everything else, the response is basically: yes and I'll make a change.

(no-check is not exactly the same behavior as Optional ... definitely for multi-module programs and possibly for single modules too)

[bennn]

Awesome. I'll add the alias make-unsafe-shallow-pred-ty and merge once the tests pass.

[bennn]

So happy I'll never need to rebase this PR atop master again.

[sorawee]

Yay!

[yfzhe]

I found that both kind system rfc and this transient semantics rfc use the same 003 ordinal number. Should the transient semantics one be changed to 004?

[samth]

@yfzhe this one should change to 004.

@bennn there are some test failures on DrDr, eg http://drdr.racket-lang.org/61460/racket/share/pkgs/typed-racket-test/unit-tests/shallow-rewrite-expansion/list.rkt

[capfredf]

@bennn seems like racket -l typed-racket-test -- --unit don't run those failed tests found by DrDr

[bennn]

Right, those files aren't supposed to run. The harness compiles them & looks at the expanded code. (Except for type-annotation.rkt, which is unsupported.)

I tried adding compile-omit-paths. Also fixed the rfc number: https://github.com/racket/typed-racket/pull/1273