Re: [TYPES] Identity extension for the system F term model
Andrew Polonsky <[email protected]> Wed, 27 Aug 2025 23:34:34 -0400
| Newsgroups | gmane.comp.science.types |
|---|---|
| Message-ID | <CABcT7WDw8Z3+=u=HnUn0_h9zPdXLzAvokfedRsEhv3P6YoKiCw@mail.gmail.com> |
WyBUaGUgVHlwZXMgRm9ydW0sIGh0dHA6Ly9saXN0cy5zZWFzLnVwZW5uLmVkdS9tYWlsbWFuL2xp c3RpbmZvL3R5cGVzLWxpc3QgXQoKUHV0ClRvcCA9IFxmb3JhbGwgWC4gWCAtPiBYCnR0ID0gL1xY Llx4OlgueCA6IFRvcApUKFgpID0gKFggLT4gVG9wKSAtPiAoVG9wIC0+IFRvcCkKQTEgPSBBMiA9 IFRvcApSIFxzdWJzZXQgQTF4QTIgaXMgPWJldGEoZXRhKQpUKFIpIGlkZW50aWZpZXMgXHgueCwg XHh5LnksIGFuZCBceHkudHQuCgpXaGlsZSBJIGFncmVlIHRoYXQgdGhlIHRlcm0gImluaXRpYWwg bW9kZWwiIGlzIG1vc3Qgb2Z0ZW4gYXBwbGllZCB0byBhIHRlcm0KbW9kZWwgd2l0aCBhIHN5bnRh Y3RpYyBub3Rpb24gb2YgZXF1YWxpdHksIGluIGRpc2N1c3Npb25zIG9mIElFTCB0aGVyZSdzIGEK Z2VuZXJhbCBpbXBsaWNhdHVyZSB0aGF0IHlvdSBhcmUgaW50ZXJlc3RlZCBpbiBwYXJhbWV0cmlj IG1vZGVscy4gQW5kIHRoZQppbml0aWFsIHN1Y2ggbW9kZWwgaXMgcHJlY2lzZWx5IHRoZSBleHRl bnNpb25hbCBxdW90aWVudCBvZiB0aGUgdGVybSBtb2RlbCwKZm9yIHdoaWNoIElFTCBob2xkcyB0 YXV0b2xvZ2ljYWxseS4gIChNb3JlIHByZWNpc2VseSwgaXQgaG9sZHMgYnkgdGhlCmZ1bmRhbWVu dGFsIHRoZW9yZW0gb2YgbG9naWNhbCByZWxhdGlvbnMsIHRoZSB2ZXJzaW9uIGZvciBvcGVuIHRl cm1zIHRoYXQKaXMgdmVyaWZpZWQgaW4gdGhlIHByb29mIG9mIHRoZSB0aGVvcmVtLikKCkJlc3Qs CkFuZHJldwoKCk9uIFdlZCwgQXVnIDI3LCAyMDI1IGF0IDc6NTnigK9QTSBSeWFuIFdpc25lc2t5 IDx3aXNuZXNreUBnbWFpbC5jb20+IHdyb3RlOgoKPiBUaGFua3MgZXZlcnlvbmUgZm9yIHRoZSBp bmZvcm1hdGl2ZSBkaXNjdXNzaW9uISAgIEFuZHJld+KAmXMgY291bnRlci1leGFtcGxlCj4gb2Yg VChYKSA9IFgtPlggdG8gdGhlIElFTCBpbiB0aGUgaW5pdGlhbCBtb2RlbCBpcyBqdXN0IHdoYXQg d2FzIGFza2VkIGZvci4KPgo+IElmIEkgbWF5IGFzayBhIGZvbGxvdy11cDogZG9lcyBhbnlvbmUg aGF2ZSBhIGNvdW50ZXItZXhhbXBsZSBmb3IgdGhlIElFTAo+IGluIHRoZSBpbml0aWFsIG1vZGVs IGZvciBhIHR5cGUgZXhwcmVzc2lvbiB0aGF0IGRlZmluZXMgYSBmdW5jdG9yPyAgT3IgYQo+IHBy b29mIHRoYXQgSUVMIGFsd2F5cyBob2xkcyBmb3IgZGVmaW5hYmxlIGZ1bmN0b3JzIGluIHRoZSBp bml0aWFsIG1vZGVsPwo+IChUKFgpID0gWC0+WCBpcyB3ZWxsLWtub3duIG5vdCB0byBiZSBhIGZ1 bmN0b3IuKS4KPgo+IFRoYW5rcyBhZ2FpbiEKPiBSeWFuCj4KPiA+IE9uIEF1ZyAxNCwgMjAyNSwg YXQgMTA6NTnigK9QTSwgQW5kcmV3IFBvbG9uc2t5IDxhbmRyZXcucG9sb25za3lAZ21haWwuY29t Pgo+IHdyb3RlOgo+ID4KPiA+IFsgVGhlIFR5cGVzIEZvcnVtLAo+IGh0dHA6Ly9saXN0cy5zZWFz LnVwZW5uLmVkdS9tYWlsbWFuL2xpc3RpbmZvL3R5cGVzLWxpc3QgIF0KPiA+Cj4gPiBZZXMsIHRo ZSBpbml0aWFsIG1vZGVsIG9mIFN5c3RlbSBGIHNhdGlzZmllcyB0aGUgaWRlbnRpdHkgZXh0ZW5z aW9uCj4gbGVtbWEsCj4gPiBhc3N1bWluZyB0aGF0IGJ5ICJpbml0aWFsIG1vZGVsIiB5b3UgbWVh biB0aGUgZXh0ZW5zaW9uYWwgcXVvdGllbnQgb2YKPiA+IGNsb3NlZCB0ZXJtcyBhcyB0cmVhdGVk IGUuZy4gYnkgSGFzZWdhd2EgWzFdLgo+ID4KPiA+IFRoZSBpZGVudGl0eSByZWxhdGlvbiBpbiB0 aGlzIG1vZGVsIGlzIHRoZSBleHRlbnNpb25hbCBlcXVhbGl0eSBkZWZpbmVkCj4gYnkKPiA+IGlu ZHVjdGlvbiBvbiB0eXBlIHN0cnVjdHVyZSB3aXRoIHRoZSB1c3VhbCBsb2dpY2FsIHJlbGF0aW9u IGNvbmRpdGlvbnMuCj4gPiBUaGlzIGlkZW50aWZpZXMgdGVybXMgdGhhdCBhcmUgbm90IGJldGEo LWV0YSkgY29udmVydGlibGUsIGxpa2UgdGhlIHR3bwo+ID4gc3VjY2Vzc29ycyBvbiB0aGUgcG9s eW1vcnBoaWMgY2h1cmNoIG51bWVyYWxzLgo+ID4KPiA+IE5hdCA9IFxmb3JhbGwgQS4gKEEgLT4g QSkgLT4gKEEgLT4gQSkKPiA+IFMsIFMnIDogTmF0IC0+IE5hdAo+ID4gUyA9IFxuZnMuZihuZnMp Cj4gPiBTJyA9IFxuZnMubmYoZnMpCj4gPgo+ID4gSWYgYnkgImluaXRpYWwgbW9kZWwiIHlvdSBt ZWFuIHNvbWV0aGluZyBpbnRlbnNpb25hbCBsaWtlIGEgbGFtYmRhCj4gYWxnZWJyYQo+ID4gd2l0 aCBiZXRhIGNvbnZlcnNpb24sIHRoZW4gSUVMIGZhaWxzLiAgV2UgY2FuIHVzZSB0aGUgc2FtZSB0 eXBlIGFzIHRoZQo+ID4gY291bnRlcmV4YW1wbGUuCj4gPgo+ID4gVChYKSA9IFggLT4gWAo+ID4g QTEgPSBBMiA9IE5hdAo+ID4gUiBcc3Vic2V0IEExeEEyIGlzID1iZXRhCj4gPiBUKFIpIGlkZW50 aWZpZXMgUyBhbmQgUycKPiA+Cj4gPiBCZXN0LAo+ID4gQW5kcmV3Cj4gPgo+ID4gUC5TLiBSZWdh cmRpbmcgdGhlIG90aGVyIHF1ZXN0aW9uIHJhaXNlZCBpbiB0aGUgWnVsaXAgY2hhdCB5b3UgbGlu a2VkLAo+ID4gd2hldGhlciBldmVyeSB0eXBlIEEgaXMgaXNvbW9ycGhpYyB0byAiZm9yYWxsIFgu IChBIC0+IFgpIC0+IFgiIGluIHRoaXMKPiA+IGV4dGVuc2lvbmFsIG1vZGVsLCBJIGJlbGlldmUg dGhlIGFuc3dlciB0byBiZSAieWVzIiBiYXNlZCBvbiBjb21tZW50cyBieQo+ID4gVGhpZXJyeSBD b3F1YW5kIGluIFsyXSwgc2xpZGUgNTIuCj4gPgo+ID4gWzFdCj4gaHR0cHM6Ly91cmxkZWZlbnNl LmNvbS92My9fX2h0dHBzOi8vZG9pLm9yZy8xMC4xMDA3LzMtNTQwLTU0NDE1LTFfNjFfXzshIUlC eldMVXMhUzhhSmgzNTZ3dm1EZGNIenVObl94LW5fcEFJTkV1QjlPb3JRUzR2cFZWUHh6cGs2ZjFG cno2YlhVMmlLT21XVTJlSm5maW9mNFV2Q1E3UHo3RVkyZThpUVluczAycDhfZ1RCN0xRJAo+ID4g WzJdCj4gaHR0cHM6Ly91cmxkZWZlbnNlLmNvbS92My9fX2h0dHBzOi8veW91dHUuYmUvNkFvOXpY d3l0ZVk/c2k9NUZkQzV0NU1ueWFqbWNoeiZ0PTQ2NjBfXzshIUlCeldMVXMhUzhhSmgzNTZ3dm1E ZGNIenVObl94LW5fcEFJTkV1QjlPb3JRUzR2cFZWUHh6cGs2ZjFGcno2YlhVMmlLT21XVTJlSm5m aW9mNFV2Q1E3UHo3RVkyZThpUVluczAycDhhejRPS1NnJAo+ID4KPiA+Cj4gPiBPbiBUdWUsIEF1 ZyAxMiwgMjAyNSBhdCAxMjowMuKAr1BNIDwKPiB0eXBlcy1saXN0LXJlcXVlc3RAbGlzdHMuc2Vh cy51cGVubi5lZHU+Cj4gPiB3cm90ZToKPiA+Cj4gPj4gU2VuZCBUeXBlcy1saXN0IG1haWxpbmcg bGlzdCBzdWJtaXNzaW9ucyB0bwo+ID4+ICAgICAgICB0eXBlcy1saXN0QExJU1RTLlNFQVMuVVBF Tk4uRURVCj4gPj4KPiA+PiBUbyBzdWJzY3JpYmUgb3IgdW5zdWJzY3JpYmUgdmlhIHRoZSBXb3Js ZCBXaWRlIFdlYiwgdmlzaXQKPiA+PiAgICAgICAgaHR0cHM6Ly9MSVNUUy5TRUFTLlVQRU5OLkVE VS9tYWlsbWFuL2xpc3RpbmZvL3R5cGVzLWxpc3QgCj4gPj4gb3IsIHZpYSBlbWFpbCwgc2VuZCBh IG1lc3NhZ2Ugd2l0aCBzdWJqZWN0IG9yIGJvZHkgJ2hlbHAnIHRvCj4gPj4gICAgICAgIHR5cGVz LWxpc3QtcmVxdWVzdEBMSVNUUy5TRUFTLlVQRU5OLkVEVQo+ID4+Cj4gPj4gWW91IGNhbiByZWFj aCB0aGUgcGVyc29uIG1hbmFnaW5nIHRoZSBsaXN0IGF0Cj4gPj4gICAgICAgIHR5cGVzLWxpc3Qt b3duZXJATElTVFMuU0VBUy5VUEVOTi5FRFUKPiA+Pgo+ID4+IFdoZW4gcmVwbHlpbmcsIHBsZWFz ZSBlZGl0IHlvdXIgU3ViamVjdCBsaW5lIHNvIGl0IGlzIG1vcmUgc3BlY2lmaWMKPiA+PiB0aGFu ICJSZTogQ29udGVudHMgb2YgVHlwZXMtbGlzdCBkaWdlc3QuLi4iCj4gPj4KPiA+Pgo+ID4+IFRv ZGF5J3MgVG9waWNzOgo+ID4+Cj4gPj4gICAxLiAgSWRlbnRpdHkgZXh0ZW5zaW9uIGZvciB0aGUg c3lzdGVtIEYgdGVybSBtb2RlbCAoUnlhbiBXaXNuZXNreSkKPiA+Pgo+ID4+Cj4gPj4gLS0tLS0t LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t LS0tLS0tLQo+ID4+Cj4gPj4gTWVzc2FnZTogMQo+ID4+IERhdGU6IE1vbiwgMTEgQXVnIDIwMjUg MjE6MjU6MTkgLTA3MDAKPiA+PiBGcm9tOiBSeWFuIFdpc25lc2t5IDx3aXNuZXNreUBnbWFpbC5j b20+Cj4gPj4gVG86ICJ0eXBlcy1saXN0QGxpc3RzLnNlYXMudXBlbm4uZWR1Igo+ID4+ICAgICAg ICA8dHlwZXMtbGlzdEBMSVNUUy5TRUFTLlVQRU5OLkVEVT4KPiA+PiBTdWJqZWN0OiBbVFlQRVNd IElkZW50aXR5IGV4dGVuc2lvbiBmb3IgdGhlIHN5c3RlbSBGIHRlcm0gbW9kZWwKPiA+PiBNZXNz YWdlLUlEOiA8Q0MzRjgzNTYtMEIwNS00QTY4LTlFODctREQxODFBNTg3REI0QGdtYWlsLmNvbT4K PiA+PiBDb250ZW50LVR5cGU6IHRleHQvcGxhaW47ICAgICAgIGNoYXJzZXQ9dXRmLTgKPiA+Pgo+ ID4+IEhpIEFsbCwKPiA+Pgo+ID4+IEknbSBob3BpbmcgdGhlIGZvbGtzIG9uIHRoaXMgbGlzdCBj YW4gc2V0dGxlIGEgcXVlc3Rpb24gb2YgZm9sa2xvcmU7Cj4gPj4gbXlzZWxmIGFuZCBNaWtlIFNo dWxtYW4gYW5kIG90aGVycyBoYXZlIGJlZW4gZGlzY3Vzc2luZyBpdCBvbiB0aGUKPiBhcHBsaWVk Cj4gPj4gY2F0ZWdvcnkgdGhlb3J5IHp1bGlwIGNoYW5uZWwgYnV0IGhhdmUgeWV0IHRvIHJlYWNo IGEgY29uY2x1c2lvbjoKPiA+Pgo+IGh0dHBzOi8vdXJsZGVmZW5zZS5jb20vdjMvX19odHRwczov L2NhdGVnb3J5dGhlb3J5Lnp1bGlwY2hhdC5jb20vKm5hcnJvdy9jaGFubmVsLzIyOTE5OS1sZWFy bmluZy4zQS1xdWVzdGlvbnMvdG9waWMvQ29udGludWF0aW9ucy4yQy4yMHBhcmFtZXRyaWNpdHku MkMuMjBhbmQuMjBwb2x5bW9ycGhpc20vd2l0aC81Mjg0NzkxODhfXztJdyEhSUJ6V0xVcyFVZjg5 SGI3dVdqdGJ6NHFVZUZiTUNWd2Z4a3V5ZTJscEIyN09pNHZDaGhNVjZ5TVBwQTU3amwyb1puQnQz VGFPT1lhN1VoalFUejE2ZFBNVVpvR3RHdWJRZXNYVCQKPiA+Pgo+ID4+IFRoZSBxdWVzdGlvbiBp cyB3aGV0aGVyIHRoZSBpbml0aWFsICh0ZXJtKSBtb2RlbCBvZiBzeXN0ZW0gRiAoMm5kIG9yZGVy Cj4gPj4gaW1wcmVkaWNhdGl2ZSBwb2x5bW9ycGhpYyBsYW1iZGEgY2FsY3VsdXMpIHNhdGlzZmll cyB0aGUgImlkZW50aXR5Cj4gPj4gZXh0ZW5zaW9uIGxlbW1hIiwgd2hpY2ggaXMgb25lIG9mIHRo ZSBwcmltYXJ5IGxlbW1hcyBjaGFyYWN0ZXJpemluZwo+ID4+IChSZXlub2xkcykgcGFyYW1ldHJp YyBtb2RlbHMuICBUbyBiZSBjbGVhciwgdGhpcyBxdWVzdGlvbiBpcyBhYm91dCB0aGUKPiA+PiBp bml0aWFsICh0ZXJtKSBtb2RlbCBvZiBzeXN0ZW0gb2YgRiwgaXRzIGluaXRpYWwgbW9kZWwgb2Yg Y29udGV4dHMgYW5kCj4gPj4gc3Vic3RpdHV0aW9ucy4KPiA+Pgo+ID4+IFRoZXJlIGFyZSBtYW55 IHBsYWNlcyB0aGF0IHN0YXRlIHRoZSBzeXN0ZW0gRiB0ZXJtIG1vZGVsIHNob3VsZCBvYmV5Cj4g Pj4gaWRlbnRpdHkgZXh0ZW5zaW9uLCBmb3IgZXhhbXBsZSwgdGhpcyByZW1hcmsgYnkgQW5keSBL b3ZhY3M6Cj4gPj4KPiBodHRwczovL3VybGRlZmVuc2UuY29tL3YzL19faHR0cHM6Ly9jcy5zdGFj a2V4Y2hhbmdlLmNvbS9xdWVzdGlvbnMvMTM2MzU5L3JpZ29yb3VzLXByb29mLXRoYXQtcGFyYW1l dHJpYy1wb2x5bW9ycGhpc20taW1wbGllcy1uYXR1cmFsaXR5LXVzaW5nLXBhcmFtZXRyaWNpLzEz NjM3MyoxMzYzNzNfXztJdyEhSUJ6V0xVcyFVZjg5SGI3dVdqdGJ6NHFVZUZiTUNWd2Z4a3V5ZTJs cEIyN09pNHZDaGhNVjZ5TVBwQTU3amwyb1puQnQzVGFPT1lhN1VoalFUejE2ZFBNVVpvR3RHcFFT dzNJaSQKPiA+PiAuCj4gPj4KPiA+PiBIb3dldmVyLCBuZWl0aGVyIG15c2VsZiBub3IgTWlrZSBu b3IgYW55b25lIG9uIHRoZSB6dWxpcCBjaGF0IG9yIGFueW9uZQo+ID4+IHdlP3ZlIGFza2VkIGhh cyBiZWVuIGFibGUgdG8gZmluZCBhIHByb29mIChvciBkaXNwcm9vZikuCj4gPj4KPiA+PiBBbnl3 YXksIGRvIHBsZWFzZSBsZXQgbWUga25vdyBpZiB5b3Uga25vdyBvZiBhIGNsZWFyIHByb29mIG9y IGRpc3Byb29mCj4gb2YKPiA+PiB0aGUgaWRlbnRpdHkgZXh0ZW5zaW9uIGxlbW1hIGZvciB0aGUg aW5pdGlhbCAodGVybSkgbW9kZWwgb2Ygc3lzdGVtIEYhCj4gPj4KPiA+PiBUaGFua3MsCj4gPj4g UnlhbiBXaXNuZXNreQo+ID4+Cj4gPj4gUFMgSGVyZSdzIGEgc3RhdGVtZW50IGZyb20gTWlrZSBh Ym91dCB0aGUgZXhhY3QgZGVmaW5pdGlvbiBvZiB0aGlzCj4gPj4gcXVlc3Rpb246Cj4gPj4KPiA+ PiBMZXQgQyBiZSB0aGUgaW5pdGlhbCBtb2RlbCBvZiBzeXN0ZW0gRi4gIExldCBSKEMpIGJlIHRo ZSByZWxhdGlvbmFsCj4gbW9kZWwKPiA+PiBidWlsdCBmcm9tIEMsIHNvIGl0cyBvYmplY3RzIGFy ZSBvYmplY3RzIG9mIEMgZXF1aXBwZWQgd2l0aCBhIGJpbmFyeQo+ID4+IHJlbGF0aW9uLiAgVGhl cmUgaXMgYSBzdHJpY3QgcHJvamVjdGlvbiBmdW5jdG9yIFIoQykgLT4gQywgYW5kIHNpbmNlIEMK PiBpcwo+ID4+IGluaXRpYWwgdGhpcyBwcm9qZWN0aW9uIGhhcyBhIHNlY3Rpb24gQyAtPiBSKEMp LCB3aGljaCBpcyAiZXh0ZXJuYWwKPiA+PiBwYXJhbWV0cmljaXR5Ii4gIEluIGEgdGhlb3J5IGxp a2UgU3lzdGVtIEYgdGhhdCBoYXMgdHlwZSB2YXJpYWJsZXMsIGEKPiA+PiAibW9kZWwiIGluY2x1 ZGVzIGluZm9ybWF0aW9uIGFib3V0IHR5cGVzIGluIGEgY29udGV4dCBvZiB0eXBlCj4gdmFyaWFi bGVzLCBzbwo+ID4+IGV4dGVybmFsIHBhcmFtZXRyaWNpdHkgc2VuZHMgZXZlcnkgdHlwZSBpbiBj b250ZXh0IHRvIGEgInJlbGF0aW9uIGluCj4gPj4gY29udGV4dCIuICBEbyB0aGUgcmVsYXRpb25z LWluLWNvbnRleHQgcmVzdWx0aW5nIGluIHRoaXMgd2F5IGZyb20gdHlwZXMKPiBvZgo+ID4+IFN5 c3RlbSBGIGFsd2F5cyBtYXAgaWRlbnRpdHkgcmVsYXRpb25zIHRvIGlkZW50aXR5IHJlbGF0aW9u cz8KPiA+Pgo+ID4+IC0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLQo+ID4+Cj4gPj4gU3Vi amVjdDogRGlnZXN0IEZvb3Rlcgo+ID4+Cj4gPj4gX19fX19fX19fX19fX19fX19fX19fX19fX19f X19fX19fX19fX19fX19fX19fX18KPiA+PiBUeXBlcy1saXN0IG1haWxpbmcgbGlzdAo+ID4+IFR5 cGVzLWxpc3RATElTVFMuU0VBUy5VUEVOTi5FRFUKPiA+PiBodHRwczovL0xJU1RTLlNFQVMuVVBF Tk4uRURVL21haWxtYW4vbGlzdGluZm8vdHlwZXMtbGlzdCAKPiA+Pgo+ID4+Cj4gPj4gLS0tLS0t LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tCj4gPj4KPiA+PiBFbmQgb2YgVHlwZXMtbGlzdCBEaWdl c3QsIFZvbCAxNTUsIElzc3VlIDMKPiA+PiAqKioqKioqKioqKioqKioqKioqKioqKioqKioqKioq KioqKioqKioqKioKPiA+Pgo+Cj4K