stan/WLP2024
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add Subtyping rules

Browse Source
This commit is contained in:
JanUlrich 2024-06-11 11:49:50 +02:00
parent 5f549ae540
commit d4040b2611
1 changed files with 15 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
aspUnify.tex
View File

@ -75,6 +75,21 @@ Java has adopted more and more type inference features over time.
Currently Java only has local type inference. Currently Java only has local type inference.
We want to bring type inference for Java to the next level. We want to bring type inference for Java to the next level.
\section{Subtyping}
\begin{mathpar}
\inferrule[Refl]{}{
\type{T} <: \type{T}
}
\and
\inferrule[Trans]{\type{T}_1 <: \type{T}_2 \\ \type{T}_2 <: \type{T}_3}{
\type{T}_1 <: \type{T}_3
}
\and
\inferrule[Class]{\texttt{class}\ \exptype{C}{\ol{X}} \triangleleft \type{N}}{
\exptype{C}{\ol{T}} <: [\ol{T}/\ol{X}]\type{N}
}
\end{mathpar}
\section{Unify} \section{Unify}
Input: Every type placeholder must have an upper bound. Input: Every type placeholder must have an upper bound.
Output: Every $\tv{a} \lessdot \type{T}$ constraint gets a Output: Every $\tv{a} \lessdot \type{T}$ constraint gets a