--- /dev/null
+% proof.sty (Proof Figure Macros)
+%
+% version 3.1 (for both LaTeX 2.09 and LaTeX 2e)
+% Nov 24, 2005
+% Copyright (C) 1990 -- 2005, Makoto Tatsuta (tatsuta@nii.ac.jp)
+%
+% This program is free software; you can redistribute it or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation; either versions 1, or (at your option)
+% any later version.
+%
+% This program is distributed in the hope that it will be useful
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+% GNU General Public License for more details.
+%
+% Usage:
+% In \documentstyle, specify an optional style `proof', say,
+% \documentstyle[proof]{article}.
+%
+% The following macros are available:
+%
+% In all the following macros, all the arguments such as
+% <Lowers> and <Uppers> are processed in math mode.
+%
+% \infer<Lower><Uppers>
+% draws an inference.
+%
+% Use & in <Uppers> to delimit upper formulae.
+% <Uppers> consists more than 0 formulae.
+%
+% \infer returns \hbox{ ... } or \vbox{ ... } and
+% sets \@LeftOffset and \@RightOffset globally.
+%
+% \infer[<Label>]<Lower><Uppers>
+% draws an inference labeled with <Label>.
+%
+% \infer*<Lower><Uppers>
+% draws a many step deduction.
+%
+% \infer*[<Label>]<Lower><Uppers>
+% draws a many step deduction labeled with <Label>.
+%
+% \infer=<Lower><Uppers>
+% draws a double-ruled deduction.
+%
+% \infer=[<Label>]<Lower><Uppers>
+% draws a double-ruled deduction labeled with <Label>.
+%
+% \deduce<Lower><Uppers>
+% draws an inference without a rule.
+%
+% \deduce[<Proof>]<Lower><Uppers>
+% draws a many step deduction with a proof name.
+%
+% Example:
+% If you want to write
+% B C
+% -----
+% A D
+% ----------
+% E
+% use
+% \infer{E}{
+% A
+% &
+% \infer{D}{B & C}
+% }
+%
+
+% Style Parameters
+
+\newdimen\inferLineSkip \inferLineSkip=2pt
+\newdimen\inferLabelSkip \inferLabelSkip=5pt
+\def\inferTabSkip{\quad}
+
+% Variables
+
+\newdimen\@LeftOffset % global
+\newdimen\@RightOffset % global
+\newdimen\@SavedLeftOffset % safe from users
+
+\newdimen\UpperWidth
+\newdimen\LowerWidth
+\newdimen\LowerHeight
+\newdimen\UpperLeftOffset
+\newdimen\UpperRightOffset
+\newdimen\UpperCenter
+\newdimen\LowerCenter
+\newdimen\UpperAdjust
+\newdimen\RuleAdjust
+\newdimen\LowerAdjust
+\newdimen\RuleWidth
+\newdimen\HLabelAdjust
+\newdimen\VLabelAdjust
+\newdimen\WidthAdjust
+
+\newbox\@UpperPart
+\newbox\@LowerPart
+\newbox\@LabelPart
+\newbox\ResultBox
+
+% Flags
+
+\newif\if@inferRule % whether \@infer draws a rule.
+\newif\if@DoubleRule % whether \@infer draws doulbe rules.
+\newif\if@ReturnLeftOffset % whether \@infer returns \@LeftOffset.
+
+% Special Fonts
+
+\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
+ \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
+
+% Macros
+
+% Renaming @ifnextchar and @ifnch of LaTeX2e to @IFnextchar and @IFnch.
+
+\def\@IFnextchar#1#2#3{%
+ \let\reserved@e=#1\def\reserved@a{#2}\def\reserved@b{#3}\futurelet
+ \reserved@c\@IFnch}
+\def\@IFnch{\ifx \reserved@c \@sptoken \let\reserved@d\@xifnch
+ \else \ifx \reserved@c \reserved@e\let\reserved@d\reserved@a\else
+ \let\reserved@d\reserved@b\fi
+ \fi \reserved@d}
+
+\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
+ \ifx \@tempa \@tempb #2\else #3\fi }
+
+\def\infer{\@IFnextchar *{\@inferSteps}{\relax
+ \@IFnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
+
+\def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse
+ \@IFnextchar [{\@infer}{\@infer[\@empty]}}
+
+\def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue
+ \@IFnextchar [{\@infer}{\@infer[\@empty]}}
+
+\def\@inferSteps*{\@IFnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
+
+\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
+
+\def\deduce{\@IFnextchar [{\@deduce{\@empty}}
+ {\@inferRulefalse \@infer[\@empty]}}
+
+% \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
+
+\def\@deduce#1[#2]#3#4{\@inferRulefalse
+ \@infer[\@empty]{#3}{\@infer[{#1}]{#2}{#4}}}
+
+% \@infer[<Label>]<Lower><Uppers>
+% If \@inferRuletrue, it draws a rule and <Label> is right to
+% a rule. In this case, if \@DoubleRuletrue, it draws
+% double rules.
+%
+% Otherwise, draws no rule and <Label> is right to <Lower>.
+
+\def\@infer[#1]#2#3{\relax
+% Get parameters
+ \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
+ \setbox\@LabelPart=\hbox{$#1$}\relax
+ \setbox\@LowerPart=\hbox{$#2$}\relax
+%
+ \global\@LeftOffset=0pt
+ \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
+ \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
+ \inferTabSkip
+ \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
+ #3\cr}}\relax
+ \UpperLeftOffset=\@LeftOffset
+ \UpperRightOffset=\@RightOffset
+% Calculate Adjustments
+ \LowerWidth=\wd\@LowerPart
+ \LowerHeight=\ht\@LowerPart
+ \LowerCenter=0.5\LowerWidth
+%
+ \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
+ \advance\UpperWidth by -\UpperRightOffset
+ \UpperCenter=\UpperLeftOffset
+ \advance\UpperCenter by 0.5\UpperWidth
+%
+ \ifdim \UpperWidth > \LowerWidth
+ % \UpperCenter > \LowerCenter
+ \UpperAdjust=0pt
+ \RuleAdjust=\UpperLeftOffset
+ \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
+ \RuleWidth=\UpperWidth
+ \global\@LeftOffset=\LowerAdjust
+%
+ \else % \UpperWidth <= \LowerWidth
+ \ifdim \UpperCenter > \LowerCenter
+%
+ \UpperAdjust=0pt
+ \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
+ \LowerAdjust=\RuleAdjust
+ \RuleWidth=\LowerWidth
+ \global\@LeftOffset=\LowerAdjust
+%
+ \else % \UpperWidth <= \LowerWidth
+ % \UpperCenter <= \LowerCenter
+%
+ \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
+ \RuleAdjust=0pt
+ \LowerAdjust=0pt
+ \RuleWidth=\LowerWidth
+ \global\@LeftOffset=0pt
+%
+ \fi\fi
+% Make a box
+ \if@inferRule
+%
+ \setbox\ResultBox=\vbox{
+ \moveright \UpperAdjust \box\@UpperPart
+ \nointerlineskip \kern\inferLineSkip
+ \if@DoubleRule
+ \moveright \RuleAdjust \vbox{\hrule width\RuleWidth
+ \kern 1pt\hrule width\RuleWidth}\relax
+ \else
+ \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
+ \fi
+ \nointerlineskip \kern\inferLineSkip
+ \moveright \LowerAdjust \box\@LowerPart }\relax
+%
+ \@ifEmpty{#1}{}{\relax
+%
+ \HLabelAdjust=\wd\ResultBox \advance\HLabelAdjust by -\RuleAdjust
+ \advance\HLabelAdjust by -\RuleWidth
+ \WidthAdjust=\HLabelAdjust
+ \advance\WidthAdjust by -\inferLabelSkip
+ \advance\WidthAdjust by -\wd\@LabelPart
+ \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
+%
+ \VLabelAdjust=\dp\@LabelPart
+ \advance\VLabelAdjust by -\ht\@LabelPart
+ \VLabelAdjust=0.5\VLabelAdjust \advance\VLabelAdjust by \LowerHeight
+ \advance\VLabelAdjust by \inferLineSkip
+%
+ \setbox\ResultBox=\hbox{\box\ResultBox
+ \kern -\HLabelAdjust \kern\inferLabelSkip
+ \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
+%
+ }\relax % end @ifEmpty
+%
+ \else % \@inferRulefalse
+%
+ \setbox\ResultBox=\vbox{
+ \moveright \UpperAdjust \box\@UpperPart
+ \nointerlineskip \kern\inferLineSkip
+ \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
+ \@ifEmpty{#1}{}{\relax
+ \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
+ \fi
+%
+ \global\@RightOffset=\wd\ResultBox
+ \global\advance\@RightOffset by -\@LeftOffset
+ \global\advance\@RightOffset by -\LowerWidth
+ \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
+%
+ \box\ResultBox
+}
\ No newline at end of file
\AST/ plus the environment in which it was typed (for debug purposes), or it is
an error describing the problem with the \AST/.
-During this analysis \SPLC checks four properties of the program:
+During this analysis \SPLC{} checks four properties of the program:
\begin{enumerate}
\item That no functions are declared with the same name
\item That \tt{main} is of type \tt{(-> Void)}
\textit{typeof}\textrm{(main)} = \rightarrow\textrm{Void} $
\item [The program should have a main function] $\exists f \in
\textrm{functions} \ldotp f.\textrm{name} = \textrm{'main'}$
-\end{description}
\ No newline at end of file
+\end{description}
+
+\subsection{Type inference}
+\SPLC{} features a Hindley-Milner type inference algorithm based on the
+algorithm presented in the slides. It supports full polymorphism and can
+infer omitted types. It does not support multiple recursion and all
+functions and identifiers need to be declared before they can be used. In
+essence the program is typed as nested \tt{let .. in ..} statements.
+
+\subsubsection{Types}
+Listing~\ref{lst:types} shows the ADT representing types in \SPLC{}. Most of
+these are self explanatory, however typing of functions requires some special
+attention. \SPLC{}s extension is Higher order functions, this is described
+in more detail in Section~\ref{sec:ext}. These require a change to the
+type system, which we will already describe here.
+
+Higher order functions require that the type system can distinguish if an
+expression represents a type $a$ or a functions which takes no input and returns
+a value of type $a$ (we write: $\rightarrow a$). The latter is represented by
+the \CI{FuncType}.
+
+Another important difference with standard \SPL{} is that \SPLC{} supports
+currying of functions, functions are not typed with a list of argument types
+and a return type, but with just a single argument and return type. This return
+type then in itself can be a function.
+
+\begin{lstlisting}[
+ label={lst:types},
+ caption={SPLC types},
+ language=clean]
+:: Type
+ = TupleType (Type, Type) -- (t1, t2)
+ | ListType type -- [t]
+ | IdType TVar -- polymorphic type
+ | IntType
+ | BoolType
+ | CharType
+ | VoidType
+ | FuncType Type -- (-> t)
+ | (->>) infixl 7 Type Type -- (t1 -> t2)
+\end{lstlisting}
+
+\subsubsection{Environment}
+As all stages of \SPLC{}, the type inference is programmed in Clean. It takes an
+AST and produces either a fully typed AST, or an error if the provided AST
+contains type errors. The Program is typed in an environment $\Gamma : id
+\rightarrow \tau$ which maps identifiers of functions or variables to types.
+
+In Clean the type inference functions run in the \tt{Typing} monad, which is
+defined as \CI{Typing a :== StateT (Gamma, [TVar]) (Either SemError) a}. The
+carried list of \tt{TVar} is an infinite list of fresh \tt{TVars}, which are
+just an alias of \tt{String}.
+
+\subsubsection{Substitution and Unification}
+In \SPLC{} substitutions are defined as map from type variables to concrete
+types. Composing of substitutions is then simply taking the union of two
+substitutions and substituting the first substitution over the types in the
+second substitution.
+
+Unification ($\cup$) takes two types and either provides a substitution which
+could
+unify them, or an error of the types are not unifiable. The interesting case
+of unification is when trying to unify an type variable with a more
+specialised type. Equation~\ref{eq:unifyId} shows this. All other cases
+are trivially promoting unification to the contained types, or checking directly
+if the types to be unified are equal.
+
+\begin{equation} \label{eq:unifyId}
+ \infer{tv \cup \tau \Rightarrow [tv \mapsto \tau]}
+ {tv \notin ftv(\tau)}
+\end{equation}
\ No newline at end of file
repositories / cc1516.git / commitdiff