elvis/lci
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Clarification

Browse Source
This commit is contained in:
elvis
2025-02-04 16:15:52 +01:00
parent ab469ffa39
commit e70c252184
2 changed files with 3 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
report/report.tex
View File

@ -429,8 +429,8 @@ output := y;
\begin{section}{Addendum: Algorithm W}
Added since the last submission a simplified version of the Algorithm W from {\bf A Theory of Type Polymorphism in Programming}\cite{MILNER}. The implementation uses levels instead of prefexes and does not contain the fixed point as described in {\bf Extension of ML type system with a sorted equation theory on types}\cite{REMY} and \href{https://okmij.org/ftp/ML/generalization.html}{okmij.org/ftp/ML/generalization.html}. Thus \texttt{let rec} is not implemented. But the remaining grammar is fully polimorphically typable.
An interpreter that outputs the type of the input program is provided as \href{../bin/miniFunPolyInterpreter.ml}{miniFunPolyInterpreter.ml}. The interpreter admits program that are not functions from integers to integers like with the other interpreter, so the evaluation of the program with input is disabled by default. Otherwise the only possible types of programs would be \(\texttt{Int} \to \texttt{Int}\), \(\forall \texttt{a}, \texttt{a} \to \texttt{Int}\) and \(\forall \texttt{a}, \texttt{a} \to \texttt{a}\) since they can be all unified to \(\texttt{Int} \to \texttt{Int}\).
Added since the last submission a simplified version of the Algorithm W from {\bf A Theory of Type Polymorphism in Programming}\cite{MILNER} for the miniFun language. The implementation uses levels instead of prefixes as described in {\bf Extension of ML type system with a sorted equation theory on types}\cite{REMY} and \href{https://okmij.org/ftp/ML/generalization.html}{okmij.org/ftp/ML/generalization.html}, but does not contain a fixed point operator. Meaning \texttt{let rec} is not implemented. But the remaining grammar is fully polimorphically typable.
An interpreter that outputs the type of the input program is provided as \href{../bin/miniFunPolyInterpreter.ml}{miniFunPolyInterpreter.ml}. The interpreter admits program that are not functions from integers to integers like with the other interpreter, so the evaluation of the program with input is disabled by default. Otherwise the only possible types of programs would be \(\texttt{Int} \to \texttt{Int}\), \(\forall \texttt{a}, \texttt{a} \to \texttt{Int}\) and \(\forall \texttt{a}, \texttt{a} \to \texttt{a}\) since they can be all unified with \(\texttt{Int} \to \texttt{Int}\).
In addition the character \texttt{?} is mapped to the new type \texttt{Unknown}. The new type is not used by the program and any type specification is ignored. The \texttt{?} symbol is just a useful shorthand.
@ -458,6 +458,7 @@ f (\x: ? => \y: ? => \z: ? => if fst y then snd y else snd z)
is correctly evaluated as having the type \( \forall \texttt{a}\ \texttt{b}, (\texttt{Int} \to (\texttt{Bool}, \texttt{a}) \to (\texttt{b}, \texttt{a}) \to \texttt{a}) \to \texttt{Int} \to (\texttt{Bool}, \texttt{a}) \to (\texttt{b}, \texttt{a}) \to \texttt{a} \).
\end{section}
%%% Local Variables:
%%% TeX-command-extra-options: "-shell-escape"
%%% TeX-master: "document.tex"