Re: [TYPES] a naive question on datatype declarations

Jon Sterling <[email protected]> Mon, 29 Jan 2024 09:36:10 +0000
Newsgroups gmane.comp.science.types
Message-ID <[email protected]>
WyBUaGUgVHlwZXMgRm9ydW0sIGh0dHA6Ly9saXN0cy5zZWFzLnVwZW5uLmVkdS9tYWlsbWFuL2xp
c3RpbmZvL3R5cGVzLWxpc3QgXQoKSGkgVGhvcnN0ZW4sCgpJIGRvbid0IGtub3cgd2hhdCB0byB0
ZWxsIHlvdSwgc2luY2UgSSdtIGRlc2NyaWJpbmcgbm90aGluZyBtb3JlIHRoYW4gdGhlIHJ1bGUg
b2YgY29udHJhY3Rpb24gaW4gbG9naWMgLyB0eXBlIHRoZW9yeSDigJQgd2hpY2ggaXMgdGhlIGVz
c2VuY2Ugb2YgYWJzdHJhY3Rpb24gKHRlbXBvcmFyaWx5IHZpZXdpbmcgdHdvIGlkZW50aWNhbCB0
aGluZ3MgYXMgZGlmZmVyZW50KS4gSWYgeW91IHdhbnQgdG8gZGlzcHV0ZSBhYm91dCB3aGV0aGVy
IHRoaXMgaXMgc2VtYW50aWNhbGx5IG1lYW5pbmdsZXNzIG9yIGEgImhhY2siLCBnbyBhaGVhZCDi
gJQgYnV0IEkgdGhpbmsgSSdtIGdvaW5nIHRvIGJvdyBvdXQgb2YgdGhlIGRpc2N1c3Npb24uIEdl
cnNob20gYnkgbm93IGhhcyBnb3R0ZW4gYSB2YXJpZXR5IG9mIHZlcnkgaW50ZXJlc3RpbmcgYW5k
IGhlbHBmdWwgYW5zd2Vycy4KCkJlc3QsCkpvbgoKCj4gT24gSmFuIDI5LCAyMDI0LCBhdCA5OjMy
4oCvQU0sIFRob3JzdGVuIEFsdGVua2lyY2ggPFRob3JzdGVuLkFsdGVua2lyY2hAbm90dGluZ2hh
bS5hYy51az4gd3JvdGU6Cj4gCj4gV2hhdCBkb2VzIGl0IG1lYW4gdG8gaW50cm9kdWNlIHR3byBj
b3BpZXMgb2YgdGhlIHNhbWUgZGF0YXR5cGU/Cj4gIAo+IEFuZCBpZiB3ZSBjYW7igJl0IHNob3cg
QWdlbnRJbnQgIT0gTGVuZ3RoSW50IGNhbiB3ZSBzaG93IG5vdCggQWdlbnRJbnQgIT0gTGVuZ3Ro
SW50KT8KPiAgCj4gSXQgc2VlbXMgdG8gbWUgeW91ciBzdWdnZXN0aW9uIGlzIGp1c3QgYSBoYWNr
IGFidXNpbmcgYW4gZXhpc3RpbmcgbGFuZ3VhZ2UgZmVhdHVyZSBidXQgaXQgaXMgc2VtYW50aWNh
bGx5IG1lYW5pbmdsZXNzLgo+ICAKPiBUaG9yc3Rlbgo+ICAKPiBGcm9tOiBKb24gU3Rlcmxpbmcg
PGpvbkBqb25tc3RlcmxpbmcuY29tPgo+IERhdGU6IE1vbmRheSwgMjkgSmFudWFyeSAyMDI0IGF0
IDA4OjI0Cj4gVG86IFRob3JzdGVuIEFsdGVua2lyY2ggKHN0YWZmKSA8cHN6dHhhQGV4bWFpbC5u
b3R0aW5naGFtLmFjLnVrPgo+IENjOiB0eXBlcy1saXN0QExJU1RTLlNFQVMuVVBFTk4uRURVIDx0
eXBlcy1saXN0QExJU1RTLlNFQVMuVVBFTk4uRURVPgo+IFN1YmplY3Q6IFJlOiBbVFlQRVNdIGEg
bmFpdmUgcXVlc3Rpb24gb24gZGF0YXR5cGUgZGVjbGFyYXRpb25zCj4gCj4gVGhvcnN0ZW4g4oCU
IFRoZSB1c2Ugb2YgYWJzdHJhY3QgdHlwZXMgdG8gZm9ybWFsbHkgZGlzdGluZ3Vpc2ggdHdvIGNv
cGllcyBvZiB0aGUgInNhbWUiIGRhdGEgdHlwZSBpcyBwcmVjaXNlbHkgdGhlIHRoaW5nIHRoYXQg
YXZvaWRzIG9ic2VydmluZyBhbnl0aGluZyBhYm91dCBhIGRhdGF0eXBlIGJleW9uZCBpdHMgaXNv
bW9ycGhpc20gY2xhc3MsIGFuZCB0aGlzIGRvZXMgY2VydGFpbmx5IG5vdCBpbXBseSBpbnRyb2R1
Y2luZyB0YWdzLiBZb3VyIHByb3Bvc2VkIHNvbHV0aW9uLCB0byBpbnRyb2R1Y2UgdGFncyBpbiBv
cmRlciB0byBkaXN0aW5ndWlzaCB0d28gZGlmZmVyZW50IGludGVuZGVkIHVzZXMgb2YgYSBkYXRh
dHlwZSwgaXMgZmFyIHRvbyBzdHJvbmcgYW5kIGlzIHVubmVjZXNzYXJ5LiBJbmRlZWQsIHdpdGgg
dGFncywgeW91IHdvdWxkIGJlIGFibGUgdG8gc2hvdyB0aGUgbmVnYXRpb24gb2YgIkFnZUludCA9
IExlbmd0aEludCIgb3Igc29tZXRoaW5nLCBidXQgYWxsIHRoYXQgaXMgbmVlZGVkIHRvIGFuc3dl
ciBHZXJzaG9tJ3MgcXVlc3Rpb24gaXMgdGhhdCB3ZSAiQWdlSW50ID0gTGVuZ3RoSW50IiBiZSBu
b24tZGVyaXZhYmxlLiBJbiB0aGUgcGFzdCwgY2VydGFpbiBzeXN0ZW1zIGhhdmUgaW1wbGVtZW50
ZWQgYWJzdHJhY3Rpb24gYnkgbWVhbnMgb2YgdGFncywgYnV0IHRoYXQgaXMgbm90IG5lY2Vzc2Fy
eTsgdGhlIHNpbXBsZXN0IGltcGxlbWVudGF0aW9uIG9mIGFic3RyYWN0aW9uIGlzIGEgZm9ybSBv
ZiBsZXQtYmluZGluZywgd2hpY2ggb2J2aW91c2x5IGludHJvZHVjZXMgbm8gbm90aW9uIG9mIHRh
ZyDigJQgYW5kIGlzIGNvbXBhdGlibGUgbmVpdGhlciAiQWdlSW50ID0gTGVuZ3RoSW50IiBub3Ig
Ik5vdChBZ2VJbnQgPSBMZW5ndGhJbnQpIiBiZWluZyBkZXJpdmFibGUsIGFzIGlzIGRlc2lyYWJs
ZSBpbiB0aGUgcHJlc2VudCBkaXNjdXNzaW9uLgo+ICAKPiBJIHdvdWxkIHNheSB0aGF0IHRoZSBj
b25jZXB0IG9mIHRhZ3MgaXMgYSBzZXBhcmF0ZSBvbmUgdGhhdCBoYXMgZGVlcCBhbmQgaW50ZXJl
c3RpbmcgdGhlb3J5IGFuZCBhcHBsaWNhdGlvbnMsIGFzIEpvbmF0aGFuIEFsZHJpY2ggaGFzIHBv
aW50ZWQgb3V0LiBCdXQgdHlwZSBhYnN0cmFjdGlvbiBkb2VzIG5vdCBpbXBseSB0YWdnaW5nIOKA
lCBub3QgZXZlbiAic3RhdGljIiB0YWdnaW5nLiBUYWdnaW5nIGlzIGltcG9ydGFudCB3aGVuIHlv
dSB3YW50IHRvIGJlIGFibGUgdG8gYWN0dWFsbHkgbmVnYXRlIHRoZSBpZGVudGlmaWNhdGlvbiBv
ZiB0d28gZGlmZmVyZW50bHktdGFnZ2VkIHR5cGVzLiBOZWdhdGlvbiBpcyBub3QgdGhlIHNhbWUg
dGhpbmcgYXMgZmFpbHVyZS4KPiAgCj4gQmVzdCwKPiBKb24KPiAgCj4gCj4gCj4gT24gSmFuIDI4
LCAyMDI0LCBhdCA2OjUy4oCvUE0sIFRob3JzdGVuIEFsdGVua2lyY2ggPFRob3JzdGVuLkFsdGVu
a2lyY2hAbm90dGluZ2hhbS5hYy51az4gd3JvdGU6Cj4gIAo+IEhpLAo+ICAKPiBUaGlzIGRvZXNu
4oCZdCBtYWtlIHNlbnNlIHRvIG1lOiBkYXRhdHlwZXMgYXJlIG5vdCBhYnN0cmFjdCB0eXBlcyBo
ZW5jZSB3aHkgc2hvdWxkIHRoZXkg4oCcdHJlYXRlZOKAnSBhcyBzdWNoPwo+ICAKPiBGcm9tIGEg
c2VtYW50aWMgcG9pbnQgb2YgdmlldyBhbGwgdGhhdCB3ZSBzaG91bGQgYmUgYWJsZSB0byBvYnNl
cnZlIG9mIGEgZGF0YXR5cGUgaXMgaXRzIGlzb21vcnBoaXNtIGNsYXNzLiBOb3cgaW4gYXBwbGlj
YXRpb25zIHdlIHdhbnQgdG8gZGlzdGluZ3Vpc2ggZGlmZmVyZW50IHVzZXMgb2YgYSBkYXRhdHlw
ZSwgZS5nLiBhbiBpbnRlZ2VyIG1heSByZXByZXNlbnQgYW4gYWdlIG9yIHRoZSBudW1iZXIgb2Yg
ZWdncy4gVGhpcyBpcyBhIGRpZmZlcmVudCBiZWFzdCBpdCBpcyBhIHR5cGUgdG9nZXRoZXIgd2l0
aCBhIHRhZyAob3IgYSBkaW1lbnNpb24pLiBJdCBkb2VzbuKAmXQgc2VlbSByaWdodCB0byBjb25m
dXNlIHRoZSB0d28gdGhpbmdzLgo+ICAKPiBDaGVlcnMsCj4gVGhvcnN0ZW4KPiAgCj4gRnJvbTog
VHlwZXMtbGlzdCA8dHlwZXMtbGlzdC1ib3VuY2VzQExJU1RTLlNFQVMuVVBFTk4uRURVIDxtYWls
dG86dHlwZXMtbGlzdC1ib3VuY2VzQExJU1RTLlNFQVMuVVBFTk4uRURVPj4gb24gYmVoYWxmIG9m
IEpvbiBTdGVybGluZyA8am9uQGpvbm1zdGVybGluZy5jb20gPG1haWx0bzpqb25Aam9ubXN0ZXJs
aW5nLmNvbT4+Cj4gRGF0ZTogU2F0dXJkYXksIDI3IEphbnVhcnkgMjAyNCBhdCAxNToyNQo+IFRv
OiB0eXBlcy1saXN0QExJU1RTLlNFQVMuVVBFTk4uRURVIDxtYWlsdG86dHlwZXMtbGlzdEBMSVNU
Uy5TRUFTLlVQRU5OLkVEVT4gPHR5cGVzLWxpc3RATElTVFMuU0VBUy5VUEVOTi5FRFUgPG1haWx0
bzp0eXBlcy1saXN0QExJU1RTLlNFQVMuVVBFTk4uRURVPj4KPiBTdWJqZWN0OiBSZTogW1RZUEVT
XSBhIG5haXZlIHF1ZXN0aW9uIG9uIGRhdGF0eXBlIGRlY2xhcmF0aW9ucwo+IAo+IFsgVGhlIFR5
cGVzIEZvcnVtLCBodHRwOi8vbGlzdHMuc2Vhcy51cGVubi5lZHUvbWFpbG1hbi9saXN0aW5mby90
eXBlcy1saXN0IF0KPiAKPiBIaSBHZXJzaG9tLAo+IAo+IFRoaXMgaXMgYSBnb29kIHF1ZXN0aW9u
LCBhbmQgb2Z0ZW4gb3Zlcmxvb2tlZC4gQm9iIEhhcnBlciB0YXVnaHQgbWUgdG8gdGhpbmsgb2Yg
dGhlc2UgdGhpbmdzIGFzIGFic3RyYWN0IHR5cGVzLCBhbmQgSSBhZ3JlZSDigJQgc28gdGhlIHRo
aW5nIHRoYXQgbWFrZXMgdHdvIGRpZmZlcmVudCBkYXRhdHlwZSBkZWNsYXJhdGlvbnMgZGlmZmVy
ZW50IGlzIHRoZSBleGlzdGluZyBhYnN0cmFjdGlvbiBtZWNoYW5pc20gb2YgeW91ciBsYW5ndWFn
ZS4gV2hlbiB5b3UgdGhpbmsgb2YgaXQgdGhpcyB3YXksIHlvdSB0aGluayBvZiB0aGUgcGF0dGVy
bi1tYXRjaGluZyBmb3JtcyBhcyBiZWluZyBlbGFib3JhdGVkIHRvIHNvbWUga2luZHMgb2YgZGVz
dHJ1Y3RvcnMgb3IgY29tYmluYXRvcnMg4oCUIHdoaWNoIGFyZSB0aGVtc2VsdmVzIHBhcnQgb2Yg
dGhlIGFic3RyYWN0IGludGVyZmFjZSBvZiB0aGUgdHlwZS4KPiAKPiBJIGNhbm5vdCBjb25maXJt
IGJlY2F1c2UgSSBkb24ndCByZW1lbWJlciB0aGUgY29kZSwgYnV0IGl0IG1heSBiZSB0aGF0IHRo
ZSBUSUxUIGNvbXBpbGVyIGFjdHVhbGx5IHdvcmtlZCB0aGlzIHdheS4gUHJvYmFibHkgQm9iIHdp
bGwgaGF2ZSBhIGZyZXNoZXIgcmVjb2xsZWN0aW9uIG9mIHRoaXMuCj4gCj4gQmVzdCwKPiBKb24K
PiAKPiAKPiBPbiBGcmksIEphbiAyNiwgMjAyNCwgYXQgMTA6MTggUE0sIEdlcnNob20gQiB3cm90
ZToKPiA+IFsgVGhlIFR5cGVzIEZvcnVtLCBodHRwOi8vbGlzdHMuc2Vhcy51cGVubi5lZHUvbWFp
bG1hbi9saXN0aW5mby90eXBlcy1saXN0IF0KPiA+Cj4gPiBJbiB0eXBpY2FsIHRyZWF0bWVudHMg
b2YgbGFuZ3VhZ2VzIHdpdGggcmVjdXJzaXZlIHR5cGVzLCB3ZSBwcmVzZW50IGEKPiA+IHN5bnRh
eCB3aXRoIGVpdGhlciBpc29yZWN1cnNpdmUgb3IgZXF1aXJlY3Vyc2l2ZSB0eXBlcy4gQnV0IHdl
IGRvIG5vdAo+ID4gaGF2ZSBhIHN5bnRheCBmb3IgaW50cm9kdWN0aW9uIG9mIHR5cGUgZGVjbGFy
YXRpb25zLgo+ID4KPiA+IFRoaXMgaXMgdG8gc2F5IHRoYXQgd2UgYXNzZW1ibGUgdHlwZXMgb3V0
IG9mIGNvbnN0cnVjdG9ycyBmb3IgZS5nLiwKPiA+IHBvbHltb3JwaGlzbSwgcmVjdXJzaW9uLCBz
dW0sIHByb2R1Y3QsIHVuaXQsIGV4cG9uZW50aWFsIChnaXZlIG9yCj4gPiB0YWtlKS4KPiA+Cj4g
PiBCdXQgd2UgZG8gbm90IGhhdmUgdGhlIGVxdWl2YWxlbnQgb2YgYSAiZGF0YSIgZGVjbGFyYXRp
b24gaW4gSGFza2VsbAo+ID4gdGhhdCBsZXRzIHVzIGV4cGxpY2l0bHkgc2F5Cj4gPgo+ID4gZGF0
YSBCb29sID0gVHJ1ZSB8IEZhbHNlCj4gPgo+ID4gb3IKPiA+Cj4gPiBkYXRhIExpc3QgYSA9IE5p
bCB8IENvbnMgYQo+ID4KPiA+IEl0IGlzLCBJIHN1cHBvc2UsIGV4cGVjdGVkIHRoYXQgcmVhZGVy
cyBvZiB0aGVzZSBwYXBlcnMgY2FuIHRoaW5rCj4gPiB0aHJvdWdoIGhvdyB0byB0cmFuc2xhdGUg
YW55IGdpdmVuIGRhdGEgZGF0YXR5cGVzIGluIGxhbmd1YWdlcyB3aXRoCj4gPiBleHBsaWNpdCBk
ZWNsYXJhdGlvbiBpbnRvIHRoZSB1bmRlcmx5aW5nIGZpeGVkIHR5cGUgY2FsY3VsdXMuCj4gPgo+
ID4gSG93ZXZlciwgSSBhbSBjdXJpb3VzIGlmIHRoZXJlIGlzIGFueSByZWZlcmVuY2UgZm9yICpl
eHBsaWNpdCoKPiA+IHRyZWF0bWVudCBvZiB0aGUgc3ludGF4IGZvciBkYXRhdHlwZSBkZWNsYXJh
dGlvbnMgYW5kIHNlbWFudGljCj4gPiBtb2RlbGluZyBvZiBzdWNoPwo+ID4KPiA+IE9uZSByZWFz
b24gZm9yIHN1Y2ggd291bGQgYmUgdGhhdCBpbiB0aGUgY2FsY3VsaSBJIGRlc2NyaWJlZCBhYm92
ZSwKPiA+IHRoZXJlJ3Mgb2YgY291cnNlIG5vIHdheSB0byBkaXN0aW5ndWlzaCBiZXR3ZWVuIHRo
ZSBhYm92ZSBgZGF0YSBCb29sYAo+ID4gYW5kIGUuZy4gYDEgKyAxYCwgd2hpbGUgaXQgbWlnaHQg
YmUgZGVzaXJhYmxlIHRvIG1haW50YWluIHRoYXQgc3RyaWN0Cj4gPiBkaXN0aW5jdGlvbiBiZXR3
ZWVuIGFjdHVhbCBlcXVhbGl0eSBhbmQgbWVyZWx5IG9ic2VydmFibGUgaXNvbW9ycGhpc20uCj4g
Pgo+ID4gVGhhbmtzLAo+ID4gR2Vyc2hvbQo+IFRoaXMgbWVzc2FnZSBhbmQgYW55IGF0dGFjaG1l
bnQgYXJlIGludGVuZGVkIHNvbGVseSBmb3IgdGhlIGFkZHJlc3NlZSBhbmQgbWF5IGNvbnRhaW4g
Y29uZmlkZW50aWFsIGluZm9ybWF0aW9uLiBJZiB5b3UgaGF2ZSByZWNlaXZlZCB0aGlzIG1lc3Nh
Z2UgaW4gZXJyb3IsIHBsZWFzZSBjb250YWN0IHRoZSBzZW5kZXIgYW5kIGRlbGV0ZSB0aGUgZW1h
aWwgYW5kIGF0dGFjaG1lbnQuIEFueSB2aWV3cyBvciBvcGluaW9ucyBleHByZXNzZWQgYnkgdGhl
IGF1dGhvciBvZiB0aGlzIGVtYWlsIGRvIG5vdCBuZWNlc3NhcmlseSByZWZsZWN0IHRoZSB2aWV3
cyBvZiB0aGUgVW5pdmVyc2l0eSBvZiBOb3R0aW5naGFtLiBFbWFpbCBjb21tdW5pY2F0aW9ucyB3
aXRoIHRoZSBVbml2ZXJzaXR5IG9mIE5vdHRpbmdoYW0gbWF5IGJlIG1vbml0b3JlZCB3aGVyZSBw
ZXJtaXR0ZWQgYnkgbGF3Lgo+ICAKPiBUaGlzIG1lc3NhZ2UgYW5kIGFueSBhdHRhY2htZW50IGFy
ZSBpbnRlbmRlZCBzb2xlbHkgZm9yIHRoZSBhZGRyZXNzZWUgYW5kIG1heSBjb250YWluIGNvbmZp
ZGVudGlhbCBpbmZvcm1hdGlvbi4gSWYgeW91IGhhdmUgcmVjZWl2ZWQgdGhpcyBtZXNzYWdlIGlu
IGVycm9yLCBwbGVhc2UgY29udGFjdCB0aGUgc2VuZGVyIGFuZCBkZWxldGUgdGhlIGVtYWlsIGFu
ZCBhdHRhY2htZW50LiBBbnkgdmlld3Mgb3Igb3BpbmlvbnMgZXhwcmVzc2VkIGJ5IHRoZSBhdXRo
b3Igb2YgdGhpcyBlbWFpbCBkbyBub3QgbmVjZXNzYXJpbHkgcmVmbGVjdCB0aGUgdmlld3Mgb2Yg
dGhlIFVuaXZlcnNpdHkgb2YgTm90dGluZ2hhbS4gRW1haWwgY29tbXVuaWNhdGlvbnMgd2l0aCB0
aGUgVW5pdmVyc2l0eSBvZiBOb3R0aW5naGFtIG1heSBiZSBtb25pdG9yZWQgd2hlcmUgcGVybWl0
dGVkIGJ5IGxhdy4KCg==