From b30e3466cdbf98b8c9a572439f0f986d4932257a Mon Sep 17 00:00:00 2001 From: Alexander Schroth Date: Mon, 8 Oct 2018 19:04:09 +0200 Subject: [PATCH] fixed hindley/milner algorithm --- merkzettel.pdf | Bin 182876 -> 182870 bytes merkzettel.tex | 4 ++-- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/merkzettel.pdf b/merkzettel.pdf index e9d5164724c5928f0b49586358b5ad5d56a88274..01221afd7f601789ae77bbd83bb152ca71aabd10 100644 GIT binary patch delta 3627 zcmV+`4%G47lnd6B3$Pn40XUP9#VCK}TuYA|Hxj=_{`D=AEj7ER*bj}yc6KkGmYU+DSoPIcRix=;IiZukUeMOx zudgq@dL`|IQIgS&O|Ea@kr7G7#Ar&WR+H zuV>s&|NZN14uA5E`yq_dY_ANlJe$m!AWCM(QN(O6r_W|{rnUPh!*82oaYnS16H0`! z;fI&5*@P1T^PWfFKSzgVL_vquR2Nl~h72+_rtfELnuENj>qWW1W|(oJsDuGQ>Z%&> z3fmTV6mGR3{w%RAS#w)#dRr_mbgEf<<3LkMW~gtVh|wB!ifExjD~9zWi4lAfwekvQ zV7^}OE~8K8pp1v%bTpiR{iRNai7_Vh^b0ngBFqhUY;;*GOk0E?Y$bncbx;(aKbOZw zzu*c?<8HV@M{7u&!f32p`2+>E2g%L3^6Gz@@>wy>x9c1?O+y&7O;jkW-PxgQ&|p7& zjM8<8;2syHHEcK*l(V@I;xO5kifbac8iOlb-CveiS6mQI`@7PI7AwGFI?b!u-J`Io zNR32kY3bHVi;ep$!-{`9fJ-Yvt$Y-4{q1h!psUR9ORqi?4HM#~iA`@PrLb6IVGaII z%8Hy4Q{CSC7)~_dLSb;yoTLHN5iy)xroihk*cCdM&YlLk?s4dn07vn78*FXX>*FbF z(_L#r$5Q@%)armp?cwH38bX=d8cmd_oc&*BbHhQ=F_hroh)sVCt6ocR6_0#OCEO%j zGh$2Ht1aqwI<`@HR)KuY1v zXQ6PmOW~FcCjx&&#Wb8;MDf{t&gYvn6084+wUAS<{ZuzjKtAv3gryp=7@4U6&KPd z7zvISY!mcBW#GgOg!8)j79rvCh<`t!VJc7zGhSiRA|8bOud!|fiI;oGVYJ8|GnJW| zL5fwidX9f-DbNtkPw8y{N=Nf=(?=%8E8BBSaqIcFJ8Sbp29l3jy+sk$K`P;yLw`y% zgdATpRDGC);bpJ>49N+p;hJ1xQ-PRQXQMP3&7;jTfDGa6kIE5l=L>8L zgX@fuvcQHEL|8t+?^sE|T}&Xj^Bktb?^s!y{-W<>TGXoGA)0 zsfL=X7-_Cany3eus|K0~dnYpp=HQn-G*Plndv#ex3PP0@c9P5f9m+;1<}Q^Uuwp!* z4zPbQfE=olp6JuqSg)>uaR_S><9OgXv%#Kogm}-F$QhHzu|t?H|L9835FH;cmp z^7~>}7Wp>cgg12w+=Tinu1TOuT5}{?)OfVmMXnXeSR<*k-`rG_E1I)%rC&RJpRa%M zim&k5Av&Pe`+3xJHRxKiM$wFGvDrzYq#m6d(pYk6e7;2`wA9L4zkH5F7)op=n+4I` zU8ua>EOxt4drM}~7$CbmXIA72w~S_X`h1BZzfPydSek{$4!J9fHO42Tc1IIlr^?Te z_8FB=>`nWeJ30R+O8dA(qVeZ-g42Jg8u1>dBdJL{9iX;#>HMbzWu&cx8qlRpkr%GO z%tWUl!lUM_TT^*_7GZ~*v#Q5Quonj66?r-Sn> ztB*ysLD%kt5;##*7J!Ug^)Y4U3K+Vs!hze{SEHnMUx2Ey?i5{f_Y)f-d$N-@G#-Dn z46Eqo?~H4rt7CNP#8Z{|_Je2dMG2OYZ-eW9v0C13i}L;2tM)E<%pb#_by0>!-{qSn ze&EU)!qm};ejjSk*Jx6J#&+)Gh`Z|OPsJ*itGo!r($58k#LA_dg39uCV3DE9F&C1P ztbM|#YnFgUl4fnidzJ_&BjMgBoPK|OT;Un+Ty0z<8+u$|=rNK0s(q9w&0^;&e0~!M zN0fF#PcO}dFFVhprcX|j9+3X*0qK|i)M+@Gh>#!ZQXibMUf#pKt)HiOCPo&|u+{k^ z4i;OUey}{-N3l4NB7Gi;#UC)N2YxZ)w@cjRxreGng*_sD{H~Fueng4?Y$1Q<8MpuR z68|TQIL}?+e~9J6A&vAotW3)%#PW`+9CHNOJ~^bTG^CGRamT8`B{Rj&8Qw2&bTC@S zYkh{3s>u3NQHAW4{83Kt@Pd@Kyia2r2cKWV#&C{1QqY=+{Gc~Mtk0ScuQ$HKd@%)E zw1a)IKEW3Y+;Srw9fsJbk{y2qRAC;vGtQ{R5d?0xMU`Vjp@17!K|yqW_er3jOay09 z`1TP&zzhWecFIzFBl-T7CT&3X+JHREq1l%0_62WGqBFZx7HR}~C4sbcT>KEGVTNaj zHCbne?w%SSXmf(XBDH$F%~c_~FE*kCzdx=TTc}Hv*o+!er|b1e!(4ycX8;Dhd6YL) zh#9Ay*&at8gcw{EdxF~)ty%hy_~CbVTzJf#xFmOoMah!;4R9ueJSVOmZnh@ZD8iN2 zCOA4r3C83PvPbz3p9Q*m7jD-Us0q?09mWR*BvpEZ6|R>qS2Nuw?&Qjmmn%M7>>kEE zd+}Rvh{ITCru^&cB-DQQ$vFs3 zZ}KwVuHp5rg#O>>oA5s0+^mYjM?HP9FYnfiGGy#}&oxyBGKZK}DBe}&e;ID<-R9d( z9;CI{@6c?xi4WrbkiZ!pg(|C6)#Ik9ZZf-(!dLlr8|Nb5Eqs4n-sLL)x!?KSf;CW| zNAow2bbRxOPNJ_Co145{ZvyC40G%P1tGnt=-)xGqSgiad5;Os8XiR7Ro`P3e-_qIN zCent|s#e;Nb)^jl!02yCz631AoPN|C>oFt7U-_*YbKC%18JKj!!WujLlI^HPTKwK; zbKbHeJMt=ZR6>6@D*xR<=AbF_C!Mk-s+kN-p9$jrI3aJEi$KlgYF`~psjS$Yn+f-e z1-J`%vsi4qvx%yl_NRP3nT*`2TO)aMxYoVnr7?3mmSj7g?0jh0OQ&Zy8gnIf*sFV6nX1cpu zRj{%PU(`_I8ZYx(Fps?Y>4#!_^JQqZ%pDN9FaOwwZ>~Z=+oCMP3rWI@7tq0Wa|@iL z8X|A-9@l>~wQWL!eepjTWC8hfXZ;T{HJ=6%2bA+qg#rtjL436=R2QNXY z26x-CD(lqz8JT4@}|U&?rH!%nJQ5K-wA6FMNb_ zNH_<{2YAmR!_jZcpfagN@XCU0Sb!Wx{9Jzt3+2d zu0b=jKr38_Hn;&@a7)%Ry`BBkJqHM zdp`GCI{xf6CH*b)npQ~t^m?N(xbF2SFc%xqh>1lmgGVnup7}g xf)$9YKx73XD-csK&0vdTp821YI)oGp7R*-DkO zQf;atyDD@vqGwG~2|0?DT=uVT0~m5JqsBZW%2swS;$uKO8r@%i-3^FNmJ>Sp`w4Bm zesg~E^=oM-jFOCIY;t}DZyAwPOpK<4YBf2(oLo%bQf6lF&c8eS@axx1HGk!Q-ohi_ z{Cvjk^p9U>b9l)&?uRf+v%NCJ@@z6^f+(3CMiH~QoIan;nbz*348LuT#Tn63PACz^ zh991~W)n^X%zGYv{{kJF5d|GqQ(aU|8ZyYd1gaMQ#yZhNYqM|R=Z$m&Z>c;8c|Eg-$hVZyabU$qe-k6fs(ZP7y71XvMI8Br$?dqE=qv z49wT--D&j6?3HmpoQ{SQu)oylFfqo2o<3sZDZ<=vheoHh!n8#Q!d9YxRtH7#`Ez+_ z^buEJ8h67LI$A^G6h>p+$|oqOJxFfOl~@1!DW4V7e7nwZ(=>!J+eC%3+MOM`1`YPZ z$0%Kg2ySsvTEm88K{=ZXA@-APskkPBt1-C3)$M7Cb;SkYw7)C8Z?OU_rqjHd-7N~M ziquGymX>a;8CKkX0bE)UYUP7~>mSz}2VG@;TYB}GXqXT;O>BBgDTT!v3v2K% zDJybHOm%zjV>r=-3x&Z+bCL#7N5pV)ngXx=U}xxHI(r=Gy2YVO0vyHTZLqajuaEax zo9aYi| zVKE|`{tMkLLjip!l69+fcx8KmDQ-Rgc4uvV$UyQ@t9K~EI!GlvbLdZr zhLEGJS*<;{wP&paf~pUbFud&5pCLIRHC&TRY$_1*>THxIqj|J>29P0~{ZTo>?RQWn^df(Xk8_#G<=xQht{cb>y^_#LY&r=9eFJKS0byTwES1E-cB6=)g}dTUq? z=$0K+eaV%#61q>A9!V@Ituw3)#5nGF&TO#f93kH0C342(aqJML%Rf69;GUaV4hp4P z+*#38UM5UbG9P71<(y%+iE7Y9&O2SIF~A(4HwhG8-9xXtA_Q0iUNIy_+2IU-K)%1k z`Moj+#VPROB`1a-W1~mZ{WQ$W5pGK$aJWx@KI2=TJOADN$+x@Wdb3;Q>rnU`k<`dK zN1RIvK&M<{7N)BzQo%?wJ##Tvlum#2g`mx527w??DvuJtqReNB{6+{7$|B$9oA9JAftyfY#We|3No$ToiyDs>yU4X78EYhUZZ?e>LmEpCjnB8JgqB)a>zB`w2t$d@WV0Z; zyAGAN%f)UNYH!Ib8UtjP$IObH;g-?NP9HB()b41)>s0v> z(mtc|iM?r`V<+eTLTMkDNHqSuPH;MZRU_WxbR;!trvucsE}j3Jpp3M2Py@QODe}S< zn3?D_M0l$?>(*2rpGDZ==B(;*670o63G3uQtq|IknIz>nJh-xjRAZf|lT~n@?%m#b zmet3i+MsiHLJ6EGDhohHuKJiVa|H}tSK+|z-BhEbc3*(1vF;RIbN3S)A$ziuHZ&f8 zwhXK2=I@MaqN`(c>Yk@6^X(_k-is0}CEo_u|8ljw-WKJDwO8$3@R&b_mvvEwM&IX~ zC4S(_8p71UiM|On=yNnFKw~@iam00X^rvE#%T-9 zB+c5|^gIzIMiRSCc=GxT!gJhXMiJ|O@G}5I&wdOq#b-@-X#v`SLPUuq^gPlWn24jz zQPa;xe6X1ZqAdL}(s0xeVKda_GB{;7 zzeAbsI689YkTdIGv;)qfKA=#4v_P?M&&BXPe|m-b{=o6rb^5z|71c|ZD837S@czml z_;dLr`H1-5QGR2YpTlFryh_9T*cErI8hkHP?3i)<0!Iy_b-dQ+ID2w$dcp@eT=MVn z%9FOdPp2D)r7vJ(ILDnUXiX$P^vZ|z>G9!(#rK$treLkvU>9xf;i3g@+mVhgaqWoq z%+W$r$qoXlU=iIJXVl^V6Ia`RqDm&BP{56&_p*6V_feprOhjQ(oR(C@?CF5Ou(kHa z?EOnk8iDRL0(q3oGb(m8;`C z+~}%c+?N$m;@=-^jV;L~ifKj-sL0uIIjw%@_7vctH)rye3NhofGqdA=_=6CGD`1as zlcF_C{}Dgv?v4hJi8+SRhvbF>pov;E$3WKoE!N~3MYz7&gh%j|7Pz%-W<`9$=lXrP zNL!#bNSlNhA2ah++2MD))=O9Ko!%s_-^!8qD4rU4+wscN3E+Z5tj0P!wM5jI(FE`~ z{byYkR!Gf5rYz$iYXy*h9vy}HzStD&a48`a<$w2iIEY^_^D^JA;qk77{y*fK@I2pK zu8RFfJ$-poUauErNY3>hVe^j-i&_=YP0AI>?*$B2ardyQvPLRA%hX$P_boPR1MW8~1Rr*oLPm z9R_@iJVLju?o%UADRJ}cY>yJ_@tL`NoHhTl~3-j$2@UH_Pa0#~4B zc$hdWm#7>56Ql=PZn-5z!)Q{$M&H6Mj}i;hhOsv+%vfVUUDrnh-$8Q{6 z@L1wLE%Pg|kG%Tnr(%2gEc|YnJ1}xz{&^F=ISc)4i?R$4Bnb~*LI>N;6%dnM_#$tR zAJ;UsZ9;>8f$=YZS$3EP2uz!Sfx5H(4%y?AXbFPHvY3C2!K4IRUp!IRYt)1voJ_G&Glb z!vY=!I59RfG?$&j0%!*>S2HqHWmvZb!~!S;Q870*F*!jpLNzrsGdVOfLO3!;LPIu0 zFhWE#IWRLbMLr-rF*i0bIYBZ)H8nIdIW#juI5I{;LpDS(LPRq;Ff%hnK3xhgOl59o zbZ8(mIWw1F!~!XQCDJ)hRACf{@$-M>BFLr=jIzk44#*}5BA}=YvbeGdBAbYzq12W@ z`!@0w=rmH0kQhIJLHPhQly)@MG#1KpY<_v}z2`2OIc8>mgIUrGeQ*~{VehL^f&!V9 z_+fxEr$oQ70y&Uy4wAR9#394cZ_B05Qp@0#2l?;@&N1SD=TcB8%Ukz*i(nDnK{0dw z$_0vVNlM^6T!4#k8A@fTMSn^e!+b`PhD%Tj<+7S)AE|&!sDdj{4K;8b>SUP@K3or1 z;Tqh8jI1@suQos<+<+!%h8AdrHnEX{!w8JRV|W5jWkWmuHwq;s HMNdWwAtU_C diff --git a/merkzettel.tex b/merkzettel.tex index b317cec..b982fe6 100644 --- a/merkzettel.tex +++ b/merkzettel.tex @@ -336,9 +336,9 @@ f_1 \times f_2 &= \langle f_1 \circ\pi_1, f_2\circ\pi_2\rangle\\ \item Wenn $\Gamma \vdash x:\alpha$, dann existieren Typen $\beta_i$ und ein Typschema $S = \forall a_1 \ldots \forall a_k.\gamma$, so dass $(x:S)\in \Gamma$ und $\alpha = \gamma[\beta_1/a_1,\ldots,\beta_k/a_k]$ \item Wenn $\Gamma \vdash ($ let $x = s$ in $t) : \alpha$, dann existiert ein Typ $\beta$ nut $\Gamma \vdash s:\beta$ und $\Gamma, x:Cl(\Gamma, \beta) \vdash t:\alpha$ \end{enumerate} - \item erweiterter Algorithmus W mit Menge $PT$ von Typgleichungen + \item erweiterter Algorithmus W mit Menge $PT$ von Typgleichungen \siehe{S. 90} \begin{align*} - PT(\Gamma;x;\alpha) &= \lbrace a\pteq \gamma [a_1'/a_1,\ldots,a_k'/a_k] \vert (x: \forall a_1,\ldots,\forall a_k .\gamma) \in \Gamma\rbrace\\ + PT(\Gamma;x;\alpha) &= \lbrace \alpha \pteq \gamma [a_1'/a_1,\ldots,a_k'/a_k] \rbrace \text{ mit } (x: \forall a_1,\ldots,\forall a_k .\gamma) \in \Gamma\\ PT(\Gamma; \lambda x.t; \alpha) &= PT((\Gamma;x:a);t;b) \cup \lbrace a\rightarrow b \pteq \alpha \rbrace\ \text{mit $a,b$ frisch}\\ PT(\Gamma;ts;\alpha) &= PT(\Gamma; t; a\rightarrow \alpha ) \cup PT(\Gamma;s;a)\ \text{mit $a$ frisch}\\ PT(\Gamma;(\text{let } x=s\text{ in }t);\alpha) &= PT(\Gamma\sigma, x:Cl(\Gamma\sigma, \sigma(b));t;\alpha\sigma)