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

Fixes

Browse Source
This commit is contained in:
elvis
2025-02-02 20:46:55 +01:00
parent fec0142103
commit ab469ffa39
11 changed files with 79 additions and 13 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
bin/miniFunPolyInterpreter.ml
View File

@ -75,7 +75,7 @@ let () =
| Ok ty -> ty
| Error (`AbsentAssignment msg)
| Error (`WrongTypeSpecification msg)
| Error (`RecusrionsNotImplemented msg)
| Error (`RecursionNotImplemented msg)
| Error (`WrongType msg) ->
Printf.fprintf stderr "%s\n" msg;
exit (-1)

1
lib/miniFun/Lexer.mll
View File

@ -56,6 +56,7 @@ rule read = parse
| "+" {PLUS}
| "," {COMMA}
| "-" {MINUS}
| "?" {QUESTIONMARK}
| "->" {TYPEFUNCTION}
| "/" {DIVISION}
| ":" {COLUMN}

3
lib/miniFun/Parser.mly
View File

@ -13,7 +13,7 @@
%token <int> INT
%token COMMA COLUMN LEFTPAR RIGHTPAR CMPLESS CMPGREATER PLUS MINUS TIMES
%token DIVISION MODULO POWER ASSIGNMENT BAND BOR CMP CMPLESSEQ CMPGREATEREQ
%token FIRST SECOND
%token FIRST SECOND QUESTIONMARK
%token EOF
%type <t_exp> prg
@ -90,6 +90,7 @@ texp:
typeexp:
| TYPEINT {IntegerType}
| TYPEBOOL {BooleanType}
| QUESTIONMARK {UnknownType}
| v = delimited(LEFTPAR, typeexp, RIGHTPAR)
{v}
| a = typeexp; COMMA; b = typeexp {TupleType (a, b)}

12
lib/miniFun/TypeChecker.ml
View File

@ -35,13 +35,13 @@ let rec unify type_a type_b =
unify a1 b1
| VariableTypeP ({contents = Link ty_link}), ty_rest
| ty_rest, VariableTypeP ({contents = Link ty_link})
when ty_link = ty_rest ->
Ok ()
| ty_rest, VariableTypeP ({contents = Link ty_link}) ->
unify ty_rest ty_link
| VariableTypeP ({contents = Unbound (a1, _)}),
VariableTypeP ({contents = Unbound (b1, _)})
when a1 = b1 ->
(* should never happen *)
Error (`WrongType "Only a single instance of a type should be available.")
| type_ab, VariableTypeP ({contents = Unbound (_id, _level)} as tvar)
@ -252,7 +252,7 @@ let rec evaluate_type_polimorphic program (env: env) level =
let generalized_ty = generalize level var_ty in
evaluate_type_polimorphic rest (VariableMap.add x generalized_ty env) level
| LetFun (f, xs, _typef, fbody, rest) ->
let* _ = Error (`RecusrionsNotImplemented "Let Rec is not implemented.") in
let* _ = Error (`RecursionNotImplemented "Let Rec is not implemented.") in
let tmp_type_f = VariableTypeP (ref (Unbound (new_global_id (), level))) in
let new_env = VariableMap.add f tmp_type_f env in
let param_type = VariableTypeP (ref (Unbound (new_global_id (), level))) in
@ -421,7 +421,7 @@ let typecheck (program: t_exp) : (ftype, [> typechecking_error]) result =
let typecheck_polymorphic (program: t_exp)
: (type_f, [> typechecking_error]) result =
: (type_f, [> polytypechecking_error]) result =
global_type_id := 0;
let* type_program = evaluate_type_polimorphic program VariableMap.empty 0 in
let* _ = unifyable type_program (FunctionTypeP (IntegerTypeP, IntegerTypeP))
@ -430,7 +430,7 @@ let typecheck_polymorphic (program: t_exp)
Ok (generalized_ty)
let typecheck_polymorphic_unbound (program: t_exp)
: (type_f, [> typechecking_error]) result =
: (type_f, [> polytypechecking_error]) result =
global_type_id := 0;
let* type_program = evaluate_type_polimorphic program VariableMap.empty 0 in
let generalized_ty = generalize (-1) type_program in

