From d629d19ea2f4447e62425cb7dabdaa8592ba90df Mon Sep 17 00:00:00 2001 From: Francesco Mazzoli Date: Mon, 3 Jun 2013 15:37:24 +0100 Subject: [PATCH] ... --- kant-web.png | Bin 0 -> 9763 bytes thesis.lagda | 519 ++++++++++++++++++++++++++++++++++++++++++++++++--- 2 files changed, 492 insertions(+), 27 deletions(-) create mode 100644 kant-web.png diff --git a/kant-web.png b/kant-web.png new file mode 100644 index 0000000000000000000000000000000000000000..8a2d32977d5dc0622c95e0507b11ad394b435c47 GIT binary patch literal 9763 zcmZvC1z3~c`}YF~7)T=^5?>?)iNRE)oT!L2lF~i8ks53$Dj+4zB$blxZloEEaO401 z0g+}fV!+<{{r!J$T-SRR&v{Nf*NOZ7+@JeCPq>zb()Fu1uL1yYUHQc`Z2%yD1^{Gt zFO!o>%KNTylP*`>Ul@7;04w9)ADLa|7^xLN?X9e?NIgeIah+94#ZDbVDq{CmeC7Sr z&Bevm)f;%~X=~|iYs2H~;BC*Nq^z!G@P?KZ0C)i9X9~K0Gh1`Uk$eWopL;ttwx+Y& z!=CiB*B^#S(q>l~MW|b&K zp{r#3JdFv-Vjd_stZ3@^K+%bTf&Xh_*bN4L6#@rJAUEL#!zg2`e)xkj$(_+vL}C~% ze5LvE+o#j4p^&h!JN!mnXFB2Ui1c=$9d}>%HmUc|nO-XU>Zlu4`0{??gLS=GY;(>g zByqwBS$C?);BwclHpLNXYM-0<(2n1)>;|H$&A5$O#pxxKTS1}P{^jDjR>y^&60&po z(tTR^gu?Xeas!;U=taf1n|j%QpQ^5a`LVj13nKpz`-5d}fpfue0FAa zwYy|X-xu?iKu;`@&>PplBpBZhFZled@J6$k_Wi1z7Z~rP!u4C3|1{lVn=2{PZUABb~xtG*2yInzScNUox2=r)wKYMMpxjmB#-1HYF zoMOa{w)Z~}mgQb7^H+{{CN;7Oo@2zEU0t1>&qfIs_O*|Ui!f)Nd*>9vac>RjuU4~u zpxd(ZAGnrr<73!_!rinm?HQbR3I&xWgQDD)x8YvM2ZYO{(ff20HS2sl??0V7Uz@XR zwVoxcttA;b=G#g8eNY4BZ`t8-hxZemfWNba7? zP(aHFgezP5I_FfQ?A3+uxtHuyC4ZTHwHtqbl)IXsPoPR2{vDmXZed-nPRVJhW@LMz zN`3xJ_M_8PRxSxSXZ}K;#ij0|($)YdG*7>Xp$Eu1K%q>+WMynmkumk(fdpm$gga>O zbS)KU@4ZxtAy|mP@l%@W)K&Xgx^cHVG~)uf=}3m!nF7-d?I80wY3qQdO)sX>O(=J4IQ`ifUTNI zGsO8J-T7W<=|lJKL<19tBK*O)=A1__=eh3II`^Z)e%bBaA|Jw5U3g!Gb+4p;31PF& zsHB%0(F`NxKRPT(m-XG>x)fa8f$~YIHn1s4k7lrhsGXz6(Sd8S3!_Gm{i7HYkDnji zo$Ck}Jc=*JrctXjnp)7OyC1i%OkEUz|7Hj2iZ!zNix1dW0AolirsNY`7S5 zDhndaE?i*B;P)YrvV?&Be!#A;T=XgB>)7S0wr+oHapB z4&fAt;qv?W2D98-)_VG9xi^NmML}m@VxX^|l$4}hxSBkPp0uhl5^W=&ofRb#&kvvMvS_KB3AgupnColaL~R{<*-4Y?yM7;)qqv$@cQu(bT5 zUlg>&lzF)`-eG^d)-5Y(SWbMCeROof9;WUWFj;EKDsHB$f^nu38LUyaOCq5HD3uv3(S=--*f z?qA}3oUp~rT}$~fNr^ki8=WCf8eAp;yXM-klB8d>wT^$CZ0h@+;Px=+^k4@;Byh_5 zIJ>z`I^HKPv8kmyd}f{-U3uU$Qz-BLt8Wj3A%W;gMWCgnL)wYo`4FD;>xkbX(|bNuYi*|smy&ENlIHPx+kJumh1kZNraaWq@W zJm?U^bB}7>OsmFS_y*40@=JQ5{BC>fa<9SB_AI0gWL_l1P*5<_+1a^07nN)l;P2$L zan1bri3%oRY$?(~bpUlnyb(Jzq>4C6CiY+8r|mLb9;C{LAUXPZ_XHTxIk%htBxo^& zN5`J`a@|=UnZ9-fpbRneg<5b>nE`|*;Y@bL#!9mJ{LG9@;IX@RuyOCMl*?0p=e)1q*MckS>&xrw zE#PK9j7aDj87m?`*v|oK{OswqDaud6{@~B-b1%CuUJLeV!B59Chlhsl-@J}E&3*s= z{mRNp-|br^hbOo-bN`jZjWUG!6moPO%PL}HEfChY8+r{)l5w2Z{Q_wwO-DVQLVX;a zN!g_Qmg(_#?i;JDT^dxkwnq)6m7ay4ww1LSl}#F#=x2|XgDo6Oh?~)nCfu;B?06PF zS5@6kTq6RRJ~{aASGH12X=$mLxHzFC!s^uN_)DFB(GVIfbu$Ws!BBGt?(QbjMXV1M zZ2Czz(Z|ewmv{tLCAiG%*ME8aIm?$SxbPAf&CTXa^(tID!{I~I;e>GvH)MPM5Iyua zDZZT^8yo9=gs;fD9iAETtvr1Qe|--z?=fx5DrR;$W8xi-H z7i8RMW`ppn=e^1R@jUe6_&wrc&8O*n!Z<%EIoZX_(hKI~1RE^*OuME-lh+@Y<<(|q z9nE_0eSgr=oRq9A;RKDCkFgno;z;6r5l`F|6hF^QHX|)43CE2}9)Q8P@7x#eFc=Is zmTRFQs#y)$HPQvWZxi(KEXo*)Yal_HD`SH0W@4cmNpQf#Qs;`GxR+{}R;bM){{9kQJ8jd|5qn;)q6}3UG9$`Gv(9+SrwQX&H&deD zH0M||Loy@}J(k|B`5VDV6{A!4jWZAB&|Q+UPqPJ$oc7ZGvCNnV*cligED$e{NMtf% zKc4&iw^GNbS_%9B>!m4w_@h5w5V1dSx7JZ6?eP1-_qvd+&S|A;KPzrS7Z(@PR@}Z% z(Q6W;X=E7I9~#GBF?op9NVD`TAnV__K&+QppT4-sp*#pg3Z$Iio+*ko)fzl2!nBgW zjE+;Lx}}B0x;FghCofLR7T_COKdrWUld?iW?4DmvCHlxf!mjWL(7bQqt*xuoNPD>M zP@*_fg5TfYUmBxD@6a=tjMrSD7g)R6X-LmAV@4Ryyr>SlcQcA)Mh^Nyl!z;K5LuGM zLkP*4oc_DNA!pyS2}e6__ionB`55OAzjC6t!tvEa?r{Af`?^`PBGS`mOQJQ{`}M#_ zSC$+~S`O@>5`5pmU=D^k*Mru`f4b6>`Cw-e@}IUgc0M|XH`g^qCA296il5ojp`ex0 zecPMEx>eJ1e!Bt;C-X>p%)Izc8I$0o!vbY}K5@(nE>ap77_u2tL zL8d}_naI(MIy-bmZZ1Eh_a*1}h*H3r615d~{nAG?9AC9?zU@n5An-k0X4~1AYKeZ4 zS(&(~=oZQF`uO0tn|4}PKRe0I-YD!;e$%bSeyfX*pHt7P?B~FG`E;yNx4}@9fN~4Y z8W#T?p1NXC!Fe-2Kzem1<9uzC{nhEWrUXXv$4@}xKG9EH>>xB;otM79u`T*Li>xrY zy)LG~!9i}~IHYDU&7ObYT2F}oMPrfzG#gbM3cYHvLK$?PHu`Ew+1g-vX*DlQL|mLS zGKZ}bO3;R7>N=xd`EK66TE*Gamuh>AYYpwZ_ioEh(9UuUYhlo;lSMkj@r1D(ODt{;of=W>Bk=j^sp7|Y?C(-mB*2Jo z{x3)9Q^J9&+?Cj}s4A#iZ>`~zHZiCm_ydTL}Ed=5|JC!!z zXPkU@=35&4E2f(hbZdqgtYY~eDn8p}ssy=hOnr+l6zB-{mX%eBBw=dXNh&e!c+Vz< zKmlZ(J$i@Fv>LlNnyxbzaVh?>gRS78dw!?^v^L1D=<38}T=wJgIa=!t6LlR*r1q4G zo%yy#&kml^Td?WsINu%&MYxTg*{Th1qAaR~`KEwNO44z4jU4E7+2mZuHvcUt?vp;H zP08`rYph~v^03-DS2POcjd*Z@CviU#Puf+d4E})u zXS&0oqe)%@%tCd3aMoXmy2T2YO%oJwcNo|G9X=_Yoh@CP%81O(N(}S!Nl0n#8Dz%tpW@fHA zT?ORdB9)(h{oZ-@r9WLqTe|Iv@puBxc%_=|LsR5~3dPAkn^O(xa`o1o1%1VY!YcN$ z=)!0*tl^hJQ85u`XJ-<>lwvHhe{m`Jg3=Vnf6J4_Dz3v9aOg%7H@U@3rsiGMwJ`$6I{(H*qLeTi88Qy1FQ*tRt#o*1o#Y=TJ=_R--yb7Q z`8EChs53P^!iajyJKNpthWDCQ;c_`=gSJutzp%-o2sV4Vq`tel<+-r#{oEgCXJ;ss znmR_H*pcb1fE2-bjwv*+X=Flt@4wsWFNX4dT3b`*^+_Kj+xm^CugHDQ(as2#ZxHG! zV}B{u2K^NezN>#kVP+m;S5^6Ye*QZSotjrWO7*;Pn+;9=5f_<~on zqBCwPjPsJLY>?8YAQ^>-zp<(3m~S&V2I}dT-x{*b^Ac0{LpXwDKU^)ci0kZg+ah!_ zv9q^sM&9!gENAg(a__p;LNLrCsQ&HtH=Gl1T5}qMIJ0i-0Dzt*spXlOn|5RXXu>g# z6e#SV0f4vc0B{NX|K=}4vwzr=tWl5sk=9TES^LNj>oO}|D{7tIi>kG2X9yqj>#*oi zpM^Nv$G-EE23ncj(P;?ghp;*BX9GvV_;;G^NAxMbP$Go)l6Wz=i_1{!%J{D2mZm*=&#Tz-qo3wMERG^(BRC)6iei?R+z1O(6JsjbMuW1$5AOSxMtK6P65Ws8$4beMqD}A0HUbYiFU^tN2Qf$lqp}d(Q zTky>vs;Vy~yV@POHYC^f%!z3b8!2a)*6hX_T=^>_Rbns>s$90?-|IMuD41y}F$W#x zH6@(lv6@F$`df)P=u+7SMeq`3}so7$ZDaqex|H`-zDabY`HG4JZJI->Jt-d~{Zxu9G&67KB zfnHv1G3nuwQkAX>+!m7Jmp_UhLxTt#FnFGFx*QCC(ETU%+)D(TDlu8dO4`}@OzT({ zGV9O=b~3=aY*?s0Vat*k;%u}MY@`Gtm7o(|AZTgDL!o7DFVU!2k9RwdljDSZ*FPmF zj0oKh^xDdAU!w$=GLS1nx>m_?v0qhT-aEoR(sb;DJysk+T?W`-_rT;p57$s6 zOX66ZvJ?~WO&_YiGQ1R9LH*Q>Lxf*n0s#RcB~zm27(ty=A^;n8cXDv-MP3ox0>6cd zh}|0;^2gaLKL<7-r4d!UrhU7@jeUdP!Yccv;fjd+qwz`M4FnMYy+pFBw$pq`TS*ee z=aB(G{YylXe} zV_>Um6t`BHltLCP(T$A+f`tZ2OYmP52)3Xi{)blN37-6jNRk zCBWkb=m5QTMi6qpDknQ;&^CRS!a^m)&~S3Z!<;;?9p+zq31DJD+3+R>v%_yPJMi$A zkq5u+D8^c7Wi^y#lIwnWZfnIBAwVN%E=1SoNpn z43*VC#S-t=sDTd*C@Z^T(W6Q(n6%hleMp$hcag`6!*qad@15jeWH1F8Ae@d&Oij)y zj*qi-h>P?Xjz!_-kYwq?Qu%1l_{p#|EWusP>HPAl_;Y zA17s&t?0gFFWfZ+zsC zGi{A8y1h&#RGY_dmeGCd3fQCUVWzCAY~5IHy%bsUq;xq+`}HEnlQ z-9HF3tocUVvZA!a`lFr2H!V@rdzP^;P^TlwF-Em5ZZv3TVeA;#|%=BV{#bb z!YX)S?!qKKXu-!G(HM!YoN5PTw!bken6Cd8;TnGySXGkUuB3Q^Gb;W9L_X4H!-Zd`+(vD2K2o_%Q=0Df`cO)RS;KIf z&33m;*nFg+j098!(Su`xnH+_hwD9WOgjH(Z3>LZyeY}{;s6zY5iiX{bgngHxDFJFR zIC8<8&6-<%Wn>z28RpJ1GeGP6*1&WoP&Uz|VEY}aoHHQr+kj7&M#cmiB!|gWJ%62E@QM2CENSy7GfA%o1kLBV z05s|y{1%l;l_mtCbKwypBk10|3%cI<~kNDgI&- zu$V#`qDe*wWl+f7&*z`zI*_%qF6Rbl9il`u)(zbOfHL;)y8sRav2+va`747rTND^h zHfIT|x~7%LGx{cZTZl4*^{#vPC?}Ao6=MgzU@D$6{OswX8J^646UukTy?FbT;&1Zc z4k#3Vdbb~Z54u3hB}LwT`7OJpGdmw;ZRxpjusd2tOs%8Wgjn@U))#n7-=%K*B}l!8;1)I@&~jo=i{dyvJ}4X7Iy2V+O@fP zJH{k_*qt=XdN+}~>J@a2p7JkmtCBXx2I}v&HrVLMYQMcP{T{8(ep@{HTpIRzOja9j zSY|>%!?0Ie^(jH=J+Lcmjf-T!yT8=;uZR3RCXvLkY)EUZ<`3e)2#enGE#}wDFWw@7 z-HDj8(*A6|+wYhYE?)uo zsll)vlb@dB=pd=y^vGrCwDbvkFyqR`&{PmBB+bm{mTz^&z-p zFg^$ytNZZMis)PIw;s~zeR!BMZ`{}Lp{_gaTZ$RZVEz#Tv$eAAHPynNDj4H( zi`a9PShwe4^)X~x%*`ns7hHgmJM0{$Lu6z9^tl5#qk}ef%pdMElMqL(APVDlPgCC9 z6|_vcwb*1J(NU(Gs08g?XA)4@bf`I%B>bU$>0d_yfG&k|K0Y&xh6j4W*ClN6!vzd;icq4|#+Zmqk4 zoEt9aJ(zz|`A{&=826)MY!b|&kbL^@bkVrKGhvVLvML-hKjH3$lXxL8(5Cc@86Yj} z|8b-9OoD>a&Gi0bFaKNdSN8s!|I4!f@BF`hcL|X$!Jazb*b=ZNz0CzED{4F|ePZ$U Fe*v=OLq-4q literal 0 HcmV?d00001 diff --git a/thesis.lagda b/thesis.lagda index eb7dc9e..8a5065c 100644 --- a/thesis.lagda +++ b/thesis.lagda @@ -14,6 +14,7 @@ %% Symbols \usepackage[fleqn]{amsmath} +\usepackage{stmaryrd} %llbracket %% Proof trees \usepackage{bussproofs} @@ -21,6 +22,19 @@ %% Diagrams \usepackage[all]{xy} +%% Quotations +\usepackage{epigraph} + +%% Images +\usepackage{graphicx} + +%% diagrams +\usepackage{tikz} +\usetikzlibrary{shapes,arrows,positioning} +% \usepackage{tikz-cd} +% \usepackage{pgfplots} + + %% ----------------------------------------------------------------------------- %% Commands for Agda \usepackage[english]{babel} @@ -64,14 +78,23 @@ \FrameSep0.2cm \newcommand{\mydesc}[3]{ - {\small - \vspace{0.3cm} - \hfill \textbf{#1} $#2$ - \vspace{-0.3cm} - \begin{framed} - #3 - \end{framed} -} + \noindent + \mbox{ + \parbox{\textwidth}{ + {\small + \vspace{0.3cm} + \hfill \textbf{#1} $#2$ + + \framebox[\textwidth]{ + \parbox{\textwidth}{ + \vspace{0.1cm} + #3 + \vspace{0.1cm} + } + } + } + } + } } % TODO is \mathbin the correct thing for arrow and times? @@ -97,7 +120,7 @@ % TODO \mathbin or \mathrel here? \newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3} \newcommand{\mytt}{\mydc{$\langle\rangle$}} -\newcommand{\myunit}{\mytyc{$\top$}} +\newcommand{\myunit}{\mytyc{Unit}} \newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}} \newcommand{\myfst}{\myfld{fst}} \newcommand{\mysnd}{\myfld{snd}} @@ -108,7 +131,7 @@ \newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}} \newcommand{\myleft}[1]{\mydc{left}_{#1}} \newcommand{\myright}[1]{\mydc{right}_{#1}} -\newcommand{\myempty}{\mytyc{$\bot$}} +\newcommand{\myempty}{\mytyc{Empty}} \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}} \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}} \newcommand{\myarg}{\_} @@ -135,6 +158,23 @@ \newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4} \newcommand{\mylub}{\sqcup} \newcommand{\mydefeq}{\cong} +\newcommand{\myrefl}{\mydc{refl}} +\newcommand{\mypeq}[1]{\mathrel{\mytyc{=}_{#1}}} +\newcommand{\myjeqq}{\myfun{=-elim}} +\newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}} +\newcommand{\mysubst}{\myfun{subst}} +\newcommand{\myprsyn}{\myse{prop}} +\newcommand{\myprdec}[1]{\llbracket #1 \rrbracket} +\newcommand{\myand}{\wedge} +\newcommand{\myprfora}[3]{\forall #1 {:} #2. #3} +\newcommand{\mybot}{\bot} +\newcommand{\mytop}{\top} +\newcommand{\mycoe}{\myfun{coe}} +\newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}} +\newcommand{\mycoh}{\myfun{coh}} +\newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}} +\newcommand{\myjm}[4]{(#1 {:} #2) = (#3 {:} #4)} +\newcommand{\myprop}{\mytyc{Prop}} %% ----------------------------------------------------------------------------- @@ -655,6 +695,20 @@ fact is that while System F is impredicative it is still consistent and strongly normalising. \cite{Coquand1986} further extended this line of work with the Calculus of Constructions (CoC). +Most widely used interactive theorem provers are based on ITT. Popular ones +include Agda \citep{Norell2007, Bove2009}, Coq \citep{Coq}, and Epigram +\citep{McBride2004, EpigramTut}. + +\subsection{A note on inference} + +% TODO do this, adding links to the sections about bidi type checking and +% implicit universes. +In the following text I will often omit explicit typing for abstractions or + +Moreover, I will use $\mytyp$ without bothering to specify a +universe, with the silent assumption that the definition is consistent +regarding to the hierarchy. + \subsection{A simple type theory} \label{sec:core-tt} @@ -745,13 +799,20 @@ The first thing to notice is that a barrier between values and types that we had in the STLC is gone: values can appear in types, and the two are treated uniformly in the syntax. -While the usefulness of doing this will become clear soon, a consequence is that -since types can be the result of computation, deciding type equality is not -immediate as in the STLC. For this reason we define \emph{definitional - equality}, $\mydefeq$, as the congruence relation extending $\myred$. Types -that are definitionally equal can be used interchangeably. Here the -`conversion' rule is not syntax directed, however we will see how it is possible -to employ $\myred$ to decide term equality in a systematic way. % TODO add section +While the usefulness of doing this will become clear soon, a consequence is +that since types can be the result of computation, deciding type equality is +not immediate as in the STLC. For this reason we define \emph{definitional + equality}, $\mydefeq$, as the congruence relation extending +$\myred$---moreover, when comparing types syntactically we do it up to +renaming of bound names ($\alpha$-renaming). For example under this +discipline we will find that +\[ +\myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}} +\] +Types that are definitionally equal can be used interchangeably. Here the +`conversion' rule is not syntax directed, however we will see how it is +possible to employ $\myred$ to decide term equality in a systematic +way. % TODO add section Another thing to notice is that considering the need to reduce terms to decide equality, it is essential for a dependently type system to be terminating and confluent for type checking to be decidable. @@ -760,11 +821,11 @@ Moreover, we specify a \emph{type hierarchy} to talk about `large' types: $\mytyp_0$ will be the type of types inhabited by data: $\mybool$, $\mynat$, $\mylist$, etc. $\mytyp_1$ will be the type of $\mytyp_0$, and so on---for example we have $\mytrue : \mybool : \mytyp_0 : \mytyp_1 : \dots$. Each type -`level' is often called a universe in the literature. While it is possible, to -simplify things by having only one universe $\mytyp$ with $\mytyp : \mytyp$, -this plan is inconsistent for much the same reason that impredicative na\"{\i}ve -set theory is \citep{Hurkens1995}. Moreover, various techniques can be employed -to lift the burden of explicitly handling universes. +`level' is often called a universe in the literature. While it is possible, +to simplify things by having only one universe $\mytyp$ with $\mytyp : +\mytyp$, this plan is inconsistent for much the same reason that impredicative +na\"{\i}ve set theory is \citep{Hurkens1995}. Moreover, various techniques +can be employed to lift the burden of explicitly handling universes. % TODO add sectioon about universes \subsubsection{Contexts} @@ -981,13 +1042,118 @@ type-level binders, $\myprod$ and $\mytyc{W}$. } } - \section{The struggle for equality} \label{sec:equality} -\subsection{Propositional equality...} +In the previous section we saw how a type checker (or a human) needs a notion of +\emph{definitional equality}. Beyond this meta-theoretic notion, in this +section we will explore the ways of expressing equality \emph{inside} the +theory, as a reasoning tool available to the user. This area is the main +concern of this thesis, and in general a very active research topic, since we do +not have a fully satisfactory solution, yet. -\subsection{...and its limitations} +\subsection{Propositional equality} + +\noindent +\begin{minipage}{0.5\textwidth} +\mydesc{syntax}{ }{ + $ + \begin{array}{r@{\ }c@{\ }l} + \mytmsyn & ::= & \dots \\ + & | & \mytmsyn \mypeq{\mytmsyn} \mytmsyn \mysynsep + \myapp{\myrefl}{\mytmsyn} \\ + & | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn} + \end{array} + $ +} +\end{minipage} +\begin{minipage}{0.5\textwidth} +\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{ + \centering{ + $ + \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn + $ + } + \vspace{0.9cm} +} +\end{minipage} + +\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{ + \centering{ + \AxiomC{$\myjud{\mytya}{\mytyp_l}$} + \AxiomC{$\myjud{\mytmm}{\mytya}$} + \AxiomC{$\myjud{\mytmn}{\mytya}$} + \TrinaryInfC{$\myjud{\mytmm \mypeq{\mytya} \mytmn}{\mytyp_l}$} + \DisplayProof + + \myderivsp + + \begin{tabular}{cc} + \AxiomC{\phantom{$\myctx P \mytyp_l$}} + \noLine + \UnaryInfC{$\myjud{\mytmt}{\mytya}$} + \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\mytmt \mypeq{\mytya} \mytmt}$} + \DisplayProof + & + \AxiomC{$\myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\myb{x} \mypeq{\mytya} \myb{y}}{\mytyp_l}}}$} + \noLine + \UnaryInfC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}\hspace{1.2cm}\myjud{\myse{p}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}}$} + \UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$} + \DisplayProof + \end{tabular} + } +} + +To express equality between two terms inside ITT, the obvious way to do so is +to have the equality construction to be a type-former. Here we present what +has survived as the dominating form of equality in systems based on ITT up to +the present day. + +Our type former is $\mypeq{\mytya}$, which given a type (in this case +$\mytya$) relates equal terms of that type. $\mypeq{}$ has one introduction +rule, $\myrefl$, which introduces an equality relation between definitionally +equal terms---in the typing rule we display the term as `the same', meaning +`the same up to $\mydefeq$'. % TODO maybe mention this earlier + +Finally, we have one eliminator for $\mypeq{}$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes +\begin{itemize} +\item $\myse{P}$, a predicate working with two terms of a certain type (say + $\mytya$) and a proof of their equality +\item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and + $\myse{n}$) are equal +\item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$, plus + the trivial proof by reflexivity showing that $\myse{m}$ is equal to itself +\end{itemize} +Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied to +$\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a +witness that $\myse{P}$ works with \emph{definitionally equal} terms, and +returns a witness of $\myse{P}$ working with \emph{propositionally equal} +terms. Invokations of $\myjeqq$ will vanish when the equality proofs will +reduce to invocations to reflexivity, at which point the arguments must be +definitionally equal, and thus the provided +$\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$ +can be returned. + +While the $\myjeqq$ rule is slightly convoluted, ve can derive many more +`friendly' rules from it, for example a more obvious `substitution' rule, that +replaces equal for equal in predicates: +\[ +\begin{array}{l} +(\myabs{\myb{A}\ \myb{P}\ \myb{x}\ \myb{y}\ \myb{q}\ \myb{p}}{ + \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{q}}{\myb{p}}}) : \\ +\myind{1} \myfora{\myb{A}}{\mytyp}{\myfora{\myb{P}}{\myb{A} \myarr \mytyp}{\myfora{\myb{x}\ \myb{y}}{\myb{A}}{\myb{x} \mypeq{\myb{A}} \myb{y} \myarr \myapp{\myb{P}}{\myb{x}} \myarr \myapp{\myb{P}}{\myb{y}}}}} +\end{array} +\] +This rule is often called $\myfun{subst}$---here we will invoke it without +specifying the type ($\myb{A}$) and the sides of the equality +($\myb{x},\myb{y}$). + +Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding +equality, such as symmetry, transitivity, and a congruence law: + +% TODO finish this + +\subsection{Common extensions} eta law @@ -995,11 +1161,158 @@ congruence UIP +\subsection{Limitations} + +\epigraph{\emph{Half of my time spent doing research involves thinking up clever + schemes to avoid needing functional extensionality.}}{@larrytheliquid} + +However, propositional equality as described is quite restricted when +reasoning about equality beyond the term structure, which is what definitional +equality gives us (extension notwithstanding). + +The problem is best exemplified by \emph{function extensionality}. In +mathematics, we would expect to be able to treat functions that give equal +output for equal input as the same. When reasoning in a mechanised framework +we ought to be able to do the same: in the end, without considering the +operational behaviour, all functions equal extensionally are going to be +replaceable with one another. + +However this is not the case, or in other words with the tools we have we have +no term of type +\[ +\myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{ + \myb{A} \myarr \myb{B}}{ + (\myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{\myb{B}} \myapp{\myb{g}}{\myb{x}}}) \myarr + \myb{f} \mypeq{\myb{A} \myarr \myb{B}} \myb{g} + } +} +\] +To see why this is the case, consider the functions +\[\myabs{\myb{x}}{0 \mathrel{\myfun{+}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{+}} 0}\] +where $\myfun{+}$ is defined by recursion on the first argument, gradually +destructing it to build up successors of the second argument. The two +functions are clearly denotationally the same, and we can in fact prove that +\[ +\myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{+}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{+}} 0)} +\] +By analysis on the $\myb{x}$. However, the two functions are not +definitionally equal, and thus we won't be able to get rid of the +quantification. + +For the reasons above, theories that offer a propositional equality similar to +what we presented are called \emph{intensional}, as opposed to +\emph{extensional}. Most systems in wide use today (such as Agda, Coq and +Epigram) are of this kind. + +This is quite an annoyance that often makes reasoning awkward to execute. It +also extends to other fields, for example proving bisimulation between +processes specified by coinduction, or in general proving equivalences based +on the behaviour on a term. + \subsection{Equality reflection} +One way to `solve' this problem is by identifying propositional equality with +definitional equality: + +\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{ + \centering{ + \AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$} + \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$} + \DisplayProof + } +} + +This rule takes the name of \emph{equality reflection}, and is a very +different rule from the ones we saw up to now: it links a typing judgement +internal to the type theory to a meta-theoretic judgement that the type +checker uses to work with terms. It is easy to see the dangerous consequences +that this causes: +\begin{itemize} +\item The rule is syntax directed, and the type checker is presumably expected + to come up with equality proofs when needed. +\item More worryingly, type checking becomes undecidable also because + computing under false assumptions becomes unsafe. + Consider for example + \[ + \myabss{\myb{q}}{\mytya \mypeq{\mytyp} (\mytya \myarr \mytya)}{\myhole{?}} + \] + Using the assumed proof in tandem with equality reflection we could easily + write a classic Y combinator, sending the compiler into a loop. +\end{itemize} + +Given these facts theories employing equality reflection, like NuPRL +\citep{NuPRL}, carry the derivations that gave rise to each typing judgement +to keep the systems manageable. % TODO more info, problems with that. + +For all its faults, equality reflection does allow us to prove extensionality, +using the extensions we gave above. Assuming that $\myctx$ contains +\[\myb{A}, \myb{B} : \mytyp; \myb{f}, \myb{g} : \myb{A} \myarr \myb{B}; \myb{q} : \myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}\] +We can then derive +\begin{prooftree} + \AxiomC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{q}}{\myb{x}}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}$} + \RightLabel{equality reflection} + \UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$} + \RightLabel{congruence for $\lambda$s} + \UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$} + \RightLabel{$\eta$-law for $\lambda$} + \UnaryInfC{$\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}$} + \RightLabel{$\myrefl$} + \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\myb{f} \mypeq{} \myb{g}}$} +\end{prooftree} + +Now, the question is: do we need to give up well-behavedness of our theory to +gain extensionality? + \subsection{Observational equality} +\ref{sec:ott} + +% TODO should we explain this in detail? +A recent development by \citet{Altenkirch2007}, \emph{Observational Type + Theory} (OTT), promises to keep the well behavedness of ITT while being able +to gain many useful equality proofs\footnote{It is suspected that OTT gains + \emph{all} the equality proofs of ETT, but no proof exists yet.}, including +function extensionality. The main idea is to give the user the possibility to +\emph{coerce} (or transport) values from a type $\mytya$ to a type $\mytyb$, +if the type checker can prove structurally that $\mytya$ and $\mytya$ are +equal; and providing a value-level equality based on similar principles. A +brief overview is given below, + +\mydesc{syntax}{ }{ + $ + \begin{array}{r@{\ }c@{\ }l} + \mytmsyn & ::= & \dots \\ + & | & \myprdec{\myprsyn} \mysynsep + \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep + \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\ + \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn + \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn} \\\ + & | & \mytmsyn = \mytmsyn \mysynsep + \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} + \end{array} + $ +} +\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{ + \centering{ + } +} + +The original presentation of OTT employs the theory presented above. It is +close to the one presented in section \ref{sec:itt}, with the additions +presented above, and the change that only one the `first' universe, the type +of small types ($\mytyp_0$), is present. + +The propositional universe is meant to be where equality proofs live in. The +equality proofs are respectively between types ($\mytya = \mytyb$), and +between values + + + +However, only one universe is present ($\mytyp_0$), and a \emph{propositional} +universe is isolated, intended to be the universe where equality proofs live +in. Propositions (as long as our system is consistent) are inhabited only by +one element, and thus can all be treated as definitionally equal. + -\subsection{Univalence foundations} \section{Augmenting ITT} \label{sec:practical} @@ -1025,6 +1338,145 @@ UIP \section{\mykant} \label{sec:kant} +\mykant is an interactive theorem prover developed as part of this thesis. +The plan is to present a core language which would be capable of serving as +the basis for a more featureful system, while still presenting interesting +features and more importantly observational equality. + +The author learnt the hard way the implementations challenges for such a +project, and while there is a solid and working base to work on, observational +equality is not currently implemented. However, a detailed plan on how to add +it this functionality is provided, and should not prove to be too much work. + +\subsection{High level overview} + +\subsubsection{Features} + +The features currently implemented in \mykant are: + +\begin{description} +\item[Full dependent types] As we would expect, we have dependent a system + which is as expressive as the `best' corner in the lambda cube described in + section \ref{sec:itt}. + +\item[Implicit, cumulative universe hierarchy] The user does not need to + specify universe level explicitly, and universes are \emph{cumulative}. + +\item[User defined data types and records] Instead of forcing the user to + choose from a restricted toolbox, we let her define inductive data types, + with associated primitive recursion operators; or records, with associated + projections for each field. + +\item[Bidirectional type checking] While no `fancy' inference via unification + is present, we take advantage of an type synthesis system in the style of + \cite{Pierce2000}, extending the concept for user defined data types. + +\item[Type holes] When building up programs interactively, it is useful to + leave parts unfinished while exploring the current context. This is what + type holes are for. +\end{description} + +The planned features are: + +\begin{description} +\item[Observational equality] As described in section \label{sec:ott} but + extended to work with the type hierarchy and to admit equality between + arbitrary data types. + +\item[Coinductive data] ... +\end{description} + +We will analyse the features one by one, along with motivations and tradeoffs +for the design decisions made. + +\subsubsection{Implementation} + +The codebase consists of around 2500 lines of Haskell, as reported by the +\texttt{cloc} utility. The high level design is heavily inspired by Conor +McBride's work on various incarnations of Epigram, and specifically by the +first version as described \citep{McBride2004} and the codebase for the new +version \footnote{Available intermittently as a \texttt{darcs} repository at + \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.}. In many ways \mykant is +something in between the first and second version of Epigram. + +The interaction happens in a read-eval-print loop (REPL). The repl is a +available both as a commandline application and in a web interface, which is +available at \url{kant.mazzo.li} and presents itself as in figure +\ref{fig:kant-web}. + +\begin{figure} + \centering{ + \includegraphics[scale=1.0]{kant-web.png} + } + \caption{The \mykant web prompt.} + \label{fig:kant-web} +\end{figure} + +The interaction with the user takes place in a loop living in and updating a +context \mykant declarations. The user inputs a new declaration that goes +through various stages starts with the user inputing a \mykant declaration, +which then goes through various stages that can end up in a context update, or +in failures of various kind. The process is described in figure +\ref{fig:kant-process}. The workings of each phase will be illustrated in the +next sections. + +\begin{figure} + {\small + \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded + corners, minimum height=2.5em, node distance=0.7cm] + + \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly + centered, inner sep=0pt, node distance=0.7cm] + + \tikzstyle{line} = [draw, -latex'] + + \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text + centered, node distance=1.5cm] + + + \begin{tikzpicture}[auto] + \node [cloud] (user) {User}; + \node [block, below left=1cm and 0.1cm of user] (parse) {Parse}; + \node [block, below=of parse] (desugar) {Desugar}; + \node [block, below=of desugar] (reference) {Reference}; + \node [block, below=of reference] (elaborate) {Elaborate}; + \node [block, below=of elaborate] (tycheck) {Typecheck}; + \node [decision, right=of elaborate] (error) {Error?}; + \node [block, right=of parse] (distill) {Distill}; + \node [block, right=of desugar] (update) {Update context}; + + \path [line] (user) -- (parse); + \path [line] (parse) -- (desugar); + \path [line] (desugar) -- (reference); + \path [line] (reference) -- (elaborate); + \path [line] (elaborate) edge[bend right] (tycheck); + \path [line] (tycheck) edge[bend right] (elaborate); + \path [line] (elaborate) -- (error); + \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill); + \path [line] (error) -- node [near start] {no} (update); + \path [line] (update) -- (distill); + \path [line] (distill) -- (user); + + + \end{tikzpicture} + } + \caption{High level overview of the life of a \mykant prompt cycle.} + \label{fig:kant-process} +\end{figure} + +\subsection{Bidirectional type checking} + +We start by describing bidirectional type checking since it calls for fairly +different typing rules that what we have seen up to now. The idea is to have +two kind of terms: terms for which a type can always be inferred, and terms +that need to be checked against a type. A nice observation is that this +duality runs through the semantics of the terms: data destructors (function +application, record projections, primitive recursors) \emph{infer} types, +while data constructors (abstractions, record/data types data constructors) +need to be checked. + +To introduce the concept and notation, we will revisit the STLC in a +bidirectional style. \appendix @@ -1035,7 +1487,7 @@ the type of relation being established and the syntactic elements appearing, for example \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{ - Typing derivations here. + \centering{Typing derivations here.} } In the languages presented and Agda code samples I also highlight the syntax, @@ -1114,6 +1566,19 @@ module ITT where (x : W S P) → -- If so, ... C x -- ...C always holds. rec C c (s ◁ f) = c s f (λ p → rec C c (f p)) + + data _≡_ {a} {A : Set a} : A → A → Set a where + refl : ∀ x → x ≡ x + + J : ∀ {a b} {A : Set a} + (P : (x y : A) → x ≡ y → Set b) → + ∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y + J P p (refl x) = p + + subst : ∀ {a b} {A : Set a} + (P : A → Set b) → + ∀ {x y} → (x≡y : x ≡ y) → P x → P y + subst P q p = J (λ _ y _ → P y) p q \end{code} \nocite{*} -- 2.30.2