From 4720d333efbc8c94e720a7f740ead4127da66531 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Mon, 17 Jul 2023 10:56:57 -0700 Subject: [PATCH] Another draft --- papers/hatra23/hatra23.pdf | Bin 399217 -> 399231 bytes papers/hatra23/hatra23.tex | 22 +++++++++++++--------- 2 files changed, 13 insertions(+), 9 deletions(-) diff --git a/papers/hatra23/hatra23.pdf b/papers/hatra23/hatra23.pdf index 128f4f918929b1b1a74764c049bef089d38978f6..36c86f5e07aa066b75d6d2666504c48447aca0be 100644 GIT binary patch delta 10316 zcmajDQ*b2=*sL2T6Hjb=f)(2~R%~lxW0DoywrxzjVoaP&Y}=Sv``hPKom2n5*%!}E zzkS(NZ*||+;eFNNHB^3s;$}}~#iIko>KeIjaG`=`%2(Qwt-w_>az!b=F2JsICFZf! zs|_~{;nA)pEnw|IT}gY7G6(`vtpx0GM|DdI5kz(aU1ILuE2r7pBa1VWU%&nCM&9H? zJ*QpTp>MEVJIBau-Z*Z7Qw`QOaMUs?GJ2~bR$5|{FZztj+pjB2M+0*HT?akL>Pji2 z(f%a9U0Iw5EWH68pKnVdd~Cm*izL;x;A!3~`8zs3QHCH{B{0%u=~Z&fThbUbEu@lu zd3`~Sy^H?z?|FA?(&T%+mOgTRyiLbUUE7VGcskZP_NX~)6*wJSmG*hNeBaxJWoUAXooNhH6f-)+BSQf%y;wMOS<5$tuD8=MZt6xf+KBHnT$%usQ0&b<<&s{6$ zH}(D41O~(9uCeAmgDn#O=td=QJKE@>WsAG6yFE$##h-9k)2d16vIVg}KHg-TWSj-k z2#OOwj?gMAiXthtieMlJAi5mqxPBD}bkugfRdyba z#iKZdaodD@K4|Zc{d;n^LM_XOBUoKB#@N1@UCVoB-Bs+}RyJT4$~}<90+MD1h4^uT ziL|~1mp0Slv&}n+M?lbY$16wkY(^FxG4~v$Q~dj5qh7NTy_|aUsY&l12YE3+3xwtY z6i?xaov(3uzjWyhmIm_|`2YO_SEII<105b@OxaOtzO2-ntj{L7E}i=>oVOfsG=hcM zz!naic;hQ}?VOtf-h4P-$*R1jCfJz~uCr;XlXyHuug2<51)wE>;Ef_-R!{Wmoco#1 zD_>-4QgzGdUXA(z)bwl%_>KE-d(Cx>;=*Q_xBkCyKh7RO4@ZfdfR?aE9olUpe`#K`!-N@bIGkVbDa%UkZpe~8z1LgqXI90e3@lcj>9H+VuWmd<{YX4C zJ|E4AaeRQ%9tbwx=?q0r*x}dh#h=2LN;AvrF0-p2DxnF^i6w>1meTk{&IGt3w80{w z@D`Sz;#F-I`c`c&9u($SS?YN0@0%#mqfR360Nx;*n&zTdSK3$DZ z7i^(ZD*z33MKLci>NIaJhZnw#F!L1t{1bN1;T`}9{um`aBAWGu-r-7*$B=RyV_RCLJSqDTwOP!CtIWHk;mA}0o9n(tW{|J#; z)yUciKhjI16XdxJ2!5m-Uus=w$VE4AL#eCOrLgoAXJRq$J0Q~^XblLCu%T;^#=m6z z*j%u;O5Ro44>exuvC%UYoV5x1o)+y_&W1xziv406i@OiVnd9#Q2?E)eva+NJ2Rp<< zhCxWEPP53PZf;hOt>q(@%fG2?q=}il?x&}SeSLJXRBzcj33vj5L{owu18d+h}f3l)3-Q-H5UJGd=JV`4_20ZAug- zcvk3qmYojvFZtLYy=f&oY@TQ(Y$2hhV!$4|@AQorU7l>@VF!&jBWM0O@?AfwWrC4* zOzs&(4`q!>_U%o099;C~yeU^#)SBT%fRg<3cOS?u!jTa$huKq31Ah%n`fraeBoKGG zoJ<<5E^+bn-!a=E z2=nJOABXQy5}X?kbwU7o!cO!wa?_dbja@2X;Lda|{ZZ}1Us-rJlSO3&I%U4mbV&Pd zy)hm{?BTDa@HDP$#sww)XKBWR$ zRCHEA0plOVN0qCQ3xB=d6di`#p~@ZT&!1Jg0w&3Bc0Liu;c@e{V#zkYuhCrL9vR<# zZKe|yoS)053Q>s&6(a^xYzm48IigsgLbV_Nu8@YU!~k%Fp12e=4p@PMJD>=7O`Y%M zI!C_7lsCWevmHm82F z0U}PTfIAQqeUM_G)vUDg{rxgfU?a@J^k}GX6gqJ~GEjgnwP0y^Wv6`OFG)vO*XHYQ_q>CiE}OLK~k42!l+zBujpKN?EHg zz6~O|I=4vWBjLBO+SmH!$CQ`d@26{@4^xLl9$^fMI7Mbg(D$9-H;UjIt>wrG)emB) zR%xFzZivnYj;|fH){2YjL`_#agX3h>G)BIaL_j{wmoCfRr$TupP+b_4dQMqd<&GHG zR|lG9^A$g?gWTG8>w@lB4oRxdE5+0a#M zNr{Wq#XRQP|7eF$GbgVFZUH29(3613VGiCfmHjvrM~y1b6`=3c)O8%k0*0JK>o|D8 zOr7Po{Zz2oI)lr5lZj1-8yGnm4t<+UhjKer%Qwa3QZ=wU5CucIig9dKpSO1?R3I=} z=;TGS1=H8XB3fw%&ufC|k0L)x%DNZ`;eMWqb$G`Z+O}hYV~ouF%xOtc0jA!7w-euR zbf7dy{m+(dA4uXU_kKijM3mTt*Q`%EjvWCR3M@jRX3lMh$$LH&xW$IxPkS~>6$`|k zlM0Y?yTwYNvoKoOAB42)+L3BOzaSuh-gnykl|I?`%QnnwS%|lm1yGujFrk-@i-i%h z6$&fosWGpFs)VT3h>R?uU8A5ho4pmX5YxDdotM3-0cwl2m^4(EAZ!@1l&{!wF440( z7o+IRCE9Q%r5%^l(L)?P1L_6S-my`|FOo_12_;)CwKsG3Cswxhhht2;@zwZLCzd5l zW5LaK7)xd$$??tVrnz0%>j9|w%&yH_BIitxix^Fv3UcTKf45Z2b{|ruDU4NTV9i9j z7EOj`f_k9uIh;0#*hzUDbp}A_cp&_53 z)g8S|l7}Bntqy8j^4|D2k>?ET)&1mZ-E&=k#QCNdWEd1$2~(2tn0=J~Z={ezHRMy@ zdh|P-IfAc&6*yi0EPkSgv1)Ca3(a$({C7359@yp z4+@^KsG%YRvx<%;PPyFgbp;&a=u46qdnB^RO!0fGLM4ilv6#1Cr989kaW~n$h5wBj zR^C=>+;4Rm!{Brs7re5DhH)Mf*OstNF&FG zXh9IwaE^I)5RkFiuXv1=476G zBxJk@zQ*B4uiT@gT7ai}_5C?F2-K|;m4869=lJN@vq4qO6hjWsNWc=v%JgMe6OT)& zSzBDp{$iw0!Po;v!F>8)Rx2D<;y)Qqq5Ip@zNzf&ZuTi(KbbzrqnTR`{44|K$NHdE2kC~$;eYLBJL|8`bM`2w)zx97DqFBF+ zGjN3~XE$2SPK)jL(hEG}zt6cDwQPWWDhN|M{54^qJ~8IAJ=47ACCV+aq;2$pGtF!k1`|`mzjkLJ3Bis6953Y(_psO-kj&I)hZW)i5EGWLKF(&K5YGtR2#<%oi7eQM?6X!!7Kcn>B1T}NR) z<97AT83!@zd5jT5=s}W4&)y2{;4%~!*1QFLbJSyeP)Z6O_E79IzOG@A@i-jTB?wg1xb{Zg+;oh&2ijO+T&$UeMHdML~+6D+QWU_9GS>{8rE$YvZ$WW zvLK9I-YGLF7E{8B@mL7`SEsfhhw)K(K_Z?IgCsSsoR^Bfe zyJN8iskXZf_)TijyQ5i^EXV|l$IeT{Y@3vjdSd>Xf_6u}@8~%zi{dCD{ug3kOy70wbvVh+ zS~?In>w#A1*u}u@LPtl)sfiPwo&U!Vd5N7k>hb1Bd6Pqd<0=35?H8_V5QXc!vE3Rb z8NM+KM5h+zW&4=w_Ter<&kJ@%Pk{+h{KY44nLu6vHC`-KH2n}s77n6|oA)CXSWNfW$?hz<1wi(9ZP>dkNiD5yVNv(?MwF!US# zGrYg$T*$|K*W4{DF$5b24+0*_(9jW%`3eDzN+7-m+7UN{RxBgoVz`E*6ct^@@N9JfZHiZuV^;C2S!05n zf2l^d9#QGkplxG1NRbKBsJX$9DA|~#JVmrIhp<(r>>0C6U=sE>MHt$Cn)TYt3g(lW zz*qk*eW9Ol88IpAvHoUeCMm~admJR#=GvtX6rb;io<;|F^d<8^x4v8p#zuTGQw_M` z6~RWALGKFPurJL+eIsGAwc`?3hl-ZFF?)Z;>=hf9=}?RUaj!Ao9Hzo(UCBkV2d9$g zuh>VBx2&SV4>%24h=);PHoS38DvU5}T+y(_?Nw{lgVpyZzadlG_f<$4*JUgOk; zA1bnmtCt?zM# z03q1FJDdItQbnf9fm7Xp@6VV=H*`ji;U!iAbK4Q+IzYL}+iO#J`b}7DO_l4z9jy`X zG&!~tArqNM@JJU>+0pumd-?k7)FKh9ZaZ5YN)}RjXRiDA)22(du-`KCWz|0YK03`lPB0KJZhni!K=+{Zu1MJu;teARcQi$~-B*Dk;dgFhSiw`=!Z z8xM({Ls%sxwG+%}g*q`ELtGcHW!?();B0~PlMWu(9P1>vl-}9;zUtl_8HmEPmG7~} z#e$X~W^VD^l4G%`W;}*KC*d2vH}$>emr0m;ss8k?+!^Gpon4MsC^)b1&kXuoofZDA zuPo%tFN;C4t@<{^B?#M|5^PilUtpUh)RDIbo9>wNcZmTh`}uIu4X;G(qI z97iiir*N*B2HaM)%>#F^+V-t>cQXr}Z>QXRVFEFoWjpqn*8iRqpu8N$sdVptu(7y+AC&X|~DSOu*Kcua;z%iFGO)T*VS zI1bx{+(BwfNfR%REVwx;Md+H*YFJX%@3&22@UikI7?M~cz9uOESVSf}jsc$C6nlIY zeWwAK-SL2H3W)_~Nr`wILHOiX=G=x0f_f0+D_1|_d58xC;(6#}kDU%O4r@cKSaaq) zo@(lV3FBd`$aR&3LBVWIu&8_Bm7GaTBZa8x6Kr2vm88mddua4@#CE8gAu$OwDldFM z)4eVX`t<~zSY)CBy+{QUcErfr9Pjr)Fr(=N-duGEJO%dOX(;j?xX?LxNDp3vB0mu1 z5FU3Br8%w;FH+BQMAGGK{Cr)g-ti4aLJs^&gufrmAFK%x6Q1~dsQr+E$eS0b{B??k8RQUl$kU7xVzxOKQ@&P%_&t-i) zVL^K$ORb2pfjJmN8DbKpN$NPFDI}m`@f8c0Xov>J0;IgAFsgnYRTQ*y3$eSUb zz}()$wF5%RusAzKdxTl4-^A5ME5Z_^?1OMgjy{ zo3f5P&(eC=5unfJhZ8hH=(^`{wKICq^b7mZOo%Y$r`z+q;y;#GqK6T|)Fpyk{4u!Z)_ZtyQt+qwJ1Prd%tJ&?Tn z6WpA6{8OrXf83(^&5c{Tp&F#CJWGq98)-(4=9A3s@p&LCpXc9O8zOL~ufgVtc_^kNL6dV3LLMpdqwjY715?r|!{nyDyo;EWt z4;4=Q-)rPm5=6~-=yd2<=v3%L=!~QkGRuG4ajFRIWHb3eqyVuy+&)MzZu^7zpc%8n z$nVs>dLP$Uj3jEzT9;Es(OCD++($@urrtMrhN**_$UwbVB84xxcU=7CB3TLTK+Kau zNT+Hp#*KAvB-EH_~iIzr_nkF@PeFBz?sJU4zo)4`<3L$&8=!-e|gY>jl-*ABC4@x z&Dt?L;6(RE#on5Ps%D)!B$BFwxX{JWroxLyZ#GRPS^1dv&-?*yqAOTf=-}bRhpmHH zIIW5O>K(L75?6O%f80tCd+2V(cGjos$inRDk5?LblNR$7YV$+E1dtgdtXu&3Z2KvkeZI99o~WDJ9dTb)t3#nRr$Uaq)9~AmNBsa%>rzz?AH%RX zCQ*0dmJ#D3?zqr6y=0U${0iv+NhE3|7H@1!n;+y9c0P9SwLF^XtuuKKICXHn4H8{U zx0%~SmArL2=@TdZB#c1L;Vu6%rf`)25`;kVsA-EKABCe^aDHUB7o^<)WFis@=tqEy zaS96w<6jW@or8bv6^Hm^@d&4uSX)&eKJmKBs<^3Ll-o2kc;edKhih&5VD<;>IXi!- zw15D58WvpFgPIzu43lJSm560k4cNfUPS-^1>?#B!eT%iSDzQZ|$4PyHF*)|wN-O4v zl#;X&yGiCbm3$~G@q7X3i*jS=>r{-d30x^>Y7C7Gk_`yvc(*0Wxu%0X3mq&9zEGl} zNQ5xy$+uvJQ236&1gd?8j9Scz?-J3EDxirXMqqZtqdtxqK4&r48U>PBSHx`#)C^?} z9hui%lf^-jHA6SET2YAXcY>nE{X0rIzK|2ERw5)x0;t6%Yui}5lJ?ZF%vFsIvK%ty@|PHhdHQ_l`g1WT5ZqvlX>s{$4qaN6 z4uf3D)8n?I*_@~7M@VVry#+AGc3m_{_l6m1T0B{ot-yB&S&B*Ie~1}royf5>>BLx` zr7c?YNAe6v!V*~+&@Lw>1iJ#bD?mepb=1BUvW0>GC;EIhr^>$aXo1Kb%2R+vkKK+B z&lv&pI&O#gK~~F4^+W;4@WRaBxx1w=2MP{BVODD8Crmyax7Lo|ZZaaFEiDJr7$TS@ zfe^l`lY*EpUD6?W>AJ8|-IJyclEc@DMx-aLOmj$`%Y68Dyry!&YrO9)6I7YB#QRln zN>e*iZH~?HV?3#8M<`<0SN<}5In-Gk>H^oDGhN`sFvG8J7y?Br??vaF5sDpCR9y!K zmPsqpj+wy#$yJu30Sz~BY)_9BH!6Te92n^1qMxLAM*&8@_fPh)SFe(GL7Xn(NR8QJ z0OBWEA<4FgQK-{?r;>(91tGcNpra(^sdG(9mfsS+wQW2#tm?PNLghOIjZ>)T*9JZn z%dW6Rk0!93uwO3sweal0+eZ*2`f}zSi2+&TjCOg{WCJ^EnL7s#P|t<32+@(V7FHlo z3iF;M|^d)P48gT z$Mm9h`-Z6_7yb4k$StCvqQOScY2y$q@C-HoHho#IaeYP*uSxD&amW2zgfu)^sdw3r zul-C5id30qaSC3hi&}Vkt*_$mu)Ebz#g~l7fr$V1m>KE6*@{WvmsAfp^LMdlxMRNX z*P;70m_X4d_)O8t<>SbSNwI68#vs{av9Dh{gugQ<*1dBMv`=i%DZ5n1XCk-w zE&I&xxf;&mlRV|)^KSDt9Ie2vVVUsJH~4hw)Tik;gA6Vf^T}wph+eYRF5%ssdna2cSlYFu4f$5fi|OU;>+uN zj^|cS;eAs}qNIAhW4ZMmeE`a|{hXWqIf2PI&3PX6NH@f}ArtG>M~r)>y>S*8ZqNZ^ zA}kouPH&<$K zIVs-7-(mK-1waFGOo}^l#D`fmP8>Nyc$3Z}TZ)yCn^WSA$tGXGhei$#CTo59tWo)j zr|g87a?j*yf^G1#ghV%wF>OsK!hCa~-17)P%J#kU4;`f4z@r1j^as}~Y6sj`&wS8F zlV~IfR+dtpzkrwbzlnqOXJ0Ep%tZXltkGhU{wRtQ9|_wVbl$%>N`s3l$8NcPAGQJ{ zaUDG$XAX_T5(_3cm8%t;nf7dIJ zlThfj_S_Ta)(0;}XY|$%;@|_bl`oRnZDmZ;;J&C!pC9+jhh4QM%^WF(YCS!Ad#(l= zuf1BF4w)nUj*X18C zMrj7y(^s=hLty0%x#wReXrQ|w14W_(%t(ts{cu}K))cQlu2bv&lTWP;n{}Od!%G(8 zi`Z6Ttc^w);caNhOoY_ZY=I9neKxj?|JZml6E9ziXXc=XqULD;Wdb~f)DA7^28KX3 z>w+x>gFBY5cuM<}>G00!A4Cg^d`}4U#(7NjZ{#j-s0Al?0ox2Nbu^#i+mJY^+4!ET z1rq;r1BJRj0tXqkd8pfH1&O%WGjFw?rBA!M!hSkX8jQhgjc|w*dIbztZzHZ(_rLcM z74Drf2rZEma|F^mCI#ERRjfjRD*Slq&Tx=V?7 zHg$=^7;|`9iLc?5n<+>v;_eeF9SAPrDMWeq3oQ2wwG=35(w+2v22!1-2dx`aAMG(5 zH59RE(yvHVu>I0o}Nx!bX73*qqZQQ zwEWRq8hm^G&Ezz7^ZN+LR%4pxl-7wt*U=A-NuhF72O*c*B`5w?_PyOHLZyf!j&fe-^<_@3YlCnv~kh z0_XmBFuc#tt=lhjs3EI0cZJ?OCH;%Vwhffq>dDivB4qgaD1LeKM#K2Rm zbbM?$XH{Ntb}3dVHgPd-HeN{%0Duc1%F4>a%E>9o%f%tZ#wA21@PD-!{C^_|I~!+u z;{hx^hG3{tYN7ZzS*P- zAWW>V?`i8O^JzNQSIJdU;!~YUR6WOv>&nnMLc7R8YgC<}CMXDc&IC4RCkR;^4rxOL zN**0DQ3Wm<9riDJ@m?4Ax+yv89yugNKeTKD2$_B-)NWKgl8*~otsfo}fSL?I0RrIJ z0Z3-(Vcw~l>6vQCiz?6>DyaSyA-WX-M5CbsbOB;?YTu?ayxkK@U7k(jN)yl^@dACU z1ElZ*Xsp9jtpiQ0L&*^a$bO4ye m@J+9wcIi6uV+t(#0>75UxtT753rF^i6M#rfEvYPp_`d+?@yI^_ delta 10289 zcmai&Q*@pU)TU!Mwv)!j8^19c+fLKicAhk9Y&N!SHntkuwi{=@^&iZdnUguV4)%TT z^S$=&W%%nJs(iZwn4-hVZ+n7;o5wrWjFgER&}H(psjoS~t#hj@Suzd2@wdmgpdi#h5`-GD+^7FpcBGL}iVOmp&g(#I|vtM@;w zsp%2+4lFx3sN`7mX_)1~4-cL_N8Q%HkeXVZoUN2ta`L3_v=15fJ$={H z7q&wx-4$tt9MUc7;wkqhzpbjjzbJ1lU8K;(Ow|iq%4v>>w~+$;7H{oWu^LK|IVp@7 z3v!ShnW1;C#U=&2OezCdX$xy9o<$4{Cl=SlDw2Y61!^lxzb?_4?8n@Fm|8lY%HXE1 zsW$Gb2^kvYTdH(z(k_?hCW@g_pCY7e_;-hcmp1$X+p`_7bZQlO(|sh&DUCb#_4j|u zO+?&0qpn+M@XA1pU}qX?b);>)Imc9EanLjg{KlP4*G}GS&Psx5UGqgGPKyAFZ`BHe z0M#w1W4F-6g8rooo{?H*(0Z6l!4AiXylk7d&LywUBX3Z4zYc>~hvlaI5`%UdGEa{VaW1s+uG>C)G|%60%nPt)wcM}YxL$wA8+tV#c0t8x z&8@RXQu?EAgqb{>Cx1^IyQFnf&|!9MY5FyeVz3uti=)$%b-fDdRMG~_um z3^Hjt!K}$H6XbL%UOpOLUhOE=`wOki>mf^_>e$Lem5^PF$pNXa9z1>-c3bKk7KI0z zcNYh|w!p8}siKYMKBMd=Row7Mg)Dlm+{!$AeIKox7+ndmnxs}3R9VBtgio2C&=-(9 z?s$fT?Bu?`hjga6+ut5YHVN1uG59Vafh2J|H7JP&R+-=1MNR9Cd5v=*VsY03 zL9>2n!`l8z<5=I^HuBG&wt%28s|aHDh8O^$M&KLZVatYZh+re_xHsEQiS^82Bd(D73kZE^ z&FNz1Z;jkIwS$ji`_8(F$b~G)%TFr&Q$H@uv>hlPG1%S#HiWOMXmOWWg0}vTaY%q} zTIlOeYnebqXes}wYpovmlSX4eKO{xrvx0F9fhTw|GnW=PIB_`a88^e-+W3-zt zz{K&oxhsAV|4u`F=&pdWZ`phnoYo7V(F|k?^pqt`Poe&l82E8!M`sBzbeA-| zkb|Gn&@Z%|^!`(#;Ko-guLn;}f9x;wgF{TFN3JO`cgt-!G@a|geR!9QY=y)fCrGQA zp>WG0@DOCg4LlZ|2q73fp&RLBZ_lx)bnlF-rBe z$JMO542GH>oCRg=SOV`~e~9K=(k1ct1%7u?GvmOR4Hqv?4|T1KhvCpYmkqduOr!8N z4jd$|nu>bb?&DtagXNQ-Pw+eIkw6)2E928-GEMF)HHLXNeb`dK)B>=KZq?xq8)Dr> zDmHYKZ$~5YZS2DJJ_ zY}5-zHK77wVxhlesQJK0B`Evj{QE4KQ1e2wYkL6(ijo_Oh*qxF-bj+^b=4I_O;b-! z?go=eJLA`S?GCV)-BlGkzH?qebG2O*S;Ajy8Uf%}boz#gw&fL@Jd8(L_&v!aUk{YH zuN9|tUT2IZHk52)C~c{pvX0soj|Lr`++Xjm=q1Q-O=TH+0#)D-uNAx*a5a~^0 z#gYIXh?HSThp4Z<)6FEG817WV%P+g#4~%-mxHrHZq@_AUp#Q@MhiYk%tlIy`{;JAu z=)>Lb{epon8CE??ClhbA-&^@U=ttAT2=NyWZCrJ_yhDVh-QVpcIQ`Z87-B!4=AGe@ zkL;cUg5GbOPCbAfh;KJq_NYz|8fmoTbHIQKuI^@NHUY?#VkDq zw~pc2OUn$fLC6@@?U5(7Iff}069+-+aDO`;tC6Qf!bp5LWMTb-YN$US_n_ogpI)16 zV;-GX&B6%J`ORay)-Mndy-U~JT+Z#X!fQA~MnIu@*keGMB6$nbwVY@x5>9>+L~40@ z(JL%Wy`8~zKjc{6V`qnhfp-Znb1(V2&tY!(KMSPvdURU)BO)zB2q$O>=v@T(@LE{u z5XUCP_}~>h^GDPO9PX~~2-Rhg5wQgp+q0vbVeU3-SZo+c2ZEC+tZlJ>QDmJ?CcBsFZtalCg_g_Ag{-?pm8mi_f56OvHvk!wW=_xwJ9Z z?q!HUk(aU1f{hz&7r>6Oawl~t^R^1@B>QqBICn?~vy?HjCU2|WVZz)sfDdCP{k^6 zH3OT@T_Z6dF4|kQQ~g9|v_hL+9_ITd%|rKPb^hhq`h&jR#^-o=QZBde^4lFFBN|gX z=`h$Sl%_mhQL z34rn7QxR--PD-J;=bNt9+|#47eGE53j}-qC?Bse#Stfly|Y${k(Jd)~%7-JV3^J2B z)LedfK}n~ay5mb0;qIXv)fQ2x@AULMUn!9!%r+^HUOTEK7ovSi3(u2MpA9bT4ChSu-GBy9NJkUCd z3?JU;884i^h}D*g1S;F5!lLLxro2~rQz%3Vn?${di2n9D1jtM@uN)^x&;H0CGOc>U zTDeY_&mqf%>a!O7Ccu zU}61JC-uF3J<2ZUul2fJ2mg`z#`!c#^*Fc9dYc(S#}Pp3tXK9~ABwGCllKM`tGv*{ zG^ZtRRlG1=?dJNpy1gFO@Z2>(QOfo1pS@>HdyIaEb~!dhihBK_b%|Hr^J%j~J8FJ& zG6@`ElShANMuhqB#;Q;^1MY8TeHzuCsxs_L1LgS?eLwA4afRJP+$lT1k5z<&-aSx= zX9hxK&VeRpL@ma=j2C=*Dk<4fz$1cSshS?D#yldN(=0#mj#R%xn^9A{7l+8g5%EIdRjC$fh7c z5z%}jL;m+HbkFh+nT|S^!o7C~l&0VD$u$AK`JC)Q!EPAB1DT+M)Y*CXL45pdT+D1- z{A_HAkly%-cKXN-%wE)xU;eK)(a0P0|0KEI-2Zpdu;;A=No8ijX=cvB&BM$E;^trm zegDqQ{N2P1#B6G2VrKrsl zz_aF*S!i`0zcAW63YlUVjwor3FdOsXho>FD$|$pz2;o?_{{FZIFKMwxkY$i#P&tL` zkRE2iE@L`oUNKC7M}?T6Lj{G2Af#t!{%^CxMHs1T;dVU-KG3@+@S3aIeo^6Jdz#>( zo=^#DRS@W`IxXH9>$AT?GrS_rMuN=>YI`PLZZCD&zcMhqq2$+3R$&9y1G6BKYSQg zZyGSGoLC6&Z%*DSReed4aLoCSMdMM_Sm?m8xW&? zfFI9USjjk(^w+T5)D@bC-6}XjDwtnF@k||Dz)mDHK=kl*hi_K{re<$qO5ifv&PoSF z=~%`aA`a0U!&_D3Saf*drl2*1c~ar%vS~a`a3q4@CVt0aNTpe#R?%$A^~_KN{N`#f z5`deoj_=~B`&yP-)@w=7SakV_wP^Q#yCr?>>3EDVtF&jyEJH z4Xbw$u{vyEfGxbUp5dsx?5+up7GrZ0A1F3i>_D1?s{JCqJrDr@M;fGEdZ_)QbetFd z+nTPu?%r?Q^YGH5FBjNjM72?hj^$J1RSJ;VsA@fVy<(W~z034Eq(CY+#aBwqL>udf zw0?f1FliM8L2TP&$aC@(gg3Te#}BGAeIe`-l4ZTi9&1w=&JM;3xGQM47|;94JwR1k zaN4VZ=#NMDXh)+y56N01j3wMMa=_)o2){YfJX)JD_6n=$7nmI<@a^kSTD@mrN-h-= zb8(#4F(KY&FV0HIIvZllk2P|`Kw;ocmCvIam3?2o!AnVS zkuMD$En@WF$XK{7&(+WE{dFM%S7Fk&h*jb4uX|l5A^BG!%Bl#4A=wkg1VF?{M|JK{ zK3KDRxfq8@sJVU+nK6fUlU(SULyhJ2}-))!)AW{0hi3L7id;jh{xU&XOO$2YN` zctSyxe#a3n?JAa$oGzA$rxXOvgMAZfp7cjgv()!l(`mioVxrO9Rw@;>$N#P-hoSnwCe4Qvz!EmccPHY_V!$c^Xq+)|k`+ z5!Eh_pbpXdf8BsVBtDe`Bm`GRFhUQ~!ciwZ-{xVpV$BX=6}T$%)%!CZDd68cp6*Cy zF>!`O(FSlatNgBaf<@l7v2%SByTOBCNtNS(`He@{lRQApGunk z10r==-Jyg{760heqUTp!Pu04)<}lj{^6Rde z&bcRg7U;Q8*To8OaG5*b7+B}K8A5AceF$&u!!9<|OEn-7YoT)svEzMEI7<`q5`NaC zEV;#Yq?DOe0Y3BrD8r8fbtr_UfpAM0q7!zPCW03#zGT&?p&7(rA5rw>Slv)zqte_} z`X{r?Q9LBFZQtL16tJCMZ054Qn2$04{?LfO0xN8#&wr?;ZjG4r&7TeJ@4DT1ruHqY zK1q*#LFefs2Lpb43EN^MLsN=QgKCL&FjLpK~oVTn8#A605wK zy@jhKIfw%U`X6sQsb}Rt#Mk^@ZPXik17gDU&_qW;r*&FgF%dYqFO2@llxpYpW3+&J z{O!d9wX8@sQcv+n5Zpt(*w+sB`19khCN?EffdqX%E)oEaQa0Q{FPFdyev~>EJI0L0 zq}iQEs!*2`FbNuR*+F7-#TMds#p+G!3#ez6(ZdPB4Q&Lxhz8ssa2S&Y(T5NZ#Qt*N zGh2R@M`s8u*1%Uy?hEwYX}ZR57cq*eVtO&=)xd?qZh}+Duf<)$u#Ct*xB>H0gKq+0 zW8)+6B^*UCE3Y9Dd?9=Kp8Aj}zpx4WFdhc{B#}bHXM_0Oh>t)ByJuzvx!~NB z0Co|f>sNJ)lVB9RhKMJJu_pY@Dtk--O)m*eMOQRxJrEv3Es7XD|OfHmj^l zDBm2#_Tk#bKC3a)QU7jP8$EGzZdbgV3|wD&xuCwK2UzB&A5|t^=!z9D9Yw7g$$h)< zz0|LM8>8U02w&NyzK5!$&bHYmC|LxBEYAW5p3#rAbe-tKVx*5W7E~X{DstKWf2x9g zm)gp8Z$};3%HR^&-*QOwZd(b_N($_`%+X~%47KpOrh2b4o(5QO4KZDv7NLG(Y!+ga z*iV1!KVdE~Yxf4@qli9W?a@G{QSvbG@bl2{aPzS65U}SXXEbO+WwA|%#?juo&JzGp z4t)OqI^vWR_vcRKYV=5ih0$-N<)!Azd#$175@_e{WZL}~hs28A1B@=6WH)YNK?hQ%Xng02+S~C0o-U3cMdu6O z;!RdrBspN6*mU;XJJkq<(Sq2kCqeLuBH2G>j=AkAm|xsa#xBTFQH?AguAgh?$UgNi z@R6zF4YHCR4CpYHW@(5HqVAmfIk2k0Ic~2`he!A>VuXhGB)HkE7mT%9D9(;LSAB49GKG!#JedII#=R%^& z4DI{&Zd7WVKm#V$E$}6l2VUPB>Dh@0+^7pv`^dQ0nCjp;Isa_1YJ{D10BrbN=hw71gfz#T@aV;rHt ziQMk3-3gb8Lh-kocz^xNo#WQcI&%vG~ z9Cx~44)tDxyl;wBnt|Df|6)UB$>txMC5#=!9fSjb2nW`7fc&*%wy~>eE&64{N(Jo8 zbxtEJj^A3Dc3x3++5F{~E)CiX2BWLCI--HKwzjkj_y@+pG;SsJ)c&5=-y2?7GHjBo z*jP_+Yqq@oFj~<$5G4RK|0-bgT5GG4GWFU>kK&h>X~9eN5st!~>u5d%C*_rG`(m?$ zsAeF%fjF(M(TDra4U)|fq1h?_Kb)-z55_nB(hBiGVQ%eJ%lX=U6R`fptA^>X;*wR4 z3#3H}6gvwci>mZ|*=D8hH(<$&M4acn83Wt74h*eT6!J76xk<33Ge+zKh|ZMR#Fj@5 zh?y}3C><6GRW;KkrL(sYMBUrfVArAjt2X8;1QH+_t@Hq7{3CbNo z!4lFuR|-KPa}})$lb2jNy6UOj7=9gu>vD;(bL|osv_Bq8|EBC-QeBzsaoMV-q!-B3 zF?YuTZhX>3~!|j_@{3t%hxvYU*+nDGq6y`$W)n!k4iW8$G^Dv@rFwLVrG(& zFrWkqw@D{LEob>6@WySXLyV#ZH8jIUTud~b{^A^E`<=9#S!apE1V5P&9{<9frO$(! z7J+bbZtCCe-ih$keaV!WI$FH-VoIF1?S1PX3wx4OIO{f$a=;P zAX$Eh(@;zb@)eE1YpD{yovOOsXw6iW%ANLYx9tog=nChvWD*gQ8{BK?-x_uc8Oc$Ff4>1E~_~ zCj7?~-=NU{2dy(@k>w9{t#sWS$_yo-_yDVbp^O|BDvkJ$Bz`HJq>^>UW&W&Z%KaD9 z_R-6}GOF+GkCK{@64BpbFOf)}m_tpi$0S{t;Tc3M>juy^!TBV@tGw;V29kP0lH1bE zIMyEg_(*EJmBW_PXv6`Ekq@=C*oC9G!q04$cXJs0c`35p1W(Q{-cXT6KtdD1(UQ$j z$G;*OAo-j-*OK76D>`x)DXVf=JIbV-m{l-ZBajD$H zEm}@3*SYkTvlEi=TcYBhB|mWMsTLHP63xOSyk!Tq@YLo{wV(kvi-F2d5%+x&|E+OT zvd3%Hbc>H@Z!ZCxt4-1_ugCLLt*$$3(8-tbrL571vw~>w#a#U(7qK*e6K5ReKbp#w zH>K6Ce_Qn1_JUE+f@zU}F@oPz?E(9yyf?iA&En4=PoK9PXkH@X`_T7IV{e!CbY=~S zTiBpGhU z!>xzqy}mp9LTlT}2(k_^Iu00(F|H)~S$fks900}rGF+5)d7BYi8#^Ej^*E&UMMs&P&_gZp) zdKOY(k7lgsm9+5vf-%Rz`nl2nH#N13HSWccKd{Ph{Oqb_X#qm&wd4&v*AIcIOZU~U zNzSyS0o=!2>Fo(nd?qr#?RMtyPp~@Y;OvoU@pPeh===2s>}~S!U1AxiEg0pVJGe%3 z9f>e?#I6c=`aJLMMXX-Aq803|3nm$ylHC0Z^*LU4L~B|QB#a-dY#*k$_mk&IqmPe? z%QB{-RcO9SriqDBH2gSoO1xm!3B-zc2Ycv778f}T1@8jYY07d~y;}s>mUoT+DW%!P zBPUm@3HsmFt4Cnjb(Zt1>Zcd8NQ@0et}O6}=hN;6Yof#6Ro0}Kgjr(^^gmzEulZUJ zQS)&W*7+oXp;h72?^g+{K!gt zIF}I};UFO1u8)hR=&&ho#JDv9gkF)T*>SU5)d$R5&PhgA(qU2rT=- zg20~sZ?@29eXp_6+@9t4%2kp;$o|qRTfrNNs5TIwI0Z?`zR^Enk%Ii9@WC_m9HM+^ z$a~j8+_F@Z)F3;?O5a%`lEbMoMt}DtJPxB59D!dy5vmtleyW2J;`)`{KFN#uPtmL` z%Z*vzio#|_RWW^T+n3%W8=C!m{rYGtjYFd6kf`Z2sfC$sZ)C=`FVg;_Lk)}qW2xg~ zCM|&0;*)NNXS{*sbvLL%L<5uR{5PL7gR#DPFbDCB0oEebue- zm7h<>ENU{m;>BCWrVMW8M8W^P2 z`$wav_6A2AE4(c*$>0hbqZ=tUwor7C;yA&d`Q_m&&skKPo<&5j2@$Ig-rnFx(HoZ| zHBncVB0ANxDinperUc6ReHIG`UyEnmFX!OTq_}@~*MG2QS8NN=c%qNaR30QNb0=zW z@3bu7+71@duex^NCF~YYCWvEQCjbLi_2?-Ya03XM|A6F&SXP8y3CETR)44h2^I)iq zOEJ_t*pvVKGDn`jU^Kh-Iq@PW(LzZvcC-5#-s2+lP1JonR6%Por`oRluK3aO3|Feg zx~uuJ=U%dz{26JkVHD}MV@pu)z^e^*ad35+Gu!uKaZyk!Z_}o`Y$;@Q5>O!e`YzvR zrPR2(_t{;^))dTr)fnpEows_xx*PqecFou_kv-Gy6x&sQ#q;q~WaW^#GtE?yWZidP zw+6QT{E|W7$IDgZ`tOeU=AWqFvD@jp^0YkzVP?n-o19B^&QCLb#s6-jmAL`H=9`Wh zT~g}_SHlaP4R13Q-I`xLmpD65{qGUDo}QYwo>7BWs&1>jU&%?8S7Dntl<4eukhs8=2z=1PV=4Iz#mt+G;a7b}TN^tY>@`-VCOYyMt ziHfqZ@k+5v36X>Uzbgj+TZ(XUBz8kH03@@tNHa`Q51RClv(bs{KEcvqBl3zNK#7V42Eai2UU4aHW@Pxpv{6z53<(SjQ*uNe(!`W0 zrE40d3`F_4+X2L30a*HR$Qi~zi5MtQoY2u0Y9UFb10--hlUGt;M&qE$;^0o=0Lb+1 z|NaD#?1-aflo2T5iC(6OeoUr52BvWb9m}F+FW%6mEtRQVJpS54X0~+Er_5Wf)DDoyAfM-bfL;)3Mw&CEN}w z8UOS%Vtq4|Sh^K${re6F`E7f-&wE$~jFqakpkFhdp>EMWRk=`7HSyrc5jnY#sHr8D Hq>%m>^)adX diff --git a/papers/hatra23/hatra23.tex b/papers/hatra23/hatra23.tex index 9e9842c6..571cdbc8 100644 --- a/papers/hatra23/hatra23.tex +++ b/papers/hatra23/hatra23.tex @@ -31,8 +31,9 @@ In HATRA 2021, we presented \emph{The Goals Of The Luau Type System}, describing the human factors issues with designing a type system for a language with a heterogeneous developer community. In this extended -abstract we provide a progress report on how the design is being -delivered. +abstract we provide a progress report on the work so far, focusing on +the unexpected aspects: semantic subtyping and type error +suppression. \end{abstract} \maketitle @@ -40,7 +41,7 @@ delivered. \section{Recap} Luau~\cite{Luau} is the scripting language used by the -Roblox~\cite{Roblox} platform for shared 3D experiences. Luau extends +Roblox~\cite{Roblox} platform for shared immersive experiences. Luau extends the Lua~\cite{Lua} language, notably by providing type-driven tooling such as autocomplete and API documentation (as well as traditional type error reporting). Roblox has hundreds of millions of users, and @@ -65,10 +66,12 @@ For both communities, type-driven tooling is important, so we provide \emph{infallible type inference}, which infers types no matter the inputs. -\section{New stuff} +\section{Progress} -The main improvement is that Luau now has support for \emph{semantic -subtyping}~\cite{Jef22:SemanticSubtyping}. Semantic subtyping +There are two unexpected changes to the type system: \emph{semantic subtyping}, +and treating gradual typing as \emph{type error suppression}. + +Semantic subtyping interprets types as sets of values, and subtyping as set inclusion~\cite{GF05:GentleIntroduction}. This is aligned with the \emph{minimize false positives} goal of Luau non-strict mode, since @@ -77,9 +80,10 @@ value which inhabits the candidate subtype, but not the candidate supertype. This has the added benefit of improving error reporting in the prototype implementation: since the prototype is constructive, the witness for the failure of subtyping can help drive error reports. +See our technical blog for more details~\cite{Jef22:SemanticSubtyping}. -The other big improvement is how we view gradual typing, Rather than -the approach of~\cite{ST07:GradualTyping}, which uses \emph{consistent +Rather than the gradual typing approach +of~\cite{ST07:GradualTyping}, which uses \emph{consistent subtyping} where $\ANY \lesssim T \lesssim \ANY$ for any type $T$, we adopt an approach based on \emph{error suppression}, where $\ANY$ is an error-suppressing type, and any failures of subtyping involving @@ -93,7 +97,7 @@ mechanically verified~\cite{BJ23:agda-typeck}. Currently the type inference system uses greedy inference, which is very sensitive to order of declarations, and can easily result in -false positives. This needs replaced by some form of local type +false positives. We plan to replace this by some form of local type inference~\cite{PT00:LocalTypeInference}. Currently, non-strict mode operates in the style of gradual type