feat: checked cast with TypedMatcher #8394

turadg · 2023-09-27T15:30:01Z

Description

I ran again into the need for type narrowing with a shape object: https://github.com/Agoric/agoric-sdk/pull/8385/files#diff-b17d46d065ac769cdf1d70471b16d141f28672965c18522d58d39722d4852ad4R329-R331

endojs/endo#1721 approached the general problem of inferring the type from the shape. But until we have that, we can at least move the type description onto the shape object so users of that shape can automatically get the type a match implies.

With this, the code referenced above would be,

const questionDesc = cast(info, QuestionSpecShape);

Security Considerations

n/a

Scaling Considerations

n/a

Documentation Considerations

Once this settles in agoric-sdk, we may want to move it into Endo. Alternately, Endo waits for more general support.

Testing Considerations

Has a test. Maybe should use tsd instead of Ava

Upgrade Considerations

n/a

turadg · 2023-09-28T13:10:02Z

While searching for other places to use this, most of the shape checks are to validate the type that a value already has statically. So there's no value in the narrowing. For example, a function param foo: Foo.

We could have some utility type for indicating the soundness of the type annotation.

One way is a utility type Expect<> for "this ought to be type Foo but we don't know yet". Then functions that actually validate the type could have foo: Expect<Foo> as a parameter. That would maintain the documentation aspect of the parameters but also let the type be narrowed. Expect<Foo> would have to accept Foo as an argument so the tag would be optional. That means, since TS is structural, that anything could use an Expect<Foo> as if it were a Foo, but at least there would be an indication that it hasn't been validated. We could have a linter verify rules around use of Expect types.

Going the other way, we could have a Sound<> type that says "this claimed to be Foo and some code has run to verify that`. This perhaps aligns more with the reality of TS in that naked types have no expectation of soundness. But it seems less pragmatic to me and more verbose.

michaelfig

Just one comment, otherwise LGTM!

michaelfig · 2023-09-29T20:33:46Z

packages/internal/src/types.d.ts

@@ -18,3 +20,17 @@ export declare class SyncCallback<

  public isSync: true;
 }
+
+declare const type: unique symbol;


It's a little weird to me to use the identifier type here when it's also a TypeScript keyword. Could you please name it something like TypedMatcherParameter or anything that you think would be better.?

erights · 2023-09-30T03:03:50Z

@turadg , while I would still appreciate the verbal explanation we arranged, please don't wait on that to merge this. I understand this well enough that I'd be happy (overjoyed, actually) to see it merged based on @michaelfig 's approval. You can then clear up my remaining confusions post-merge.

turadg · 2023-09-30T03:25:17Z

@erights before merging I'd like to include some usages of it in this PR, to validate the design. If you have some in mind feel free to push commits.

erights

My memory of this has gotten stale, so perhaps I forgot. But,

Why is this in agoric-sdk? It seems much more natural to include it in endo, either @endo/patterns or @endo/exo. Isn't this useful for anything building on those?

turadg · 2023-12-01T19:12:41Z

It seems much more natural to include it in endo

That it would be useful in Endo does not seem to me a reason to exclude it from agoric-sdk.

I started in in agoric-sdk so that I could evaluate its utility in agoric-sdk and iterate on the design. Once the design and implementation are acceptable,I think the next step is to land it here. Then a separate PR can copy it to Endo and a third PR can make agoric-sdk use that once it's published.

erights · 2023-12-01T19:29:53Z

That seems like 3x as much work, spread out over at least 10x as much time. If we're agreed that the correct final destination is, say, @endo/patterns, why not just do it?

I suspect we have conflicting unstated assumptions, so probably best to postpone this to a more general engineering discussion. cc @ivanlei @kriskowal

turadg · 2024-03-28T14:19:21Z

If we're agreed that the correct final destination is, say, @endo/patterns, why not just do it?

The effort required delays my work developing our SDK product
The calendar wait to get it into Endo and then wait for an Endo sync delays its availability to anyone in SDK
It may merit some adjusting that can only be determined from active use. Endo is meant to change more slowly and take things that are battle tested.
If we hadn't had this hurdle the PR would have been available in agoric-sdk 6 months ago

michaelfig · 2024-04-23T18:51:43Z

I suspect we have conflicting unstated assumptions,

My assumptions: adding code to Agoric SDK should be frictionless and entirely based on what pragmatically benefits our platform. We should not implement experimental features in Endo until we have gained experience with them and can justify the additional cost of maintaining them for a wider audience.

I am in favour of exploring the path laid out in this PR, and committing it to Endo once we have learned its shape better.

cloudflare-workers-and-pages · 2024-04-24T00:25:34Z

Deploying agoric-sdk with Cloudflare Pages

Latest commit:	`20e1779`
Status:	✅ Deploy successful!
Preview URL:	https://2791640a.agoric-sdk.pages.dev
Branch Preview URL:	https://ta-typed-shapes.agoric-sdk.pages.dev

