@@ -883,13 +883,18 @@ the types `$T2` and `$T3` are equal to each other but not to `$T1`. These
883
883
type-checking rules for aliases of type exports mirror the * elimination* rule
884
884
of [ existential types] (∃T).
885
885
886
- Next, we consider resource type definitions, which are half-like abstract types
887
- in that they also produce a * fresh* type that is unequal to every preceding
888
- type. However, a resource type definition is ** not** abstract; it has a
889
- concrete representation that is known to the containing component (and * only*
890
- the containing component). Thus, local resource type definitions are neither
891
- structural nor abstract: they are "[ generative] ". For example, in the following
892
- example component:
886
+ Next, we consider resource type * definitions* which are a * third* source of
887
+ abstract types. Unlike the abstract types introduced by type imports and
888
+ exports, resource type definitions provide operations for setting and getting a
889
+ resource's private representation value: ` resource.new ` and ` resource.rep `
890
+ (introduced [ below] ( #canonical-built-ins ) ). However, these accessor operations
891
+ are necessarily scoped to the component instance that generated the resource
892
+ type, thereby hiding access to a resource type's representation from the outside
893
+ world. Because each component instantiation generates fresh resource types
894
+ distinct from all preceding instances of the same component, resource types are
895
+ [ "generative"] .
896
+
897
+ For example, in the following example component:
893
898
``` wasm
894
899
(component
895
900
(type $R1 (resource (rep i32)))
@@ -901,10 +906,9 @@ example component:
901
906
the types ` $R1 ` and ` $R2 ` are unequal and thus the return type of ` $f1 `
902
907
is incompatible with the parameter type of ` $f2 ` .
903
908
904
- The generativity of resource type definitions is well-suited to the abstract
905
- typing rules of type exports mentioned above, which force all clients of the
906
- component to bind a fresh abstract type. For example, in the following
907
- component:
909
+ The generativity of resource type definitions matches the abstract typing rules
910
+ of type exports mentioned above, which force all clients of the component to
911
+ bind a fresh abstract type. For example, in the following component:
908
912
``` wasm
909
913
(component
910
914
(component $C
@@ -992,9 +996,9 @@ standard [avoidance problem] that appears in module systems with abstract
992
996
types.
993
997
994
998
In summary: all type constructors are * structural* with the exception of
995
- ` resource ` , which is * generative* . Type imports and exports that have a subtype
996
- bound are * abstract (resource) types* and follow the standard introduction and
997
- elimination rules of universal and existential types.
999
+ ` resource ` , which is * abstract * and * generative* . Type imports and exports that
1000
+ have a subtype bound also introduce abstract types and follow the standard
1001
+ introduction and elimination rules of universal and existential types.
998
1002
999
1003
Lastly, since "nominal" is often taken to mean "the opposite of structural", a
1000
1004
valid question is whether any of the above "nominal typing". Inside a
0 commit comments