%the team.
\newcommand{\unif}{{\scriptscriptstyle\cup}}
+ %\subsubsection{Anonymous functions}
+ %When the programmers wants to use small functions that consist of one line to
+ %for example use the operators in a functional way the programmer has to make a
+ %named function for every operator. In some cases it is easy to do this inline
+ %using anonymous functions. A small syntactic sugar has been added that will
+ %inline anonymous functions to non-anonymous functions during the parsing phase.
+ %The following snippet is an example of a filter on even values before and after
+ %transformation.
+ %
+ %\begin{SPLCode}
+ %//Before transformation
+ %main(){
+ % var a = filter(\x->x % 2 == 0, 1 : 2 : 3 : 4 : 5 : []);
+ %}
+ %
+ %//After transformation
+ %1lambda_23(x){
+ % return x % 2 == 0;
+ %}
+ %
+ %main(){
+ % var a = filter(1lambda_23, 1 : 2 : 3 : 4 : 5 : []);
+ %}
+ %\end{SPLCode}
+
+ Every anonymous functions gets a unique name outside the namespace of legal
+ names for functions making sure the name is unique. By implementing the
+ transformation in the parsing phase the function is automatically checked
+ or inferred on type.
The semantic analysis phase asses if a -grammatically correct- program is also
semantically correct and decorates the program with extra information it
\item That no functions are declared with the same name
\item That \tt{main} is of type \tt{(-> Void)}
\item That the program includes a main function
+ \item AST transformation for lambdas
\item That the program is correctly typed
\end{enumerate}
The first three steps are simple sanity checks which are coded in slightly over
-two dozen lines of Clean code. The last step is a Hindley Milner type inference
+two dozen lines of \Clean{} code. The last step is a Hindley-Milner type
+inference
algorithm, which is a magnitude more complex. This last step also decorates the
\AST{} with inferred type information.
-\subsection{Sanity checks}
-The sanity checks are defined as simple recursive functions over the function
-declarations in the \AST. We will very shortly describe them here.
-
-\begin{description}
- \item [No duplicate functions] This function checks that the program does
- not contain top level functions sharing the same name. Formally:
- $ \forall f \in \textrm{functions} \ldotp \neg
- \exists g \in \textrm{functions} \setminus \{f\} \ldotp
- f.\textrm{name} = g.\textrm{name}$
- \item [\tt{main} should have type \tt{->Void}] Our semantics of \SPL{}
- require the main function to take no arguments and to not return a
- value. Formally: $\forall f \in \textrm{functions} \ldotp
- f.\textrm{name} = \textrm{'main'} \Rightarrow
- \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}
+\subsection{AST transformation for lambdas}
+
+% \subsection{Sanity checks}
+% The sanity checks are defined as simple recursive functions over the function
+% declarations in the \AST. We will very shortly describe them here.
+
+% \begin{description}
+% \item [No duplicate functions] This function checks that the program does
+% not contain top level functions sharing the same name. Formally:
+% $ \forall f \in \textrm{functions} \ldotp \neg
+% \exists g \in \textrm{functions} \setminus \{f\} \ldotp
+% f.\textrm{name} = g.\textrm{name}$
+% \item [\tt{main} should have type \tt{->Void}] Our semantics of \SPL{}
+% require the main function to take no arguments and to not return a
+% value. Formally: $\forall f \in \textrm{functions} \ldotp
+% f.\textrm{name} = \textrm{'main'} \Rightarrow
+% \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}
\subsection{Type inference}
\SPLC{} features a Hindley-Milner type inference algorithm based on the
\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
+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.
\begin{lstlisting}[
label={lst:types},
caption={SPLC types},
- language=clean]
+ language=Clean]
:: Type
= TupleType (Type, Type) -- (t1, t2)
| ListType type -- [t]
| CharType
| VoidType
| FuncType Type -- (-> t)
- | (->>) infixl 7 Type Type -- (t1 -> t2)
+ | (\->>) infixl 7 Type Type -- (t1 -> t2)
\end{lstlisting}
\subsubsection{Environment}
Void otherwise.
In the Clean implementation the new Gamma in the result of an inference is
-hidden in the Typing Monad.
+carried through the Typing Monad.
Below we will show the inference rules for expressions and statements. In these
lowercase Greek letters are always fresh type variables.
+Section~\ref{sec:infRules} shows all typing inference rules. Below we will show
+a few to express the basics and show some interesting cases.
+
\paragraph{Op2 expressions}
Equation~\ref{eq:inferOp2} shows the inference rule for op2 expressions.
\textit{op2type} is a function which takes an operator and returns the
(\Gamma^\star, \star, \tau, \underline{\textrm{return }} e')
}
{\Gamma \vdash e \Rightarrow (\Gamma^\star, \star, \tau, e')}
- \end{equation}
+ \end{equation}
repositories / cc1516.git / commitdiff