From 813b256e4d68a08f01ff85c27f2c385a96b9f335 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Sat, 10 Feb 2024 08:19:24 +0100 Subject: [PATCH] Intro to type rules --- constraints.tex | 2 +- tRules.tex | 29 ++++++++++++++++++----------- 2 files changed, 19 insertions(+), 12 deletions(-) diff --git a/constraints.tex b/constraints.tex index 60c0508..70bed1e 100644 --- a/constraints.tex +++ b/constraints.tex @@ -1,4 +1,4 @@ -\section{Constraint generation} +\section{Constraint generation}\label{chapter:constraintGeneration} % Our type inference algorithm is split into two parts. % A constraint generation step \textbf{TYPE} and a \unify{} step. diff --git a/tRules.tex b/tRules.tex index df9658c..84e3b99 100644 --- a/tRules.tex +++ b/tRules.tex @@ -3,21 +3,28 @@ The input syntax for our algorithm is shown in figure \ref{fig:syntax} and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}. -The algorithm presented in this paper is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm. -Additional features like overriding methods and method overloading can be added by copying the respective parts from there. +Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm. The input language is designed to showcase type inference involving existential types. -We introduce the type rule T-Call which emulates a Java method call, +Method call rule T-Call is the most interesting part, because it emulates the behaviour of a Java method call, where existential types are implicitly \textit{opened} and \textit{closed}. -The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else} -and is solely used for examples. + +%The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}. +%and is solely used for examples. +The calculus does not include method overloading or method overriding for simplicity reasons. +Type inference for both are described in \cite{TIforFGJ} and can be added to this algorithm accordingly. +Our algorithm is designed for extensibility with the final goal of full support for Java. +\unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}. +Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}. + +%Additional features like overriding methods and method overloading can be added by copying the respective parts from there. %Additional features can be easily added by generating the respective constraints (Plümicke hier zitieren) -The type system in \cite{WildcardsNeedWitnessProtection} allows a method to \textit{override} an existing method declaration in one of its super classes, -but only by a method with the exact same type. -The type system presented here does not allow the \textit{overriding} of methods. -Our type inference algorithm consumes the input classes in succession and could only do a type check instead of type inference -on overriding methods, because their type is already determined. -Allowing overriding therefore has no implication on our type inference algorithm. +% The type system in \cite{WildcardsNeedWitnessProtection} allows a method to \textit{override} an existing method declaration in one of its super classes, +% but only by a method with the exact same type. +% The type system presented here does not allow the \textit{overriding} of methods. +% Our type inference algorithm consumes the input classes in succession and could only do a type check instead of type inference +% on overriding methods, because their type is already determined. +% Allowing overriding therefore has no implication on our type inference algorithm. \begin{figure} $