intro comment

This commit is contained in:
JanUlrich 2024-02-14 15:44:46 +01:00
parent 4a0c6e5e02
commit b87fa9a048

View File

@ -172,6 +172,33 @@ m(l) {
$\tv{l} \lessdotCC \exptype{List}{\wtv{x}}, \tv{l} \lessdotCC \wtv{x}$
% One possible solution:
% \begin{verbatim}
% List<Object> m(List<Object> l) {
% return l.add(l);
% }
% \end{verbatim}
% No capture conversion for methods in the same class:
% \begin{verbatim}
% m() = new List<String>() :? new List<Integer>();
% id(a) = a
% id(m())
% \end{verbatim}
% id will get type List<?> -> List<?>
% % explain polymorphic recursion here
% % no capture conversion needed
% The id method is pre typed:
% \begin{verbatim}
% <A> List<A> id(List<A> a) = a
% m() = new List<String>() :? new List<Integer>() :? id(m());
% \end{verbatim}
% constraint m :: p -> r
% % Wildcards are only deleted in unify, never generated.
\subsection{Java Wildcards}
Wildcards are expressed by a \texttt{?} in Java and can be used as parameter types.
Wildcards can be formalized as existential types \cite{WildFJ}.