addfile ./Makefile hunk ./Makefile 1 +# General makefile for Latex stuff + +.SUFFIXES: .tib .verb .tex .fig .dvi .ps + + +MAIN = dependent-kinds + +# Styles are in papers/styles +TEXINPUTS := .:../styles//:$(TEXINPUTS) + +# Bibliographies are in papers/bibs +BIBINPUTS := .:../bibs//:$(BIBINPUTS) + +default: $(MAIN).pdf +# basic-algo-and-proofs.ps chr-based-approach.ps + +$(MAIN).pdf : always + +# Depending on 'always' ensures that the work is redone +.PHONY : always +always: + +######## General rules + +.verb.tex: + expand $*.verb | verbatim > $*.tex + +%.pdf : %.tex + pdflatex $*.tex + -bibtex $* +# AcroRd32 $*.pdf + touch always + +# Cancel this +%.dvi : %.tex + +%.ps : %.pdf + pdf2ps $*.pdf $*.ps + +%.ps : %.dvi + dvips -f -t a4 < $*.dvi > $*.ps + ps2pdf $*.ps + addfile ./abbrev.sty hunk ./abbrev.sty 1 +% abbrev.sty - make ascii symbols active commands in math mode. +% +% Original from Maarten Fokkinga, Feb 1991, after an idea of Jeremy Gibbons. + +% There are two main parts +% +% 1. ABBREVIATIONS maps char sequences to commands +% e.g. |- ==> \barMinus +% (generally not to be altered) +% +% 2. MAPPING maps commands to Latex commands +% e.g. \barMinus ==> \vdash +% (feel free to redefine these) + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% 2. MAPPING + + +\def\dquote{\text{\char'175}} % " +\def\lquote{\text{`}} % ` +\def\periodi{\mathrel{\PERIOD}} % . +\def\periodii{\PERIOD\PERIOD} % .. +\def\periodiii{\ldots} % ... +\def\slashEquals{\neq} % /= +\def\twiddleEquals{\cong} % ~= +\def\lessthan{\mathopen{\langle}} % < +\def\greaterthan{\mathclose{\rangle}} % > +\def\equalsGreater{\Rightarrow} % => +\def\equalsEqualsGreater{\Longrightarrow} % ==> +\def\equalsEqualsEqualsGreater{\Longrightarrow} % ===> +\def\lessEquals{\Leftarrow} % <= +\def\lessEqualsEquals{\Longleftarrow} % <== +\def\lessEqualsEqualsEquals{\Longleftarrow} % <=== +\def\lessEqualsGreater{\Leftrightarrow} % <=> +\def\lessEqualsEqualsGreater{\Longleftrightarrow} % <==> +\def\lessEqualsEqualsEqualsGreater{\Longleftrightarrow} % <===> +\def\equalsEquals{\equiv} % == +\def\equalsEqualsEquals{&{}={}&} % === +\def\minusGreater{\rightarrow} % -> +\def\minusMinusGreater{\longrightarrow} % --> +\def\minusPeriodMinusGreater{\dot{\rightarrow}} % -.-> +\def\lquoteMinusMinusGreater{\hookrightarrow} % `--> +\def\minusLittleO{\multimap} % -o +\def\minusSlashMinusGreater{\not \rightarrow} % -/-> +\def\lessMinus{\leftarrow} % <- +\def\lessMinusMinus{\longleftarrow} % <-- +\def\lessBar{\triangleleft} % <| +\def\lessBarGreater{\mathrel{\triangleleft\mspace{-3mu}\triangleright}} % <|> +\def\minusLquote{\rightharpoonup} % -` +\def\greaterLess{\times} % >< +\def\lessPlusGreater{\oplus} % <+> +\def\lessTimesGreater{\otimes} % <*> +\def\colon{\COLON} % : +\def\colonColon{\mathbin{\COLON\COLON}} % :: +\def\colonColonEquals{\mathbin{\mathord{\COLON}\mathord{\COLON}\mathord{=}}} + % ::= +\def\semicolon{\mathbin{\SEMICOLON}} % ; +\def\justABar{\mathrel{\BAR}} % | +\def\barBarMinus{\Vdash} % ||- +\def\barEquals{\mathrel{\BAR\mspace{-8mu}\EQUALS}} % |= +\def\barMinus{\vdash} % |- +\def\minusBar{\dashv} % -| +\def\barMinusMinus#1{\vdash_{#1}} % |-- +\def\barMinusGreater{\mapsto} % |-> +\def\barMinusMinusGreater{\longmapsto} % |--> +\def\barMinusMinusGreaterGreater{\mapsto\hspace*{-8pt}\rightarrow} + % |-->> +\def\barVeeBar{\Downarrow} % |v| +\def\barCircBar{\Uparrow} % |^| +\def\barGreater{\triangleright} % |> + +% Semantic brackets +\def\lessLess{[\![} % << +\def\lessLessLess{\left[\!\!\left[} % <<< +\def\greaterGreater{]\!]} % >> +\def\greaterGreaterGreater{\right]\!\!\right]} % >>> + +\def\twiddleTwiddleGreater{\rightsquigarrow} % ~~> +\def\asterisk{\ASTERISK} % * +\def\asteriskii{\overline{\ASTERISK}} % ** +\def\asteriskiii{\dagger} % *** +\def\asteriskiv{\star} % **** +\def\asteriskv{\ddagger} % ***** +\def\plusPlus{\mathbin{\PLUS\hspace*{-4pt}\PLUS}} % ++ +\def\bang{\mathalpha{\BANG}} % ! +\def\bangLittleW{\mathalpha{\BANG}^w} % !w +\def\bangLittleC{\mathalpha{\BANG}^c} % !c +\def\bangLittleI{\mathalpha{\BANG}^i} % !i +\def\question{\mathalpha{\QUESTION}} % ? +\def\greaterLittleI{\mathclose{\rangle}^{\!!i}} % >i +\def\greaterLittleW{\mathclose{\rangle}^{\!!w}} % >w +\def\greaterLittleC{\mathclose{\rangle}^{\!!c}} % >c +\def\greaterLittleL{\mathclose{\rangle}^{\!!l}} % >l +\def\slashBackslash{\wedge} % /\ + +% Spacing +\def\twiddlei{\TWIDDLE} % ~ +\def\twiddleii{\;} % ~~ +\def\twiddleiii{\quad} % ~~~ + +% These next ones are intended to work with prooftree.sty +% E.g. +% \prooftree +% \Gamma |- \ol{\upsilon} ~~~ +% ----------------------------------------{type} +% \Gamma |- {\tt type}\;\ol{a}\;{\tt in}\; t : \tau +% ~~~~~ +% \begin{array}{c} +% \ol{a} = extfv(\upsilon) ~~~ +% \Gamma |- \ol{\upsilon'} \\ +% \Gamma, x : [\ol{a |-> \upsilon'}]\;\upsilon |- +% [\ol{a |-> \upsilon'}]\;t : \tau +% \end{array} +% ----------------------------------------{aabs} +% \Gamma |- {\tt \backslash}(x\;{\tt ::}\;\upsilon) . t : +% ([\ol{a |-> \upsilon'}]\;\upsilon) -> \tau +% \endprooftree \\ + +\def\twiddleiv{\endprooftree\qquad\prooftree} % ~~~~ +\def\twiddlev{\endprooftree\\ \\ \prooftree} % ~~~~~... +\def\rulename#1{\textsc{#1}} +\def\minusv#1{\using\text{\rulename{#1}}\justifies} % -----... + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% 1. ABBREVIATIONS +% +% Within mathmode, the command defined in the right column below is invoked +% when you type the symbol sequence of the left column. +% -- You may redefine any command in the left column! +% By default it just reproduces the sequence that invoked it. +% Of course, your redefinition may make it a n-parameter command. +% -- Be sure to type spaces in between the symbols if you don't want to +% invoke the command that it abbreviates! Eg ~ ~ is not equivalent +% to ~~ . +% +% " invokes \dquote +% ` invokes \lquote +% `--> invoked \lquoteMinusMinusGreater +% : invokes \colon +% :: invokes \colonColon +% :l: invokes \colonLColon +% :k: invokes \colonKColon +% :h: invokes \colonHColon +% :0: invokes \colonZeroColon +% :1: invokes \colonOneColon +% ::= invokes \colonColonEquals +% ; invokes \semicolon +% ~ invokes \twiddlei +% ~~ invokes \twiddleii +% ~~~ invokes \twiddleiii +% ~~~~ invokes \twiddleiv +% ~~~~~... invokes \twiddlev +% ~= invokes \twiddleEquals +% ~~> invokes \twiddleTwiddleGreater +% /= invokes \slashEquals +% =< invokes \equalsLess +% => invokes \equalsGreater +% ==> invokes \equalsEqualsGreater +% == invokes \equalsEquals +% === invokes \equalsEqualsEquals +% ==== invokes \equalsiv +% =====... invokes \equalsv +% | invokes \justABar +% || invokes \barBar +% ||- invokes \barBarMinus +% |> invokes \barGreater +% |( invokes \barLpar +% |) invokes \barRpar +% |v| invokes \barVeeBar +% |^| invokes \barCircBar +% |- invokes \barMinus +% |-- invokes \barMinusMinus +% |= invokes \barEquals +% |-> invokes \barMinusGreater +% |--> invokes \barMinusMinusGreater +% |-->> invokes \barMinusMinusGreaterGreater +% << invokes \lessLess +% <<< invokes \lessLessLess +% <= invokes \lessEquals +% <=> invokes \lessEqualsGreater +% <==> invokes \lessEqualsEqualsGreater +% <== invokes \lessEqualsEquals +% <+ invokes \lessPlus +% <+> invokes \lessPlusGreater +% <* invokes \lessTimes +% <*> invokes \lessTimesGreater +% <- invokes \lessMinus +% <-- invokes \lessMinusMinus +% <| invokes \lessBar +% <|> invokes \lessBarGreater +% >< invokes \greaterLess +% >= invokes \greaterEquals +% >- invokes \greaterMinus +% >+ invokes \greaterPlus +% >i invokes \greaterLittleI +% >w invokes \greaterLittleW +% >c invokes \greaterLittleC +% >l invokes \greaterLittleL +% >> invokes \greaterGreater +% >>> invokes \greaterGreaterGreater +% -| invokes \minusBar +% -> invokes \minusGreater +% --> invokes \minusMinusGreater +% -/-> invokes \minusSlashMinusGreater +% -.-> invokes \minusPeriodMinusGreater +% -` invokes \minusLquote +% -o invokes \minusLittleO +% -- invokes \minusMinus +% --- invokes \minusiii +% ---- invokes \minusiv +% -----... invokes \minusv +% . invokes \periodi +% .. invokes \periodii +% ... invokes \periodiii +% .... invokes \periodiv +% * invokes \asterisk +% ** invokes \asteriskii +% *** invokes \asteriskiii +% **** invokes \asteriskiv +% ***** invokes \asteriskv +% ****** invokes \asteriskvi +% ******* invokes \asteriskvii +% ! invokes \bang +% !w invokes \bangLittleW +% !c invokes \bangLittleC +% !i invokes \bankLittleI +% ? invokes \question +% ?w invokes \questionLittleW +% ?c invokes \questionLittleC +% ?i invokes \questionLittleI +% ++ invokes \plusPlus +% +< invokes \plusLess +% / invokes \slash +% /\ invokes \slashBackslash +% // invokes \slashSlash +% /< invokes \slashLess +% /> invokes \slashGreater +% //> invokes \slashSlashGreater +% //< invokes \slashSlashLess + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% SAVED SYMBOLS +% +% " is saved as \DQUOTE +% ` is saved as \LQUOTE +% ~ is saved as \TWIDDLE +% . is saved as \PERIOD +% = is saved as \EQUALS +% - is saved as \MINUS +% * is saved as \ASTERISK +% / is saved as \SLASH +% | is saved as \BAR +% : is saved as \COLON +% ; is saved as \SEMICOLON +% < is saved as \LT +% > is saved as \GT +% + is saved as \PLUS +% ! is saved as \BANG +% ? is saved as \QUESTION +% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% MECHANISM FOR MAKING (SINGLE OR MULTIPLE CHAR) ABBREVIATIONS IN MATH MODE +% +% To make the symbol . active in math mode as \compose do following: +% +% \mathchardef\P=\mathcode`. % Save current meaning of . in \P +% \mathcode`.="8000 % Make . active in math mode. +% {\catcode`.=\active +% \gdef.{\compose} % Define . to be \compose . +% } +% +% To get <= as abbreviation for \leq do following: +% +% \mathchardef\@lt=\mathcode`< % Save < (only temporarily) in \@lt . +% \mathcode`<="8000 % Make < active in math mode. +% {\catcode`<=\active +% \gdef<{\futurelet\@NEXT\@lessthan} +% } % Define < to be \@lessthan +% % (after \futurelet has defined \@NEXT +% % to be what will come next). +% \def\@lessthan{% +% \ifx=\@NEXT % If \@NEXT (defined above) equals = , +% \def\@NEXT##1{\leq} % REDEFINE \@NEXT (with ONE parameter!) +% \else % otherwise +% \def\@NEXT{\@lt} % REDEFINE \@NEXT (with NO parameter!) +% % (remember, \@lt is the saved old < ); +% \fi % +% \@NEXT} % call the \@NEXT thus defined +% % (each parameter will consume one token). +% +% NOTE: +% {<} always produces just < but due to the braces as an ORDinary symbol. +% So {<}= gives: +% and < = gives: +% and <= gives: \leq . +% +% There can be multiple-character abbreviations and any number of +% alternatives; e.g., to get +% <=> , <= , <> , < as an abbreviation for respectively +% \iff , \leq, \diamond , \lessthan redefine \@lessthan as follows: +% +% \def\@lessthan{% +% \ifx>\@NEXT \def\@NEXT##1{\diamond}\else +% \ifx=\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@lessthanEqual}\else +% \def\@NEXT{\@lt}\fi\fi\@NEXT} +% \def\@lessthanEqual{% +% \ifx>\@NEXT \def\@NEXT##1{\iff}\else +% \def\@NEXT{\leq}\fi\@NEXT} +% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% +% WARNING WARNING WARNING: +% +% TeX, and possibly some other macros that you use, use some symbols like +% -,=,.. as if they are really mathchars, whereas by the abbreviations below +% these symbols are macros. For example, plain TeX defines \Relbar by +% \def\Relbar{\mathrel=} +% and then \mathrel complains that it is not followed by the right kind of +% token (see TeX book p.358); we have to redefine \Relbar as +% \def\Relbar{\mathrel{=}} +% Similarly for the plain TeX definition of \models . +% I don't know whether there will appear more of such definitions that are +% screwed up by the abbreviations below ...... + +\def\relbar{\mathrel{-}} +\def\Relbar{\mathrel{=}} % Plain TeX: \def\Relbar{\mathrel=} +%% \def\models{\mathrel{|}\joinrel=} % Plain TeX: +%% \def\models{\mathrel|\joinrel=} + +%% DQUOTE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% Be carefull: dutch.sty (LaTeX2e) activates " too! +\let\@DQUOTE=" % Save " as \@DQUOTE in text mode +\mathchardef\DQUOTE=\mathcode`" % Save " as \DQUOTE in math mode +\mathcode`"="8000 +{\catcode`"=\active + \gdef"{\ifmmode\dquote\else\@DQUOTE\fi}} % parameter deleted, aug95 + +%% LQUOTE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\mathchardef\LQUOTE=\mathcode`` +\mathcode``="8000 +{\catcode``=\active\gdef`{\futurelet\@NEXT\@lquote}} +\def\@lquote{% + \ifx-\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@lquoteMinus}\else + \def\@NEXT{\lquote}\fi\@NEXT} +\def\@lquoteMinus{% + \ifx-\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@lquoteMinusMinus}\else + \def\@NEXT{\lquoteMinus}\fi\@NEXT} +\def\@lquoteMinusMinus{% + \ifx>\@NEXT \def\@NEXT##1{\lquoteMinusMinusGreater}\else + \def\@NEXT{\lquoteMinusMinus}\fi\@NEXT} + +%% COLON %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\mathchardef\COLON=\mathcode`: % Save : as \COLON in math mode +\mathcode`:="8000 +{\catcode`:=\active\gdef:{\futurelet\@NEXT\@colon}} +\def\@colon{% + \ifx:\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@colonColon}\else + \ifx l\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@colonL}\else + \ifx k\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@colonK}\else + \ifx h\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@colonH}\else + \ifx 0\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@colonZero}\else + \ifx 1\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@colonOne}\else + \def\@NEXT{\colon}\fi\fi\fi\fi\fi\fi\@NEXT} +\def\@colonColon{% + \ifx=\@NEXT \def\@NEXT##1{\colonColonEquals}\else + \def\@NEXT{\colonColon}\fi\@NEXT} +\def\@colonL{% + \ifx:\@NEXT \def\@NEXT##1{\colonLColon}\else + \def\@NEXT{\colonL}\fi\@NEXT} +\def\@colonK{% + \ifx:\@NEXT \def\@NEXT##1{\colonKColon}\else + \def\@NEXT{\colonK}\fi\@NEXT} +\def\@colonH{% + \ifx:\@NEXT \def\@NEXT##1{\colonHColon}\else + \def\@NEXT{\colonH}\fi\@NEXT} +\def\@colonZero{% + \ifx:\@NEXT \def\@NEXT##1{\colonZeroColon}\else + \def\@NEXT{\colonZero}\fi\@NEXT} +\def\@colonOne{% + \ifx:\@NEXT \def\@NEXT##1{\colonOneColon}\else + \def\@NEXT{\colonOne}\fi\@NEXT} + +%% SEMICOLON %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\mathchardef\SEMICOLON=\mathcode`; % Save : as \COLON in math mode +\mathcode`;="8000 +{\catcode`;=\active\gdef;{\semicolon}} + +%% PERIOD %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\mathchardef\PERIOD=\mathcode`. % Save . as \PERIOD in math mode +\mathcode`.="8000 +{\catcode`.=\active\gdef.{\futurelet\@NEXT\@periodi}} +\def\@periodi{% + \ifx.\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@periodii}\else + \def\@NEXT{\periodi}\fi\@NEXT} +\def\@periodii{% + \ifx.\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@periodiii}\else + \def\@NEXT{\periodii}\fi\@NEXT} +\def\@periodiii{% + \ifx.\@NEXT \def\@NEXT##1{\futurelet\@NEXT\periodiv}\else + \def\@NEXT{\periodiii}\fi\@NEXT} + +%% EQUALS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\mathchardef\EQUALS=\mathcode`= +\mathcode`=="8000 +{\catcode`==\active \gdef={\futurelet\@NEXT\@equal}} +\def\@equal{% + \ifx>\@NEXT \def\@NEXT##1{\equalsGreater}\else + \ifx<\@NEXT \def\@NEXT##1{\equalsLess}\else + \ifx=\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@equalsEquals}\else + \ifx d\@NEXT\def\@NEXT##1{\futurelet\@NEXT\@equald}\else + \def\@NEXT{\EQUALS}\fi\fi\fi\fi\@NEXT} +\def\@equalsEquals{% + \ifx>\@NEXT \def\@NEXT##1{\equalsEqualsGreater}\else + \ifx=\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@equalsEqualsEquals}\else + \def\@NEXT{\equalsEquals}\fi\fi\@NEXT} +\def\@equalsEqualsEquals{% + \ifx>\@NEXT \def\@NEXT##1{\equalsEqualsEqualsGreater}\else + \ifx=\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@equalsiv}\else + \def\@NEXT{\equalsEqualsEquals}\fi\fi\@NEXT} +\def\@equald{% + \ifx e\@NEXT\def\@NEXT##1{\futurelet\@NEXT\@equalde}\else + \def\@NEXT{\EQUALS d}\fi\@NEXT} +\def\@equalde{% + \ifx f\@NEXT\def\@NEXT##1{\equalsdef}\else + \def\@NEXT{\EQUALS de}\fi\@NEXT} +\def\@equalsiv{% + \ifx=\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@equalsv}\else + \def\@NEXT{\equalsiv}\fi\@NEXT} +\def\@equalsv{% + \ifx=\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@equalsv}\else + \def\@NEXT{\equalsv}\fi\@NEXT} + +%% TWIDDLE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% new twiddle (changed March 1992 by mmf) +\let\@TWIDDLE=~ % Save text twiddle as \@TWIDDLE +\mathchardef\TWIDDLE=\mathcode`~ % Save ~ as \TWIDDLE in math mode +{\catcode`~=\active\gdef~{\futurelet\@NEXT\@twiddlei}} +\mathcode`~="8000 + +\def\@twiddlei{% + \ifx~\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@twiddleii}\else + \ifx=\@NEXT \def\@NEXT##1{\futurelet\@NEXT\twiddleEquals}\else + \def\@NEXT{\ifmmode\twiddlei\else\@TWIDi\fi}\fi\fi\@NEXT} +\def\@twiddleii{% + \ifx~\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@twiddleiii}\else + \ifx>\@NEXT \def\@NEXT##1{\futurelet\@NEXT\twiddleTwiddleGreater}\else + \def\@NEXT{\ifmmode\twiddleii\else\@TWIDii\fi}\fi\fi\@NEXT} +\def\@twiddleiii{% + \ifx~\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@twiddleiv}\else + \def\@NEXT{\ifmmode\twiddleiii\else\@TWIDiii\fi}\fi\@NEXT} +\def\@twiddleiv{% + \ifx~\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@twiddlev}\else + \def\@NEXT{\ifmmode\twiddleiv\else\@TWIDiv\fi}\fi\@NEXT} +\def\@twiddleiv{% + \ifx~\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@twiddlev}\else + \def\@NEXT{\ifmmode\twiddleiv\else\@TWIDiv\fi}\fi\@NEXT} +\def\@twiddlev{% + \ifx~\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@twiddlev}\else + \def\@NEXT{\ifmmode\twiddlev\else\@TWIDv\fi}\fi\@NEXT} +% WARNING: If not in math mode, ~~~~~... considered as ~~~~~ + +\def\@TWIDi{\@TWIDDLE} +\def\@TWIDii{\@TWIDDLE\@TWIDDLE} +\def\@TWIDiii{\@TWIDDLE\@TWIDDLE\@TWIDDLE} +\def\@TWIDiv{\@TWIDDLE\@TWIDDLE\@TWIDDLE\@TWIDDLE} +\def\@TWIDv{\@TWIDDLE\@TWIDDLE\@TWIDDLE\@TWIDDLE\@TWIDDLE} + +%% MINUS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\mathchardef\MINUS=\mathcode`- +\mathcode`-="8000 +{\catcode`-=\active \gdef-{\futurelet\@NEXT\@@@minus}} +\def\@@@minus{% + \ifx>\@NEXT \def\@NEXT##1{\minusGreater}\else + \ifx/\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@minusSlash}\else + \ifx.\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@minusPeriod}\else + \ifx`\@NEXT \def\@NEXT##1{\minusLquote}\else + \ifx o\@NEXT \def\@NEXT##1{\minusLittleO}\else + \ifx|\@NEXT \def\@NEXT##1{\minusBar}\else + \ifx-\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@minusMinus}\else + \def\@NEXT{\MINUS}\fi\fi\fi\fi\fi\fi\fi\@NEXT} +\def\@minusPeriod{% + \ifx-\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@minusPeriodMinus}\else + \def\@NEXT{\minusPeriod}\fi\@NEXT} +\def\@minusPeriodMinus{% + \ifx>\@NEXT \def\@NEXT##1{\minusPeriodMinusGreater}\else + \def\@NEXT{\minusPeriodMinus}\fi\@NEXT} +\def\@minusMinus{% + \ifx>\@NEXT \def\@NEXT##1{\minusMinusGreater}\else + \ifx-\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@minusiii}\else + \def\@NEXT{\minusMinus}\fi\fi\@NEXT} +\def\@minusSlash{% + \ifx-\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@minusSlashMinus}\else + \def\@NEXT{\minusSlash}\fi\@NEXT} +\def\@minusSlashMinus{% + \ifx>\@NEXT \def\@NEXT##1{\minusSlashMinusGreater}\else + \def\@NEXT{\minusSlashMinus}\fi\@NEXT} +\def\@minusiii{% + \ifx-\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@minusiv}\else + \def\@NEXT{\minusiii}\fi\@NEXT} +\def\@minusiv{% + \ifx-\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@minusv}\else + \def\@NEXT{\minusiv}\fi\@NEXT} +\def\@minusv{% + \ifx-\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@minusv}\else + \def\@NEXT{\minusv}\fi\@NEXT} + +%% BAR %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\mathchardef\BAR=\mathcode`| +\mathcode`|="8000 +{\catcode`|=\active \gdef|{\futurelet\@NEXT\@bar}} +\def\@bar{% + \ifx|\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@barBar}\else + \ifx(\@NEXT \def\@NEXT##1{\barLpar}\else + \ifx)\@NEXT \def\@NEXT##1{\barRpar}\else + \ifx>\@NEXT \def\@NEXT##1{\barGreater}\else + \ifx-\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@barMinus}\else + \ifx v\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@barVee}\else + \ifx^\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@barCirc}\else + \ifx=\@NEXT \def\@NEXT##1{\barEquals}\else + \def\@NEXT{\justABar}\fi\fi\fi\fi\fi\fi\fi\fi\@NEXT} +\def\@barBar{% + \ifx-\@NEXT \def\@NEXT##1{\barBarMinus}\else + \def\@NEXT{\barBar}\fi\@NEXT} +\def\@barMinus{% + \ifx>\@NEXT \def\@NEXT##1{\barMinusGreater}\else + \ifx-\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@barMinusMinus}\else + \def\@NEXT{\barMinus}\fi\fi\@NEXT} +\def\@barVee{% + \ifx|\@NEXT \def\@NEXT##1{\barVeeBar}\else + \def\@NEXT{\barVee}\fi\@NEXT} +\def\@barCirc{% + \ifx|\@NEXT \def\@NEXT##1{\barCircBar}\else + \def\@NEXT{\barCirc}\fi\@NEXT} +\def\@barMinusMinus{% + \ifx>\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@barMinusMinusGreater}\else + \def\@NEXT{\barMinusMinus}\fi\@NEXT} +\def\@barMinusMinusGreater{% + \ifx>\@NEXT \def\@NEXT##1{\barMinusMinusGreaterGreater}\else + \def\@NEXT{\barMinusMinusGreater}\fi\@NEXT} + +%% ASTERISK %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\mathchardef\ASTERISK=\mathcode`* +\mathcode`*="8000 +{\catcode`*=\active \gdef*{\futurelet\@NEXT\@asterisk}} +\def\@asterisk{% + \ifx*\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@asteriskii}\else + \def\@NEXT{\asterisk}\fi\@NEXT} +\def\@asteriskii{% + \ifx*\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@asteriskiii}\else + \def\@NEXT{\asteriskii}\fi\@NEXT} +\def\@asteriskiii{% + \ifx*\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@asteriskiv}\else + \def\@NEXT{\asteriskiii}\fi\@NEXT} +\def\@asteriskiv{% + \ifx*\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@asteriskv}\else + \def\@NEXT{\asteriskiv}\fi\@NEXT} +\def\@asteriskv{% + \ifx*\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@asteriskvi}\else + \def\@NEXT{\asteriskv}\fi\@NEXT} +\def\@asteriskvi{% + \ifx*\@NEXT \def\@NEXT##1{\futurelet\@NEXT\asteriskvii}\else + \def\@NEXT{\asteriskvi}\fi\@NEXT} + +%% PLUS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\mathchardef\PLUS=\mathcode`+ +\mathcode`+="8000 +{\catcode`+=\active \gdef+{\futurelet\@NEXT\@@@plus}} +\def\@@@plus{% + \ifx+\@NEXT \def\@NEXT##1{\plusPlus}\else + \ifx<\@NEXT \def\@NEXT##1{\plusLess}\else + \def\@NEXT{\PLUS}\fi\fi\@NEXT} + +%% BANG %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\mathchardef\BANG=\mathcode`! +\mathcode`!="8000 +{\catcode`!=\active \gdef!{\futurelet\@NEXT\@bang}} +\def\@bang{% + \ifx w\@NEXT \def\@NEXT##1{\bangLittleW}\else + \ifx c\@NEXT \def\@NEXT##1{\bangLittleC}\else + \ifx i\@NEXT \def\@NEXT##1{\bangLittleI}\else + \def\@NEXT{\bang}\fi\fi\fi\@NEXT} + +%% QUESTION %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\mathchardef\QUESTION=\mathcode`? +\mathcode`?="8000 +{\catcode`?=\active \gdef?{\futurelet\@NEXT\@question}} +\def\@question{% + \ifx w\@NEXT \def\@NEXT##1{\questionLittleW}\else + \ifx c\@NEXT \def\@NEXT##1{\questionLittleC}\else + \ifx i\@NEXT \def\@NEXT##1{\questionLittleI}\else + \def\@NEXT{\question}\fi\fi\fi\@NEXT} + +%% LT %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\mathchardef\LT=\mathcode`< +\mathcode`<="8000 +{\catcode`<=\active \gdef<{\futurelet\@NEXT\@lessthan}} +\def\@lessthan{% + \ifx=\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@lessthanEqual}\else + \ifx+\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@lessPlus}\else + \ifx*\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@lessTimes}\else + \ifx<\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@lessLess}\else + \ifx|\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@lessBar}\else + \ifx-\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@lessMinus}\else + \def\@NEXT{\lessthan}\fi\fi\fi\fi\fi\fi\@NEXT} +\def\@lessPlus{% + \ifx>\@NEXT \def\@NEXT##1{\lessPlusGreater}\else + \def\@NEXT{\lessPlus}\fi\@NEXT} +\def\@lessTimes{% + \ifx>\@NEXT \def\@NEXT##1{\lessTimesGreater}\else + \def\@NEXT{\lessTimes}\fi\@NEXT} +\def\@lessMinus{% + \ifx-\@NEXT \def\@NEXT##1{\lessMinusMinus}\else + \def\@NEXT{\lessMinus}\fi\@NEXT} +\def\@lessBar{% + \ifx>\@NEXT \def\@NEXT##1{\lessBarGreater}\else + \def\@NEXT{\lessBar}\fi\@NEXT} +\def\@lessthanEqual{% + \ifx>\@NEXT \def\@NEXT##1{\lessEqualsGreater}\else + \ifx=\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@lessthanEqualEqual}\else + \def\@NEXT{\lessEquals}\fi\fi\@NEXT} +\def\@lessthanEqualEqual{% + \ifx>\@NEXT \def\@NEXT##1{\lessEqualsEqualsGreater}\else + \ifx=\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@lessthanEqualEqualEqual}\else + \def\@NEXT{\lessEqualsEquals}\fi\fi\@NEXT} +\def\@lessthanEqualEqualEqual{% + \ifx>\@NEXT \def\@NEXT##1{\lessEqualsEqualEqualsGreater}\else + \def\@NEXT{\lessEqualsEqualsEquals}\fi\@NEXT} +\def\@lessLess{% + \ifx<\@NEXT \def\@NEXT##1{\lessLessLess}\else + \def\@NEXT{\lessLess}\fi\@NEXT} + +%% GT %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\mathchardef\GT=\mathcode`> +\mathcode`>="8000 +{\catcode`>=\active \gdef>{\futurelet\@NEXT\@greaterthan}} +\def\@greaterthan{% + \ifx=\@NEXT \def\@NEXT##1{\greaterEquals}\else + \ifx i\@NEXT \def\@NEXT##1{\greaterLittleI}\else + \ifx w\@NEXT \def\@NEXT##1{\greaterLittleW}\else + \ifx c\@NEXT \def\@NEXT##1{\greaterLittleC}\else + \ifx l\@NEXT \def\@NEXT##1{\greaterLittleL}\else + \ifx>\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@greaterGreater}\else + \ifx<\@NEXT \def\@NEXT##1{\greaterLess}\else + \ifx+\@NEXT \def\@NEXT##1{\greaterPlus}\else + \ifx-\@NEXT \def\@NEXT##1{\greaterMinus}\else + \def\@NEXT{\greaterthan}\fi\fi\fi\fi\fi\fi\fi\fi\fi\@NEXT} +\def\@greaterGreater{% + \ifx>\@NEXT \def\@NEXT##1{\greaterGreaterGreater}\else + \def\@NEXT{\greaterGreater}\fi\@NEXT} + +%% SLASH %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\mathchardef\SLASH=\mathcode`/ +\mathcode`/="8000 +{\catcode`/=\active \gdef/{\futurelet\@NEXT\@slash}} +\def\@slash{% + \ifx/\@NEXT \def\@NEXT##1{\futurelet\@NEXT\@slashSlash}\else + \ifx\ \@NEXT \def\@NEXT##1{\slashBackslash}\else + \ifx=\@NEXT \def\@NEXT##1{\slashEquals}\else + \ifx>\@NEXT \def\@NEXT##1{\slashGreater}\else + \ifx<\@NEXT \def\@NEXT##1{\slashLess}\else + \def\@NEXT{\SLASH}\fi\fi\fi\fi\fi\@NEXT} +\def\@slashSlash{% + \ifx>\@NEXT \def\@NEXT##1{\slashSlashGreater}\else + \ifx<\@NEXT \def\@NEXT##1{\slashSlashLess}\else + \def\@NEXT{\slashSlash}\fi\fi\@NEXT} + +% eof addfile ./abbrevmap.tex hunk ./abbrevmap.tex 1 +% $Id: abbrevmap.tex,v 1.1 2009-06-08 10:14:37 dimitriv Exp $ + +\def\dquote{\text{\char'175}} % " +\def\lquote{\text{`}} % ` +\def\periodi{\PERIOD} % . +\def\periodii{\PERIOD\PERIOD} % .. +\def\periodiii{\ldots} % ... +\def\slashEquals{\neq} % /= +\def\twiddleEquals{\cong} % ~= +\def\lessthan{\mathopen{\langle}} % < +\def\greaterthan{\mathclose{\rangle}} % > +\def\equalsGreater{\Rightarrow} % => +\def\equalsEqualsGreater{\Longrightarrow} % ==> +\def\equalsEqualsEqualsGreater{\Longrightarrow} % ===> +\def\lessEquals{\Leftarrow} % <= +\def\lessEqualsEquals{\Longleftarrow} % <== +\def\lessEqualsEqualsEquals{\Longleftarrow} % <=== +\def\lessEqualsGreater{\Leftrightarrow} % <=> +\def\lessEqualsEqualsGreater{\Longleftrightarrow} % <==> +\def\lessEqualsEqualsEqualsGreater{\Longleftrightarrow} % <===> +\def\equalsEquals{\equiv} % == +\def\equalsEqualsEquals{&{}={}&} % === +\def\minusGreater{\to} % -> +\def\minusMinusGreater{\longrightarrow} % --> +\def\minusPeriodMinusGreater{\dot{\to}} % -.-> +\def\lquoteMinusMinusGreater{\hookrightarrow} % `--> +\def\minusLittleO{\multimap} % -o +\def\minusSlashMinusGreater{\not \to} % -/-> +\def\lessMinus{\gets} % <- +\def\lessMinusMinus{\longleftarrow} % <-- +\def\lessBar{\triangleleft} % <| +\def\lessBarGreater{\mathrel{\triangleleft\mspace{-3mu}\triangleright}} % <|> +\def\minusLquote{\rightharpoonup} % -` +\def\greaterLess{\times} % >< +\def\lessPlusGreater{\oplus} % <+> +\def\lessTimesGreater{\otimes} % <*> +\def\colon{\COLON} % : +\def\colonColon{\mathbin{\COLON\COLON}} % :: +\def\colonColonEquals{\mathbin{\mathord{\COLON}\mathord{\COLON}\mathord{=}}} + % ::= +\def\semicolon{\mathbin{\SEMICOLON}} % ; +\def\justABar{\mathrel{\BAR}} % | +\def\barBarMinus{\Vdash} % ||- +\def\barEquals{\mathrel{\BAR\mspace{-8mu}\EQUALS}} % |= +\def\barMinus{\vdash} % |- +\def\minusBar{\dashv} % -| +\def\barMinusMinus#1{\vdash_{#1}} % |-- +\def\barMinusGreater{\mapsto} % |-> +\def\barMinusMinusGreater{\longmapsto} % |--> +\def\barMinusMinusGreaterGreater{\mapsto\hspace*{-8pt}\to} + % |-->> +\def\barVeeBar{\Downarrow} % |v| +\def\barCircBar{\Uparrow} % |^| +\def\barGreater{\triangleright} % |> +\def\lessLess{[\![} % << +\def\lessLessLess{\left[\!\!\left[} % <<< +\def\greaterGreater{]\!]} % >> +\def\greaterGreaterGreater{\right]\!\!\right]} % >>> +\def\minusv#1{\using\text{\rulename{#1}}\justifies} % -----... +\def\twiddlei{\TWIDDLE} % ~ +\def\twiddleii{\;} % ~~ +\def\twiddleiii{\quad} % ~~~ +\def\twiddleiv{\endprooftree\qquad\prooftree} % ~~~~ +\def\twiddlev{\endprooftree\\ \\ \prooftree} % ~~~~~... +\def\twiddleTwiddleGreater{\rightsquigarrow} % ~~> +\def\asterisk{\ASTERISK} % * +\def\asteriskii{\overline{\ASTERISK}} % ** +\def\asteriskiii{\dagger} % *** +\def\asteriskiv{\star} % **** +\def\asteriskv{\ddagger} % ***** +\def\plusPlus{\mathbin{\PLUS\hspace*{-4pt}\PLUS}} % ++ +\def\bang{\mathalpha{\BANG}} % ! +\def\question{\mathalpha{\QUESTION}} % ? +\def\slashBackslash{\land} % /\ + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "modules" +%%% End: + addfile ./dependent-kinds.tex hunk ./dependent-kinds.tex 1 +\documentclass[nocopyrightspace,preprint,blockstyle]{sigplanconf} % Two-column style + +%% \documentclass[draft]{article} +%% \usepackage{hyperref} + +\usepackage{enumerate} +\usepackage{xspace} +\usepackage{denot} +\usepackage{prooftree} +\usepackage{afterpage} +\usepackage{float} +\usepackage{pstricks} +\usepackage{latexsym} +%% less space consuming enumerates and itemizes +\usepackage{mdwlist} +%% \usepackage{stmaryrd} +\usepackage{amsfonts} +\usepackage{amssymb} +%% \usepackage{amsthm} + +% local packages +\usepackage{code} +\usepackage{url} + +\newcommand{\text}[1]{\mbox{#1}} +\usepackage{color} + +\renewcommand{\phi}{\varphi} + +%% \theoremstyle{remark} +%% \newtheorem{example}{Example}[section] +%% \theoremstyle{definition} +%% \newtheorem{definition}{Definition}[section] +%% \theoremstyle{plain} +%% \newtheorem{theorem}{Theorem}[section] +%% \newtheorem{lemma}[theorem]{Lemma} +%% \newtheorem{proposition}[theorem]{Proposition} +%% \newtheorem{corollary}[theorem]{Corollary} + +\setlength{\parskip}{0.35\baselineskip plus 0.2\baselineskip minus 0.1\baselineskip} +\setlength{\parsep}{\parskip} +\setlength{\topsep}{0cm} +\setlength{\parindent}{0cm} + +% Figures should be boxed +% *** Uncomment the next two lines to box the floats *** +\floatstyle{boxed} +\restylefloat{figure} +% Keep footnotes on one page +\interfootnotelinepenalty=10000 + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% Indentation -- attention: works ok for ACM formatting +%% \setlength{\parskip}{0.5\baselineskip plus 0.2\baselineskip minus 0.1\baselineskip} +%% \setlength{\parsep}{\parskip} +%% \setlength{\topsep}{0cm} +%% \setlength{\parindent}{0cm} + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\input{abbrevmap} +\def\rulename#1{\textsc{#1}} +\def\ruleform#1{\fbox{$#1$}} +\def\ol#1{\overline{#1}} +\def\nb{\penalty10000 \ } +\def\fiddle#1{\hspace*{-0.5ex}\raisebox{0.4ex}{$\scriptscriptstyle#1$}} + + +\newcommand{\trans}[2]{[\![#1]\!]_{#2}} +% Box around a type +\def\tbox#1{\psframebox[framesep=1pt,linewidth=0.5pt]{#1}} + +\newcommand{\highlight}[1]{\colorbox{yellow}{\ensuremath{#1}}} + +\newcommand{\as}{\ol{a}} +\newcommand{\bs}{\ol{b}} +\newcommand{\cs}{\ol{c}} +\newcommand{\ds}{\ol{d}} +\newcommand{\es}{\ol{e}} +\newcommand{\fs}{\ol{f}} +\newcommand{\gs}{\ol{g}} +\newcommand{\xs}{\ol{x}} +\newcommand{\alphas}{\ol{\alpha}} +\newcommand{\betas}{\ol{\beta}} +\newcommand{\gammas}{\ol{\gamma}} +\newcommand{\deltas}{\ol{\delta}} +\newcommand{\epsilons}{\ol{\epsilon}} +\newcommand{\zetas}{\ol{\zeta}} +\newcommand{\etas}{\ol{\eta}} + +\newcommand{\kappas}{\ol{\kappa}} +\newcommand{\iotas}{\ol{\iota}} + +\newcommand{\taus}{\ol{\tau}} +\newcommand{\sigmas}{\ol{\sigma}} + +%% nasty interaction between denot.sty and abbrev.sty +\def\denot#1{[\![ #1 ]\!]} +\newcommand{\erase}[1]{{\cal E}\denot{#1}} +\newcommand{\typeof}[1]{{\cal T}\denot{#1}} + + +%% Typing relations +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\usepackage{xspace} +\usepackage{natbib} +\bibpunct();A{}, +\let\cite=\citep + +\renewcommand{\topfraction}{0.95} +\renewcommand{\textfraction}{0.02} +\renewcommand{\floatpagefraction}{0.8} + + +\newcommand{\authornote}[3]{\marginpar{\sc\color{#2} #1}\textbf{\textcolor{#2}{#3}}} +\newcommand\simon[1]{\authornote{simon}{red}{#1}} +\newcommand\dv[1]{\authornote{dv}{green}{#1}} +\newcommand\conor[1]{\authronote{conor}{blue}{#1}} + +\newcommand{\cokind}{\textsc{co}} % Kind of coercions +\newcommand{\tykind}{\textsc{ty}} % Kind of types +\newcommand{\kikind}{\textsc{knd}} + +\newcommand{\turnst}{\mathrel{\vdash_{\hspace{-3pt}\tiny \tykind}}} +\newcommand{\turnsc}[1]{\mathrel{\vdash_{\hspace{-3pt}\tiny \cokind}^{\hspace{-2pt}\tiny #1}}} +\newcommand{\turnsk}{\mathrel{\vdash_{\hspace{-3pt}\tiny \kikind}}} + + +\newcommand{\at}{@} + +\newcommand{\qt}[1]{\text{``}#1\text{''}} +\newcommand{\lift}[1]{\{#1\}} + +\authorinfo{}{}{} +\usepackage{abbrev} +\begin{document} + +\title{Dependent kinds for Haskell} +\subtitle{\color{red}\today} + +\maketitle +\makeatactive + + +\begin{abstract} +We explore the addition of a dependent kind (and type) system in Haskell. + \end{abstract} + +\section{Syntax} + +\begin{figure} +\[\begin{array}{l} + \begin{array}{lcll} + \multicolumn{4}{l}{\textbf{Kinds}} \\ + \kappa,\iota & ::= & \star \mid \kappa_1 \Rightarrow \kappa_2 \mid \lift{\tau} \mid \forall(a{:}\kappa_1).\kappa_2 & \\ \\ + \multicolumn{4}{l}{\textbf{Types}} \\ + \tau & ::= & a \mid @T@ \mid F_n\;\taus^n \mid \tau_1 \to \tau_2 \mid \forall(a{:}\kappa).\tau \\ + & \mid & \tau_1\at{\tau_2} \mid \lift{C} \mid \qt{\kappa} \mid \lift{x} + \end{array} +\end{array}\] +\caption{Syntax}\label{fig:syntax} +\end{figure} + +Our first goal is to add a proper kind system with kinds that depend on types. In +Figure~\ref{fig:syntax}, the form $\lift{\tau}$ achieves exactly that. For example, we +may declare a {\em datatype}: +\begin{code} + data Nat : * where + Z :: Nat + S :: Nat -> Nat +\end{code} +which immediately gives rise to a {\em datakind}, $\lift{@Nat@}$, a lifted +version of @Nat@ to the level of kinds (or a singleton kind), inhabited by the +type @Nat@. Hence, Figure~\ref{fig:syntax} allows such kinds, of the form +$\lift{\tau}$. Figure~\ref{fig:wf-kinds} gives the well-formedness relation on kinds. + +\begin{figure} +\[\begin{array}{c} +\ruleform{ \Gamma \turnsk \kappa } \\ \\ +\prooftree + ----------------{kstar} + \Gamma \turnsk \star + ~~~~ + \Gamma \turnsk \kappa_1 \quad \Gamma \turnsk \kappa_2 + ----------------------{karr} + \Gamma \turnsk \kappa_1 \Rightarrow \kappa_2 + ~~~~~ + \Gamma \turnst \tau : \star + ----------------------------{klift} + \Gamma \turnsk \lift{\tau} + ~~~~ + \Gamma,(a{:}\kappa_1) \turnsk \kappa_2 \quad \Gamma \turnsk \kappa_1 + -------------------------------{kall} + \Gamma \turnsk \forall(a{:}\kappa_1).\kappa_2 +\endprooftree +\end{array}\] +\caption{Well-formed kinds}\label{fig:wf-kinds} +\end{figure} + +Notice that the judgement $\Gamma \turnsk \kappa$ relies on the well-formedness relation +on types $\Gamma \turnst \tau : \kappa$, to be discussed next. + +The next question is what happens at the type level. Let us consider the case of data constructors. +Since @Nat@ can be lifted to the kind $\lift{@Nat@}$ we would expect that each of the constructors +could be lifted to {\em types}. For example @Z@ could be lifted to form the type +$\lift{@Z@}$, of kind $\lift{@Nat@}$. + +However, for @S@ the situation is more complex. For @S@, of type +$@Nat@ \to @Nat@$, we have (at least) two options for giving a kind to +the lifted constructor @S@: +\begin{itemize} + \item Give $\lift{@S@}$ the kind $\lift{@Nat@ \to @Nat@}$, or + \item Give $\lift{@S@}$ the kind $\lift{@Nat@} \Rightarrow \lift{@Nat@}$. +\end{itemize} +In other words, should we be ``pushing'' the lift operator under $\to$, translating +it to $\Rightarrow$ or not? It certainly is more expressive to allow the pushing but maybe +the complexity is not worth it. + +Concretely, we have examined the following options: +\begin{enumerate} + \item Do no pushing of the ``lift'' operation on types at all. But, in order to + maintain some reasonable expressivity we will instead extend the syntax of + liftable expressions from data constructors and variables ($C$ and $x$ respectively + in Figure~\ref{fig:syntax} to a bigger set of expressions consisting of applications + of data constructors and variables $c$, below: + \[\begin{array}{lcl} + c & ::= & C \mid x \mid c\;c \mid c\;[\tau] \mid a + \end{array}\] + We include type variables $a$ in that set of expression if they are of kind $\lift{\tau}$. + \dv{we need an example here} + Hence, the type $\lift{@S@}\;\lift{@Z@}$ is not well-formed, but this application + can be recovered by the expression $\lift{@S Z@}$. Hence the typing relation for that + limited set of expressions would be: + \[\begin{array}{c}\prooftree + \Gamma \vdash_c c : \tau + --------------{ty} + \Gamma \turnst \lift{c} : \lift{\tau} + ~~~~ + (a{:}\lift{\tau}) \in \Gamma + --------------------{var} + \Gamma \vdash_c a : \tau + ~~~~~ + (C{:}\tau) \in \Gamma + ---------------------{con} + \Gamma \vdash_c C : \tau + ~~~~ + \Gamma \vdash_c c_1 : \tau_1 \to \tau_2 \quad \Gamma \vdash_c c_2 :\tau_1 + ------------------------{tapp} + \Gamma \vdash_c c_1\;c_2 : \tau_2 + ~~~~~ + \Gamma \vdash_c c : \forall(a{:}\kappa_1).\kappa_2 \quad \Gamma \vdash_c \tau : \kappa_1 + ------------------------{tapp} + \Gamma \vdash_c c\;[\tau] : \kappa_2\{\tau/a\} + \endprooftree\end{array}\] + One problem with this approach is that lifting for variables that abstract singleton + kinds seems redundant. For example we have: + \[ (a{:}\lift{\tau}) \turnst a : \lift{\tau} \] + but we also have: + \[ (a{:}\lift{\tau}) \turnst \lift{a} : \lift{\tau} \] + A question arises: do we consider $\lift{a}$ and $a$ equivalent, or not? + If yes, this approach does not have the simplicity that we were initally attracted by; if + not, then programs may fail unexpectedly (e.g. if a function expects a $\lift{a}$ and one + passes it a $a$ argument). + \item Allowing lifting over arrows, as a function $lift$ which is partially evaluated -- evaluation + stops when you reach an abstract type variabe. Hence, the rule would be: + \[\begin{array}{c}\prooftree + (C{:}\tau) \in \Gamma \quad lift(\tau) ~~> \kappa + ------------------------{liftcon} + \Gamma \vdash \lift{C} : \kappa + \endprooftree\end{array}\] + One problem with this approach is that the resulting system is not stable under substitutions. If + a function $f$ has type $a \to @Nat@ \to a$ then lifting its type would give + $\lift{a} \Rightarrow \lift{@Nat@} \Rightarrow \lift{a}$. However when $a$ was going to be substituted away for, e.g. + $@Nat@ \to @Nat@$ then we would not be able to expose the kind + \[(\lift{@Nat@} \Rightarrow \lift{@Nat@}) \Rightarrow \lift{@Nat@} \Rightarrow \lift{@Nat@} \Rightarrow \lift{@Nat@} \] + for it. Hence, we arrive at the third option, which is: + \item Allow lifting over arrows via a partially evaluated function {\em and} make substitution + push the lifting braces down the structure of the type. Both could be achieved with a single function $push$ + that pushes the braces in the types down arrows, as much as possible. + For example, the rule for eliminating types with polymorphic kinds would be: + \[\begin{array}{c}\prooftree + \Gamma \turnst \tau_1 : \forall(a{:}\kappa_1).\kappa_2 \quad \Gamma \turnst \tau_2 : \kappa_1 + --------------------------------------------------{eall} + \Gamma \turnst \tau_1\at{\tau_2} : push(\kappa_2\{\tau_2/a\}) + \endprooftree\end{array}\] + The rule for lifting a constructor would be: + \[\begin{array}{c}\prooftree + (C{:}\sigma) \in \Gamma + ----------------------------------------------{lcon} + \Gamma \turnst \lift{C} : push(\lift{\sigma}) + \endprooftree\end{array}\] + \dv{This is very reminiscent of the ``boxy substitution'' formalization we used in the FPH paper. But there + the pushing was formed as a subsumption rule not as a function eagerly applied} +\end{enumerate} + +\section{Lifting types, lowering kinds} + +Suppose that we wish to write the following version of the equality GADT: +\begin{code} + data Eq :: forall a b. {a} => {b} => * where + Refl :: forall (a:*) (b:{a}). Eq b b +\end{code} +The kind of @Eq@ says that it may accept a value of a datakind and another +datakind and will ensure that the two are the same. This can be used to encode +term-level equalities: +\begin{code} + Refl @ Nat @ {Z} : Eq {Z} {Z} +\end{code} +But we may wish to use it to encode {\em type-level} equalities as well! We +would like to say something like: +\begin{code} + Refl@ ?a @ Nat : Eq Nat Nat +\end{code} +But now the problem is {\em what do we plug in for} the instantatiation @?a@? +Intuitively we need something such that @Nat : {?a}@ and hence it would have +to be an operator on kinds that cancels-out with lifting. We introduce that operator +and we call it quote: +\[\begin{array}{c}\prooftree + \Gamma \turnsk \kappa + -------------------------{qt} + \Gamma \turnst \qt{\kappa} : \star +\endprooftree\end{array}\] +with the equality that: +\[ \lift{\qt{\kappa}} \equiv \kappa \] +In effect we created an uninhabited type, which is just a name for a particular kind. +We may now write: +\begin{code} + Refl@ ``*'' @ Nat : Eq Nat Nat + Refl@ ``*->*'' @ Maybe : Eq Maybe Maybe +\end{code} + +Such quoted kinds can be generally useful for representing +heterogeneous data structures. In Figure~\ref{fig:hrec} we give a more +substantial example of such a data structure. + +\begin{figure*}[ht] +\begin{code} + data Rec :: {[(String,``*'')]} => * where + RNil :: Rec {[]} + RCons :: forall (a :: *) + (ns :: {[(String,``*'')]} + (s :: String). a -> Rec ns -> Rec { ({:}@(String,``*'')) ({()} s a) ns } + -- just Rec {(s,a):ns} really, but well-typed +\end{code} +\caption{Heterogeneous records with fixed labels}\label{fig:hrec} +\end{figure*} + +The example in Figure~\ref{fig:hrec} also demonstrates that we probably need better syntax, or syntactic +sugar, or some form of type abbreviations. + + +\clearpage +\section{Type inference and unification} + +We do not expect any serious problems here --- we simply have to be careful that we +decompose the typing equality problems enough so that we do not forget about the constraints arising +from the corresponding kind equality problems. + + + + + + +%% \makebibliography{./local-bib-one,./local-bib-two} +\end{document}