From c1768b01611d10e1cd8c54909477fca777ac6d12 Mon Sep 17 00:00:00 2001 From: Martin Fredin Date: Wed, 24 May 2023 22:12:45 +0200 Subject: [PATCH] Add examples of higher ranked polymorphism --- demo/rank2 | Bin 0 -> 15536 bytes demo/rank2.crf | 8 ++++++++ demo/rank4 | Bin 0 -> 16280 bytes demo/rank4.crf | 20 ++++++++++++++++++++ sample-programs/working/rank2.crf | 8 ++++++++ 5 files changed, 36 insertions(+) create mode 100755 demo/rank2 create mode 100644 demo/rank2.crf create mode 100755 demo/rank4 create mode 100644 demo/rank4.crf create mode 100644 sample-programs/working/rank2.crf diff --git a/demo/rank2 b/demo/rank2 new file mode 100755 index 0000000000000000000000000000000000000000..4ee812a86b59276b931a4662d601e0ed20ce302e GIT binary patch literal 15536 zcmb<-^>JfjWMqH=W(GS35HCRhBH{p{7z#|G32N4ss_ns8LJ6_=zWYiold#01G(%nZw+Vx>}< zoD2+144a_xuzUu~7Y>3Di51X%1QTa~ic3HXDwsHof50B150qA5X#^y40!bX?K9Cp) zUqBLvl!N>dOmYewIE1L)rw80uVNQ z>)ClR&ZF~@NAr^p0U@r22MkYo^xCpAGBErXb=PNL_>!i_FW&-E3O3)P*R~VnmR{B- z5M}wJMAW03RSm>$Jy62={{g>z14!{0J_7?oseY(Ov+X)P1_lO?&Zi|j9^JOT z^cWak=>Grz|3$|C|NoD%e$-=NV2p+7gV8Um|NsAw@WKR-&JdL!9-ZGkx=U1kcyzP> ze~<IpNoNk;l-kV|Nk2vh&;@| z0FEP+SOJB=C>{-g(GVC7fzc2c4S~@R7!85Z5Eu=C(GVC7fzc2c4FTdq05rd*n#sVx zD9vmQn&Sn{QAvFG{~y%J_W1Ds{|W{MhKLXU{|A72#vlLxKfu7iQ1S8q|0_@{M4&Wd zRS*MXg#e>84?D*MMs@*^IC$> z;lsfnmn`|Nmigb|B@TdDR#O28MC0tP7-b6px0$Xb6mkz-S1JhQMeDjE2By2#kinXb6mkz~Bf0*!o4-dPUGg zE68PKAOgCc6~t@>5lH-gG(KnzB}j+|M1U};!^FVAzzbqCFfc5Eu7{L_@?q;JrJ;OS zuSp8Zhpnds_1Qo|F!`_l{)3jvGQ5B;js*25LGl-%ixy#P9R;9#&{QW#ejkWnU|`^e z(h^Ww6iUM=s5XWd(Djp0YZ$kvC^RMWnuXEADbjLaY#H0Fu>Nc!}NjDDl9bFmJBIjpcfZhhSC4qN zAV*)N+VSq0F zhZ_g>KzvehF-#G@Ed^M1A7I^Kz@S%LnOl;W#GqGPQUswhV64o%lGLIC2EDxel2koM zCr{my#B>I|^t@8NjKty$2ECNZyyD7S2whSHkts_pD$dN$L*c|1G3XVg<|KkNKv@Mj zB@BAtFwiT=DbY*MFJaItNv$Yh&;y65UQs?MG#KV5_41IGg68WJc!o##G<0a zN{9{^JEbx&F*h@r0c0Y`WClHmIZ4IE40_4=xw)x%B`E2UTn?x{29<@ddJosWDVX^n zwJR|d{^(#mW zghAygsE&u}hqVJ>G^`#5Ro5W5!}P=IV`m1??hnw850GgL46t?ujE1!%AhMACJ}@?j z_GVyU0M*$r`(gDojD}T%F!#gM!RQDE1_n?Y0LF*417I|)9fIzDkli4h4&C<#(+_Kh zz-XBNVfLf@zYwb531k>jy9U<2f!PnzF9vJ0Ahl_ zV}oc=yAu>Iuy&jRR3D6n*$+|+!cb{=^#Iy+g{(gSssKjA{0q_x!Z1FJ2GxJa`eF4E zjCKM^f;2)g)OaY5fdRBI5u^m>eptH~Mnl>SaOL2=We6Sv!!&64!Qv0TISaaZ3uZ1% z4=5gBY!E#UO+T!C0;ACzLg@O}py_vj+6$w1fGk16uyBJ3ZDU|y;DhENkQl6;58IE2 zt{%pR(T5lqK&=(<{yLC;SU+F|biX1@9Y_v@VSE^UjscSPVC`X8I}Enp5w@=plz))* z!{QOt&jH0BOh0U&)&bBeP6h@B4Ui@z46_$TgW4;|`eFTu7ewlR01bbb{jheP05svl z+zE36%w8D(88lDA^uyXm3Q+y%>OpRW=>^fC_9aLRsvIN)#xVVvU><@1sRi+nX?WTN zNkH)gsDZHksGxcVl$K%cftA0Y`~h=2R4bU0Fa}c$2{4NwT=0HNC=*P9nw8k}S3nc~ M7qBV>fo2>703rsSz5oCK literal 0 HcmV?d00001 diff --git a/demo/rank2.crf b/demo/rank2.crf new file mode 100644 index 0000000..f52060b --- /dev/null +++ b/demo/rank2.crf @@ -0,0 +1,8 @@ + +applyId : (forall a. a -> a) -> b -> b +applyId f x = f x + +id : a -> a +id x = x + +main = applyId id 145 diff --git a/demo/rank4 b/demo/rank4 new file mode 100755 index 0000000000000000000000000000000000000000..ae8b3d7f137fc5fdcd05281aeef8e22d0670b5fe GIT binary patch literal 16280 zcmb<-^>JfjWMqH=W(GS35HCRhBH{p{7$Pj73p!#6607wA?0|ShPg(t|3AbbQWk4~dG8ysgK7X>^mNdf8OfGR+zV?c@+7#LtQ zNG(Vx@M%d3$ekcIF&Gx?K~Vc}g-Zg|{V*CDybSs|nMr0Q`Z+1OIhlE-6}lA`X1Zo3 zdd2yAMqs~y%m=A;_X`C(2b8{`MuGVtHai0YIBi4R-3S&3iGdgwQ_tmsXk0j-fq_8? zi=-b8aW@>|Aa_E88pSk_+p&r3FfhQA9I}Q41_lNtWC0jEK0ZA+KQF$xB(bO@KAs`o zGsHJOCABCuJ+rtZwJ5~bIVV3aH6$@9Clw-xRi>b{Bsn9oh#@{cCo?G-YFKV!W*$R) zd~!u%d|GB+VoqjNDnmh0W?o4eLr!K=aY;(Dwl*k2%s|{+I4eClIldUgGX#kzgIHz^ z?mnJQ&hbWi#wKv4k)A070|OHSGXoO?BN&3>jFEwfVJ;}WL;bg9;xsk}24;rkP_a^} zOiqxlO;CAQK7-{82SJF$3TQrpi8DaOC7=ZrOdQ5PU=Ps;N-MB50uniaBo1;PNDPE8 zAc@2B2uS<}k~p~h0SPiNFg!pK2iXA?1{JPgCdf`ungDYc7#KL9?gWX0(l$(dlpYO% z(GVC7fzc2c4S~@R7!85Z5Eu;sQbNF^`3;9hH|tq_1_qDT10_uVFL*Q`;W!L8;=k!B zeFldAs%P{W82IHK82+n*_!%Jimk<8`|Nme0kUj%L2B@j}@&cHjrO&{SHUXpngbm+% zc3zD0=zQeS{NzJGh^yfN!;>Dpwx&!B4F5&l^%)qxr0Ma?w}6y_&G+cF?F6}{m$eB* zS^g*y_2_0*1F>5VlyLrkz%SnbQhXRnd-U2yf+TxQgFuw#Kab829tVFgdmMac@4e}VY$W|q%}DM8>;LZ1aSm)huh0Mg|2;Z=K-TdF zK-nA~yJjkhz3;f2LE<1SsOlLQR2Uc-K^ua?t!M$e$S>{{QC&2|(u&3m6y}Qjo+z`az=-2_OFdw*;wk;ZrE#;{f|( z4g&*2$A|y_&7k6iQ1LCGF6oE=|E-|nrBLxR3=9l6u&95+z`$Ve5$bP8K7j;2WS4>r z8O5U^Fd71*Aut*OqaiRF0;3@?8UmvsFd70QDFk5a7h&raq1`ElGH4*c_^oLCel$L4 z4JAm32Sk7{s3XL{z`zS)GcYh*fi7;9gz{nQD5ar%SkFWX%7?9|1og#0LNNKS|NeuP z$}+rwE{=q)dAtB!vSP+LlwL>TnwJBVCt=LtmB5P`{rdxfUYBkrQ0I# zc!D^C0(8AD%p7KB&^m5$1_3njO0fC73=5$751MQkKw}Sr4E!KXU?X7SlcDMxp!R~t zCP3?nq2jPb>fkX51_p*IM$o!-UWN&1=C?CqUq8MGs(u4hJ$NvMfq`K;RQv$cUhvol z0|Ub+Mg|5!CUFK>dI39@fq~&aNIerDyj+2avoe9)1LGlRC9pUzLjcr#SbhO56cJ+J zWpIGH2WBrjGsqlX2G~9om^;sc%wghUfbFM%*>IT&;!gBv&o3ypX6h<6Ke^mUE*a0z0FcZu|K^!0RRh34uF(Fd)|Pb?_Nsq{=yan49AiU$*(c_r~64Ca6chWON!#F9jY%oG)nxMyAo zL%gSdJlGZSrNyZ!3}8dR1d2%@&0wQI+Q1w%0wj)%LDEQuQOQKG6F^4e@E=4NtN__D zFg92MM1TSSM1$3%ZI?g^Q}A{Qu;ammCnVh9TEXrCnT`-aut4Hym?1tsr8qx6BQY-p zw6!BGGcOZ!`v%+r#wH9Z1v#a~DzL}`SvTkc73xKX_{_Y_5{CHr5MSqbS3j5dc!*0; zk`Yub$R8jK3Xa5*M99_^hWOOH6b9&~7I+wd5_WuiQgJaaS1p)zyS?O!FYDh zVA*Jcbu$fvUU6k^Nn#R%UU5kggwBAmGV@AOiwYR@^72bk^&Fi%bxRV{8T8WgO7$`l zi!&JXQY!O`D{~=qNfAV*EVZaOGd~Z76JNxjSCpEQ2+{y$737pK=z#-HuOO#HFFn76 zL9ZmWqJ%*YoHq1|^1=C4FEt}Rttc@!H9jMyhyl)nXpK)SDoU(`=zy_PD)SO^Gm{xW zCW1_6(1VzhR9wuUmzDe?e>zHe_I6`1b#QK1@HXJqx2j^AI3)FnzFgBuET|LG1=mT>{e&YwyBn zSbG!HECsn8rXSYsbY=kUasusa0-46Z0Bb+PXjpq0A`98q24jP0Z%`eK4&w$VKitC4x|o- z(ea{_YCszFe3(kQ@lZ_%Qk$10?Oi+Oe?y25et1Z2vAO{~+s!CKCowe;(vTn10xP z!~>w!$_xw)8X!$b7-lbwz77pPn0{D)`2~^sAE4=n^;-m>2_NQ8m=j?3!uZdiaRRd+ z*8Ww1>PJ@(@+(X)h<**VAF3QA1jaD^nP47*fayo3VQCMcih*GQ)IblY!$9>6C@sU> t11o<)`2(s1Sv$iGV+gk!O%i4=M3w Int -> Int +.+ x y = 0 + +const : a -> b -> a +const x y = x + +applyapplyapplyId : (forall c. c -> (forall b. (forall a. a -> a) -> b -> b) -> c) -> d -> d +applyapplyapplyId f x = f x applyId + +applyapplyId : c -> (forall b. (forall a. a -> a) -> b -> b) -> c +applyapplyId x f = f id x + +applyId : (forall a. a -> a) -> b -> b +applyId f x = f x + +id : a -> a +id x = x + +main = applyapplyapplyId applyapplyId 50 + const 100 (applyapplyapplyId applyapplyId 'G') diff --git a/sample-programs/working/rank2.crf b/sample-programs/working/rank2.crf new file mode 100644 index 0000000..f52060b --- /dev/null +++ b/sample-programs/working/rank2.crf @@ -0,0 +1,8 @@ + +applyId : (forall a. a -> a) -> b -> b +applyId f x = f x + +id : a -> a +id x = x + +main = applyId id 145