View logs

erights · 2024-04-24T00:57:23Z

I suspect we have conflicting unstated assumptions,

My assumptions: adding code to Agoric SDK should be frictionless and entirely based on what pragmatically benefits our platform. We should not implement experimental features in Endo until we have gained experience with them and can justify the additional cost of maintaining them for a wider audience.

I am in favour of exploring the path laid out in this PR, and committing it to Endo once we have learned its shape better.

This argument presumes there is some clear conceptual boundary between agoric-sdk and endo, such that we're willing to put experiments on agoric-sdk master that we're not willing to put in endo master. If the argument were to keep an experiment encapsulated within the one package that uses it, that I'd understand. A package is a modularity boundary I understand. But once it gets outside a single package, I don't get it.

Most things that start out this way never take the second step, leaving them misplaced for ages. That migration is never the most urgent thing to do right now, so it never gets done.

But since the choice seems to be to approve having it start in the wrong place vs not having it at all, I will review this as an agoric-sdk PR. Please do file an issue to migrate it to endo when "ready". Then we'll at least have a better chance at eventually getting around to it.

erights · 2024-04-24T01:00:02Z

If we're agreed that the correct final destination is, say, @endo/patterns, why not just do it?

The effort required delays my work developing our SDK product

The calendar wait to get it into Endo and then wait for an Endo sync delays its availability to anyone in SDK

It may merit some adjusting that can only be determined from active use. Endo is meant to change more slowly and take things that are battle tested.

If we hadn't had this hurdle the PR would have been available in agoric-sdk 6 months ago

I do understand and sympathize with these latency costs. I've paid them many times, with changes that should have taken a day instead taking months (attn @ivanlei @kriskowal ). But it is worth noting that if we did an endo-release-agoric-sdk-sync every night, most of this latency would disappear.

So please at least do file that issue. Thanks.

erights · 2024-04-24T01:04:16Z

@turadg , since your endojs/endo#2238 is in flight right now, could you bundle these changes with that? I'd be much happier reviewing them there ;)

erights · 2024-04-24T01:07:57Z

@turadg , since your endojs/endo#2238 is in flight right now, could you bundle these changes with that? I'd be much happier reviewing them there ;)

I am proceeding with the review here now. I did not mean to imply otherwise.

erights

Except for the one declaration that I cannot yet review, all the rest LGTM.

packages/vat-data/src/exo-utils.js

turadg · 2024-07-12T00:44:45Z

the recent TypedPattern change prompted me to clean this up to land

erights · 2024-07-12T01:01:35Z

packages/internal/src/types.d.ts

+  specimen: unknown,
+  pattern: P,
+  label?: string | number,
+) => asserts specimen is P extends TypedPattern<any> ? PatternType<P> : unknown;


Now that I understand it, OMG this is cool!

Should this eventually migrate into endo? Into the @endo/patterns package? I hope so. If you agree, would be good to comment on that expected migration here, or somewhere relevant.

Similarly, should #6160 have been an endo issue rather than an agoric-sdk issue, with the eventual fix also eventually being in endo?

If you agree, would be good to comment on that expected migration here, or somewhere relevant.

I expect it'll happen when there's some trigger.

should #6160 have been an endo issue rather than an agoric-sdk issue, with the eventual fix also eventually being in endo?

Could have been. Though it's much faster to being useful by making it work in agoric-sdk and moving it to Endo when it's stable.

erights · 2024-07-12T01:08:23Z

packages/ERTP/src/paymentLedger.js

 */

 /**
+ * @template {AssetKind} K


Generally, which I've written code like this template declaration, I revise it to

Suggested change

* @template {AssetKind} K

* @template {AssetKind} [K=AssetKind]

since the supertype constraint is usually also a fine default.

In this case there's no way the to omit the parameter because it's positional

erights · 2024-07-12T01:12:30Z

packages/internal/src/typeCheck.js

@@ -0,0 +1,23 @@
+// @ts-check
+import { mustMatch as typelessMustMatch } from '@endo/patterns';


Should we eventually move this into @endo/patterns so the only mustMatch is the typed one, and the typeless one is never exported? (Modulo the transition costs, which I expect will be painful but tolerable.)

Yes, I think once we've had some stress testing of it so we know it won't change much.

packages/orchestration/src/typeGuards.js

erights · 2024-07-12T01:15:38Z

packages/store/src/index.js

+/**
+ * @import {MustMatch} from '@agoric/internal';
+ */
+import { mustMatch as typelessMustMatch } from '@endo/patterns';


Is a layering problem causing this duplication, or could all uses of this one use the @agoric/internal one instead?

@agoric/store is actually lower than @agoric/internal, unfortunately

I see. Could it be moved and exported from @agoric/store for now? As a permanent home, that would be weird. But if it's ultimate destination is @endo/patterns, well, @agoric/store still does deprecated reexporting of many things from @endo/patterns, since patterns lived there first.

