transient semantics #948

bennn · 2020-07-03T22:53:05Z

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 bennn/rackunit@32495bf).

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

write an RFC for the transient & erasure modes (rfc for #948 #952 )
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
~~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
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
all tests pass
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)
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 · 2020-07-05T08:02:14Z

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

bennn · 2020-08-06T21:58:00Z

typed-racket-lib/typed-racket/private/type-contract.rkt

+       [(void? v)
+        (flat/sc #'void?)]
+       [(or (symbol? v) (boolean? v) (keyword? v) (null? v) (eq? unsafe-undefined v))
+        (flat/sc #`(lambda (x) (eq? x '#,v)))]


@samth FYI for my dissertation, this function is (lambda (x) (void) (eq? x '#,v)) because of racket/racket#3339

(If there's time to measure again later, I'll re-run without the (void) if possible)

bennn · 2020-12-19T21:56:19Z

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.

typed-racket-lib/typed-racket/base-env/base-env-indexing-abs.rkt

bennn · 2020-12-19T22:04:49Z

typed-racket-lib/typed-racket/env/lexical-env.rkt

+                                          (lookup-type orig-id fail))))
+                              => (λ (orig-t)
+                                   (register-type i orig-t)
+                                   orig-t)]


@samth this is the part of Shallow TR that goes behind contracts to get types.

Ideally we'd use the typecheck/renamer.rkt interface to get types, but (I believe) the typechecking code here gets run after expansion => after those rename transformers have been expanded to the contracted identifiers.

Another idea is to serialize more types for the new identifiers, but I was never able to make that work. The typed id's come from one submodule & the contract versions come from another ... and I couldn't find a meeting point.

bennn · 2021-10-18T00:29:06Z

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 · 2021-10-18T21:36:59Z

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 · 2021-10-18T21:56:11Z

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 · 2021-10-18T21:59:14Z

[[ 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 · 2021-10-18T22:23:34Z

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 · 2021-10-19T02:22:12Z

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 · 2021-10-22T14:53:30Z

The latest test failure is on CS only, and seems to be a regression racket/racket#4030
EDIT: issue closed

racket-discourse-github-bot · 2022-04-21T20:59:21Z

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

Change some `define-typed/untyped-id` forms to work with typed/racket/shallow and typed/racket/optional Those TR languages are coming in PR 948 <racket/typed-racket#948>

racket-discourse-github-bot · 2022-06-14T00:04:23Z

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 · 2022-06-14T00:16:53Z

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

bennn · 2022-08-16T02:40:56Z

ping @samth @capfredf , time to merge?

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

author Ben Greenman <benjaminlgreenman@gmail.com> 1525024072 -0400 committer Ben Greenman <benjaminlgreenman@gmail.com> 1657924870 -0400 transient-pr: massive commit, squashed all development 2 ++ sync with racket#1078 transient: rename 't/r/shallow/base' to 't/r/base/shallow' etc. transient: fix poly class ctc transient: remove contract on default-continuation-prompt-tag transient: regression test, class rowvar contract transient: renamer fix, still working on plot typecheck/renamer struct accepts 4 args now, one for each lang it knows to expand to still need work to create the right args inside plot now may be complicated because of require/typed issue ... all r/t ids get reprovided in ignored quads transient: todo list transient: typo transient: shallow + optional plot tests transient: test define-typed/untyped ids from math and plot transient: tests + notes related to racket#189 transient: extra-env-lang, allow opt-in transient trust transient: add T+ flag to -> for trust/not transient: remove for-loop special case transient: avoid domain check for private methods transient: add class-utils module, de-duplicate code remove duplicate functions etc. from - check-unit-unit.rkt - transient-rewrite.rkt transient: fix -Arrow contract transient: fix extra close paren tranient: add subtype case for PolyRow transient: rewrite, try subst in stx->arrows transient: checkpoint, upgrading annotations for transient The goal is to infer when transient can trust a function and use that to improve type annotations so programmers don't need to maintain #:T+ annotations Maintaining the annotations would be fine, though, it's an ok fallback. new test passes: typed-racket-test/unit-tests/transient-rewrite-expansion/type-annotation.rkt but `raco setup typed-racket` has problems transient: add missing keyword in -Arrow call, plus small renamings transient: disable the toplevel upgrade transient: progress on tvars, fixed poly-dots.rkt and call-comp.rkt transient: update scoped tvar env for lambdas transient: add missing type annotations transient: clarify type-annotation #:infer first call (in guard) is no-infer, second infers transient: extra-env-lang + tc-app-contracts 1. extra-env-lang, accept a #:default-T+ param to reduce annotations 2. tc-app-contract record (to type-table) the type from a contract id transient: type environment + fixes - no check for Parameter sets - add a splicing macro to set the T+ default in type definitions transient: add trust annotations to tr-more envs transient: tests for typed-racket-more environment, skipping checks transient: contract-tests pass transient: check opaque objects across deep/shallow and deep/optional boundaries transient: clean up current-te-mode uses transient: share more class code, remove extra with-type provides transient: merge require-contract, fix type-contract mode bug bug = transient -> guarded thought we were "guarded mode with typed side = #t" fix = there are 2 modes to be aware of: the stashed and the current transient: simpler prims-contract macros, fix with-type export issue transient: fix tests - top-interaction was broken, bad pattern looking for the te-mode keyword had to change pattern in core.rkt and then change expectations in tests - transient-rewrite => hide substitution error (values-dots.rkt) by not substituting anymore transient: fix typecheck tests, had to change Arrow equality transient: make-pred-ty, change the old api less give a default to the "transient-trusted-positive" argument in one additional case-lambda case transient: rewrite tests, be careful finding paths don't use raw strings transient: possible-domains, fix bad fn arg transient: temporarily hide for and case-lambda rewrite tests transient: type->contract guarded Any always wraps testing ... this MIGHT be the fix for a problem: - provides from Transient to Guarded need typed-side = #f - UNLESS the provide has an Any type inside the fix is to always make an Any wrapper when generating contracts in guarded mode I can't think of another small fix. In particular, typed-side = 'both would not be right; we'd need a fourth side ("neither"?) transient: fix typo in test transient: revert Any change typed side = #true seems to always work for provides ... but lets test transient: avoid gensyms move the `set-transient-trusted-positive` function so it can use unsafe constructors and destructors and thereby avoid making gensyms related test: succeed/fold-left-inst.rkt transient: uncomment guarded contract-test ... whoops very disturbing that that was hidden and pushed transient: 3-mode sc conversion tests transient: rewriter, minor reorg transient: relax struct-property check transient: type-contract, try provide contracts again transient: compile 'historical-counterexamples' the file depends on redex which needs a recompile because transient changes the typed-renaming struct transient: move math + plot tests to external dir transient: delete plot tests, avoid GUI transient: hide math tests for now TODO (1) merge transient TR, (2) merge racket/math#68 transient: update RFC transient: documentation checkpoint transient: doc, progress on reference transient: doc, checkpoint on D/S/O examples transient: doc, fill in function examples transient: draft reference page transient: doc edit pass transient: improve errors for transient-rewrite tests, re-enable these tests expecting a CI failure transient: remove line number from rewrite test the line pointed to racket internals (private/for.rkt?), no need to test that transient: tiny doc update transient: doc, reference, when to use D S O transient: update / extend doc and reference transient: doc, guide, finish draft transient: doc, reference, cite transient: doc, use module style for examples transient: fix transient cast srcloc transient: revert define-predicate, make-predicate Do the same thing in Deep, Shallow, and Optional If someday someone has a use case, we can change them. (Weak predicates can express every type --- so you don't get a compile-time error asking for a vector predicate or a forall predicate --- but their run-time behavior is weak, and may be too confusing.) transient: doc, guide, mention expensive types transient: doc update - give specific examples of fast and slow types - remove 'trust' comment in Optional, ... there may be some kind of point there, but I don't know how to articulate it. Maybe, optional is best when you control the untyped modules and can easily debug them if something goes wrong transient: rename all transient: rewrite tests, rename stx pattern to match fn name transient: revert CI changes, remove todo file remaining todos: - make sure tests pass, especially --int tests - ping samth + fred + everyone for review - ping discord for reviews - measure performance - draft a racket blog post transient: uncomment hash-map/copy type why was it hidden in the first place? because ben is using racket 7.6 because he wasn't able to compile a newer version last time he tried transient: doc, longer title for 'semantic forms' sec transient: doc, mention untyped utils transient: doc, fix typo model -> module new failing test from take5 benchmark transient: fix trawl-for-property one simple version for units, one less-simple version for check-class-unit and shallow-rewrite

capfredf · 2022-08-16T03:01:02Z

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

typed-racket-doc/typed-racket/scribblings/guide/typed-untyped-interaction.scrbl

typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt

typed-racket-lib/typed-racket/base-env/prims-contract.rkt

typed-racket-lib/typed-racket/env/init-envs.rkt

typed-racket-lib/typed-racket/private/shallow-rewrite.rkt

typed-racket-lib/typed-racket/utils/tc-utils.rkt

bennn · 2022-08-18T01:26:33Z

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)

don't use `r` twice silly goose!

typed-racket-lib/typed-racket/private/shallow-rewrite.rkt

bennn · 2022-08-24T00:42:44Z

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

if shallow can trust the output of a pred-ty function, use (unsafe-shallow:make-pred-ty ...), which is much clearer than (make-pred-ty ... #t) ditto for asym-pred -> unsafe-shallow:asym-pred

before, make-pred-ty tried to default to "safe" but with lots of cases to opt in to "unsafe" the problem with that is that some case-lambda cases required a safe/unsafe decision (no default) after this commit, it's always safe unless you supply all 6 (or 5) args

bennn · 2022-08-25T03:54:41Z

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

sorawee · 2022-08-25T04:00:20Z

Yay!

yfzhe · 2022-08-25T05:11:10Z

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 · 2022-08-25T15:39:31Z

@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 · 2022-08-25T19:57:25Z

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

bennn · 2022-08-26T19:58:51Z

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: #1273

Change some `define-typed/untyped-id` forms to work with typed/racket/shallow and typed/racket/optional Those TR languages are coming in PR 948 <racket/typed-racket#948>

bennn added the in-progress label Jul 3, 2020

bennn self-assigned this Jul 3, 2020

bennn force-pushed the transient-pr branch from bba75e2 to f6acf6d Compare July 3, 2020 22:56

bennn added a commit to bennn/typed-racket that referenced this pull request Jul 28, 2020

rfc for racket#948

bac8582

bennn commented Aug 6, 2020

View reviewed changes

bennn commented Dec 19, 2020

View reviewed changes

typed-racket-lib/typed-racket/base-env/base-env-indexing-abs.rkt Outdated Show resolved Hide resolved

bennn commented Dec 19, 2020

View reviewed changes

bennn force-pushed the transient-pr branch from f6acf6d to 56b7deb Compare September 20, 2021 22:31

bennn force-pushed the transient-pr branch from 00f14f7 to b3b7898 Compare November 1, 2021 17:55

bennn force-pushed the transient-pr branch from 796ffca to 657b89c Compare November 22, 2021 15:34

bennn mentioned this pull request Nov 29, 2021

remove 'untyped-' redirects racket/plot#104

Merged

bennn force-pushed the transient-pr branch from 7b2f10c to 4f5b3f4 Compare April 1, 2022 19:20

bennn force-pushed the transient-pr branch from b720302 to 1a4e9c2 Compare April 21, 2022 01:05

bennn mentioned this pull request Apr 27, 2022

adapt define-typed/untyped-id to shallow & optional racket/math#68

Merged

bennn force-pushed the transient-pr branch from 7735115 to 07f7c1a Compare May 23, 2022 03:41

samth requested a review from capfredf June 13, 2022 18:35

bennn mentioned this pull request Jun 23, 2022

rfc for #948 #952

Closed

bennn force-pushed the transient-pr branch from 60b1c47 to 50719d6 Compare August 16, 2022 02:37

bennn added 3 commits August 15, 2022 22:49

transient: revert struct provide hack

9497a97

transient: remove unused vars

50719d6

capfredf removed the in-progress label Aug 16, 2022

capfredf reviewed Aug 17, 2022

View reviewed changes

bennn added 3 commits August 18, 2022 17:53

transient: checkpoint on fredf edits

4b7a6bb

transient: fix match expander

a545014

don't use `r` twice silly goose!

transient: move rev-append to utils

369aa75

shhyou reviewed Aug 19, 2022

View reviewed changes

typed-racket-lib/typed-racket/private/shallow-rewrite.rkt Outdated Show resolved Hide resolved

transient: actually use rev-append

d1a972d

capfredf approved these changes Aug 22, 2022

View reviewed changes

samth approved these changes Aug 22, 2022

View reviewed changes

bennn added 4 commits August 24, 2022 13:14

transient: add alias for make-pred-ty / asym-pred

82aca28

if shallow can trust the output of a pred-ty function, use (unsafe-shallow:make-pred-ty ...), which is much clearer than (make-pred-ty ... #t) ditto for asym-pred -> unsafe-shallow:asym-pred

transient: fix make-pred in tests, more

0ee421a

transient: revert init-env change

0fcb652

bennn merged commit 1dde78d into racket:master Aug 25, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

transient semantics #948

transient semantics #948

bennn commented Jul 3, 2020 •

edited

Loading

jackfirth commented Jul 5, 2020

bennn Aug 6, 2020

bennn commented Dec 19, 2020

bennn Dec 19, 2020

bennn commented Oct 18, 2021 •

edited

Loading

mfelleisen commented Oct 18, 2021

bennn commented Oct 18, 2021

mfelleisen commented Oct 18, 2021

bennn commented Oct 18, 2021

mfelleisen commented Oct 19, 2021

bennn commented Oct 22, 2021 •

edited

Loading

racket-discourse-github-bot commented Apr 21, 2022

racket-discourse-github-bot commented Jun 14, 2022

bennn commented Jun 14, 2022

bennn commented Aug 16, 2022

capfredf commented Aug 16, 2022

bennn commented Aug 18, 2022

bennn commented Aug 24, 2022

bennn commented Aug 25, 2022

sorawee commented Aug 25, 2022

yfzhe commented Aug 25, 2022

samth commented Aug 25, 2022

capfredf commented Aug 25, 2022 •

edited

Loading

bennn commented Aug 26, 2022

transient semantics #948

transient semantics #948

Conversation

bennn commented Jul 3, 2020 • edited Loading

Notes for code review

RESOLVED Design questions

Issues / TODO

Future

jackfirth commented Jul 5, 2020

bennn Aug 6, 2020

Choose a reason for hiding this comment

bennn commented Dec 19, 2020

bennn Dec 19, 2020

Choose a reason for hiding this comment

bennn commented Oct 18, 2021 • edited Loading

mfelleisen commented Oct 18, 2021

bennn commented Oct 18, 2021

mfelleisen commented Oct 18, 2021

bennn commented Oct 18, 2021

mfelleisen commented Oct 19, 2021

bennn commented Oct 22, 2021 • edited Loading

racket-discourse-github-bot commented Apr 21, 2022

racket-discourse-github-bot commented Jun 14, 2022

bennn commented Jun 14, 2022

bennn commented Aug 16, 2022

capfredf commented Aug 16, 2022

bennn commented Aug 18, 2022

bennn commented Aug 24, 2022

bennn commented Aug 25, 2022

sorawee commented Aug 25, 2022

yfzhe commented Aug 25, 2022

samth commented Aug 25, 2022

capfredf commented Aug 25, 2022 • edited Loading

bennn commented Aug 26, 2022

bennn commented Jul 3, 2020 •

edited

Loading

bennn commented Oct 18, 2021 •

edited

Loading

bennn commented Oct 22, 2021 •

edited

Loading

capfredf commented Aug 25, 2022 •

edited

Loading