4
lib/miniFun/TypeChecker.mli
View File

@ -1,5 +1,5 @@
val typecheck : Types.t_exp -> (Types.ftype, [> Types.typechecking_error]) result
val typecheck_polymorphic : Types.t_exp -> (Types.type_f, [> Types.typechecking_error]) result
val typecheck_polymorphic : Types.t_exp -> (Types.type_f, [> Types.polytypechecking_error]) result
val typecheck_polymorphic_unbound : Types.t_exp -> (Types.type_f, [> Types.typechecking_error]) result
val typecheck_polymorphic_unbound : Types.t_exp -> (Types.type_f, [> Types.polytypechecking_error]) result

8
lib/miniFun/Types.ml
View File

@ -76,6 +76,7 @@ let pp_type_f (ty: type_f) : string =
type ftype = (* type used for specification *)
IntegerType
| BooleanType
| UnknownType
| TupleType of ftype * ftype
| FunctionType of ftype * ftype
@ -134,9 +135,14 @@ type base_error = [
type typechecking_error = [
| base_error
| `WrongTypeSpecification of string
| `RecusrionsNotImplemented of string
]
type polytypechecking_error = [
| typechecking_error
| `RecursionNotImplemented of string
]
type error = [
| base_error
| `DivisionByZero of string

7
lib/miniFun/Types.mli
View File

@ -34,6 +34,7 @@ val pp_type_f : type_f -> string
type ftype = (* type used for specification *)
IntegerType
| BooleanType
| UnknownType
| TupleType of ftype * ftype
| FunctionType of ftype * ftype
@ -92,7 +93,11 @@ type base_error = [
type typechecking_error = [
| base_error
| `WrongTypeSpecification of string
| `RecusrionsNotImplemented of string
]
type polytypechecking_error = [
| typechecking_error
| `RecursionNotImplemented of string
]
type error = [

19
report/document.bib
View File

@ -0,0 +1,19 @@
@article{MILNER,
title = {A theory of type polymorphism in programming},
journal = {Journal of Computer and System Sciences},
volume = {17},
number = {3},
pages = {348-375},
year = {1978},
issn = {0022-0000},
doi = {https://doi.org/10.1016/0022-0000(78)90014-4},
url = {www.sciencedirect.com/science/article/pii/0022000078900144},
author = {Robin Milner},
}
@inproceedings{REMY,
title={Extension of ML type system with a sorted equation theory on types},
author={Didier R{\'e}my},
year={1992},
url={https://api.semanticscholar.org/CorpusID:117549268}
}

BIN
report/document.pdf
View File

Binary file not shown.

4
report/document.tex
View File

@ -153,7 +153,7 @@
\newcommand{\defeq}{\vcentcolon=}
\lstdefinelanguage{miniimp}{
keywords={if, then, else, skip, while, do, for, rand},
keywords={if, then, else, skip, while, do, for, rand, let},
keywordstyle=\color{blue}\bfseries,
identifierstyle=\color{black},
sensitive=false,
@ -202,6 +202,8 @@
\input{report}
\printbibliography{}
\end{document}
%% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - %%

32
report/report.tex
View File

@ -426,6 +426,38 @@ output := y;
To see a list of all options run \texttt{dune exec <interpreter> {-}{-} -h}. A binary version of the executables can also be found in the build directory: \href{./_build/default/bin/}{./\_build/default/bin/}.
\end{section}
\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}\).
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.
Some examples:
\begin{lstlisting}
let f =
\z: ? =>
\y: ? =>
\x: ? =>
if x < 0 then y x else z x
in f
\end{lstlisting}
is correctly evaluated as having the type \( \forall \texttt{a}, (\texttt{Int} \to \texttt{a}) \to (\texttt{Int} \to \texttt{a}) \to \texttt{Int} \to \texttt{a} \).
\begin{lstlisting}
let f =
\z: ? =>
\y: ? =>
\x: ? =>
if x < 0 then y x else z x
in
f (\x: ? => \y: ? => \z: ? => if fst y then snd y else snd z)
\end{lstlisting}
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"