I leave this to your esthetics. Your status quo is not doing an offensive amount of duplication; just a tiny amount.

I'll do that before merging, so I won't merge tonight

erights · 2024-07-12T01:17:01Z

packages/time/src/timeMath.js

@@ -1,9 +1,16 @@
 import { Nat } from '@endo/nat';
 import { Fail, q } from '@endo/errors';
-import { mustMatch } from '@endo/patterns';
+import { mustMatch as typelessMustMatch } from '@endo/patterns';


Now I'm confused. This is unlikely to be a layering constraint. Why not use the one from @agoric/internal ?

because @agoric/time currently doesn't depend on anything in @agoric

Is there any reason not to change it to depend on @agoric/internal? When it doesn't create a layering problem, that's what I'd do.

I defer to @warner. If no objections then I'll do it in a follow-up PR. (probably importing from @agoric/store which is almost Endo :)

And it is thematically what @agoric/internal is for.

I'm glad you like the tred visualization ;)

Yes, using @agoric/store as a staging ground for moving to endo makes sense to me. Thanks.

erights

LGTM. I'm excited to start using this! Thanks.

turadg requested review from erights and michaelfig September 27, 2023 15:30

turadg force-pushed the ta/typed-shapes branch from 2e79cfd to 360d848 Compare September 27, 2023 23:29

michaelfig approved these changes Sep 29, 2023

View reviewed changes

turadg force-pushed the ta/typed-shapes branch from 360d848 to 94e2ff6 Compare September 30, 2023 03:25

erights requested changes Dec 1, 2023

View reviewed changes

turadg mentioned this pull request Dec 6, 2023

"Extra args dropped" was too lenient. Throw error instead endojs/endo#1888

Closed

turadg mentioned this pull request Mar 28, 2024

way to define an object type from its interface guard #9163

Open

turadg force-pushed the ta/typed-shapes branch from 235e0fe to 85e633f Compare April 24, 2024 00:25

turadg requested a review from erights April 24, 2024 00:27

erights requested changes Apr 24, 2024

View reviewed changes

packages/vat-data/src/exo-utils.js Outdated Show resolved Hide resolved

turadg marked this pull request as draft June 12, 2024 12:43

turadg force-pushed the ta/typed-shapes branch from 85e633f to 9d49f0e Compare July 12, 2024 00:44

turadg marked this pull request as ready for review July 12, 2024 00:44

erights reviewed Jul 12, 2024

View reviewed changes

erights approved these changes Jul 12, 2024

View reviewed changes

turadg added the automerge:rebase Automatically rebase updates, then merge label Jul 12, 2024

turadg added 7 commits July 12, 2024 14:41

style: jsdoc format vat-data package

4a80f4b

refactor: move TypedPattern to internal

8852a06

chore: update type-coverage

5b9fedf

feat: checked cast with TypedMatcher

ed14400

feat: narrow types with mustMatch

685ffac

chore: update type-coverage

0c4f75e

fix(types): agoricContract shape check

20e1779

turadg force-pushed the ta/typed-shapes branch from ccd0383 to 20e1779 Compare July 12, 2024 14:41

turadg mentioned this pull request Jul 12, 2024

feat: auto-stake-it example contract #9666

Merged

mergify bot merged commit 17608dc into master Jul 12, 2024
78 checks passed

mergify bot deleted the ta/typed-shapes branch July 12, 2024 15:15

	* @template {AssetKind} K
	* @template {AssetKind} [K=AssetKind]

		@@ -0,0 +1,23 @@
		// @ts-check
		import { mustMatch as typelessMustMatch } from '@endo/patterns';

feat: checked cast with TypedMatcher #8394

feat: checked cast with TypedMatcher #8394

Conversation

turadg commented Sep 27, 2023

Description

Security Considerations

Scaling Considerations

Documentation Considerations

Testing Considerations

Upgrade Considerations

turadg commented Sep 28, 2023

michaelfig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

erights commented Sep 30, 2023

turadg commented Sep 30, 2023 • edited Loading

erights left a comment

Choose a reason for hiding this comment

turadg commented Dec 1, 2023

erights commented Dec 1, 2023

turadg commented Mar 28, 2024

michaelfig commented Apr 23, 2024

cloudflare-workers-and-pages bot commented Apr 24, 2024 • edited Loading

Deploying agoric-sdk with Cloudflare Pages

erights commented Apr 24, 2024

erights commented Apr 24, 2024 • edited Loading

erights commented Apr 24, 2024

erights commented Apr 24, 2024

erights left a comment

Choose a reason for hiding this comment

turadg commented Jul 12, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

turadg Jul 12, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

erights left a comment

Choose a reason for hiding this comment

turadg commented Sep 30, 2023 •

edited

Loading

cloudflare-workers-and-pages bot commented Apr 24, 2024 •

edited

Loading

erights commented Apr 24, 2024 •

edited

Loading

turadg Jul 12, 2024 •

edited

Loading