inference.tex

\chapter{Inferencing}
Once context-sensitive checks are made, the module can now be type inferred. Type inference is used to find the most general type of an expression. This is useful for assigning the most general type to variables and functions. It also is useful for performing type checking if the programmer specifies what type a function should take in or what a variable should be.
A type system is a set of rules that assign a property to various constructs in a programming language called type. A type is a property that allows the programmer to add constraints to programs \cite{Type:Type}.
The Haskell 2010 report says that Haskell's type system is a Hindley-Milner polymorphic type system \cite{TypeSystem:Hindley, TypeSystem:Milner} that has been extended with type classes to account for overloaded functions. The semantics in this paper makes precise what this means with regard to Haskell's specific syntax.
The type inference function infers the type of the expression that is fed into it. A purpose of it is to ensure that all functions and function applications are allowed with regard to the types of the inputs and outputs.

\section{Type theory}
Type theory was created by Bertrand Russell to prevent Russell's paradox for set theory, introduced by Georg Cantor. The issue was that not specifying a certain property for sets allowed sets to contain themselves in naive set theory. So Bertrand Russell prevented this problem by specifying a property called type for objects, and objects cannot contain their own type \cite{Stanford:TypeTheory}.
Type theory turns out to be useful for computer science.

\subsection{Simply Typed Lambda Calculus}
The Lambda Calculus was created by Alonzo Church as part of his research in foundations of mathematics. However, the Lambda Calculus was logically inconsistent, similar to set theory, shown by the Kleene-Rosser paradox.
In order to prevent the Kleene-Rosser paradox for the Lambda Calculus, Church introduced the concept of types into the Lambda Calculus. This is the Simply Typed Lambda Calculus \cite{TypeSystem:Simple}.
Later, it was shown that there is a correspondence between programming languages and the Lambda Calculus, which makes the Lambda Calculus a potential abstraction for programming languages.
Later still, it was shown that there is a correspondence between proof calculi and type systems, which links mathematics between formal logic and programs. This is the Curry-Howard correspondence.

\subsection{System F}
System F \cite{Reynolds2018} introduced the concept of polymorphic types into the Lambda Calculus. It accomplishes this by using universal quantifiers over the types in System F.

\subsection{Hindley-Milner}
The concept of type systems grew out of further complications to the types used in the Lambda Calculus.
The Hindley-Milner type system adds the concept of type inference to the Lambda Calculus. Type inference used in Hindley-Milner can acquire the most general type of a program without the user giving any type annotations.

\subsection{Meta Language}
The theoretical research in type theory and programming language semantics eventually lead to the Meta Language, also known as ML. It utilizes the Hindley-Milner type system. It also features a complete formal specification.

\section{Data Structures}

A monomorphic data type has no quantifiers. It is either a ground term itself, or a term composed of ground terms. For instance, a monomorphic data type can be $(a \rightarrow b) \rightarrow c$ if a, b, and c are also types.

In the K semantics, the equivalent data type looks like
\begin{lstlisting}
forAll ( .Set , funtype ( funtype ( a , b ) , c ) )
\end{lstlisting}

Note how there are no quantified variables.

A polymorphic data type, on the other hand, has quantifiers. An example polymorphic data type could look like $\forall a b c \, . \, (a \rightarrow b) \rightarrow c$

In the K semantics, the equivalent data type looks like
\begin{lstlisting}
forAll ( a b c , funtype ( funtype ( a , b ) , c ) )
\end{lstlisting}

There are two more data structures that are made to make type inference easier. The first map is from data constructors and term identifiers to their most general polymorphic types. This map is called \texttt{Beta}. The second one is a map from the type constructor names to arities. This map is called Delta. These maps are useful for type inference because the type inference function can quickly look up a type constructor within an expression and acquire its data type and arity.

To construct \texttt{Beta}, the semantics uses the already existing T data structure.

\subsection{Transform T into Beta}
\begin{lstlisting}
    // STEP 3 Transform T into beta

    syntax KItem ::= "startTTransform"
    syntax KItem ::= "constructDelta"
    syntax KItem ::= "constructBeta"

    rule <k> startTTransform
             => constructDelta
                ~> (constructBeta) ...</k>

    rule <k> constructDelta
             => makeDelta(T,.Map) ...</k>
         <tempT> T:K </tempT>

    syntax KItem ::= makeDelta(K,Map) [function] //(T,Delta)
    syntax KItem ::= newDelta(Map) //Delta
    syntax KItem ::= newBeta(Map) //beta
    syntax List ::= retPolyList(K,List) [function] //(T,Delta)
\end{lstlisting}

\subsection{Construct Beta}
Beta is a map from the type constructor to its corresponding type.

\subsubsection{Example}
If the user makes the data type \texttt{CusBool} in module $Simp5$, and declares it with the example
\begin{lstlisting}
data CusBool = True2 | False2
\end{lstlisting}

\noindent
then the corresponding $tempBeta$ should look like this:

\begin{lstlisting}
    <tempBeta>
        ModPlusType ( Simp5 , False2 ) |-> forAll ( .Set , CusBool .TyVars )
        ModPlusType ( Simp5 , True2 ) |-> forAll ( .Set , CusBool .TyVars )
    </tempBeta>
\end{lstlisting}

\noindent
Note how the monomorphic datatype just has an empty $forAll$.

If the user makes the data type CusBool in module Simp5, and declares it with the example
\begin{lstlisting}
data CusBool a b = True2 a | False2 b
\end{lstlisting}

\noindent
then the corresponding tempBeta should look like this.
\begin{lstlisting}
    <tempBeta>
        ModPlusType ( Simp5 , False2 ) |-> forAll ( b , funtype ( b , CusBool a b ) )
        ModPlusType ( Simp5 , True2 ) |-> forAll ( a , funtype ( a , CusBool a b ) )
    </tempBeta>

\end{lstlisting}

\subsubsection{K Code}
The following is the K Code.

\begin{lstlisting}
    rule <k> constructBeta
             => makeBeta(T,.Map) ...</k>
         <tempT> T:K </tempT>

    syntax KItem ::= makeBeta(K,Map) [function] //(T,Beta,Delta)

    rule makeBeta(TList(ListItem(TObject(ModName:K,A:K,B:K,ListItem(InnerTPiece(Con:K,H:K,D:K,E:K,F:K)) InnerRest:List)) Rest:List),Beta:Map) =>
         makeBeta(TList(ListItem(TObject(ModName,A,B,InnerRest)) Rest),Beta[ModPlusType(ModName,Con) <- betaParser(E,B,A)])
    rule makeBeta(TList(ListItem(TObject(ModName:K,A:K,B:K,.List)) Rest:List),Beta:Map) =>
         makeBeta(TList(Rest),Beta)
    rule makeBeta(TList(.List),Beta:Map) =>
         newBeta(Beta)

    syntax KItem ::= betaParser(K,K,K) [function] //(Tree Piece,NewSyntax,Parameters,Constr)
    syntax Set ::= getTyVarsRHS(K,List) [function]

    syntax KItem ::= forAll(Set,K)
    syntax KItem ::= funtype(K,K)

    syntax Set ::= listToSet(List, Set) [function]

    rule listToSet(ListItem(A:KItem) L:List, S:Set) => listToSet(L, SetItem(A) S)
    rule listToSet(.List, S:Set) => S


//if optbangAtypes, need to see if first variable is a typecon
//if its a typecon then need to go into Delta and see the amount of parameters it has
//then count the number of optbangAtypes after the typecon
    rule betaParser('constrCon(A:K,, B:K), Par:K, Con:K) => forAll(getTyVarsRHS(B,.List), betaParser(B, Par, Con))
    rule betaParser('optBangATypes('optBangAType('emptyBang(.KList),, 'atypeTyVar(Tyv:K)),, Rest:K), Par:K, Con:K) => funtype(Tyv, betaParser(Rest, Par, Con))
    rule betaParser('optBangATypes('optBangAType('emptyBang(.KList),, 'baTypeCon(A:K,, B:K)),, Rest:K), Par:K, Con:K) => funtype('baTypeCon(A:K,, B:K), betaParser(Rest, Par, Con))
    rule betaParser('optBangATypes('optBangAType('emptyBang(.KList),, 'atypeGTyCon(Tyc:K)),, Rest:K), Par:K, Con:K) => funtype(Tyc, betaParser(Rest, Par, Con))
    rule betaParser(.OptBangATypes, Par:K, Con:K) => 'simpleTypeCon(Con,, Par)

    rule getTyVarsRHS(.OptBangATypes,Tylist:List) => listToSet(Tylist, .Set)

    rule <k> newBeta(M:Map)
             => .K ...</k>
         <tempBeta> OldBeta:K => M </tempBeta>
\end{lstlisting}

\subsection{Construct Delta}
Delta contains the arity of the user defined dataTypes. So if a user defined datatype takes in two parameters, tempDelta will contain the number 2.

\subsubsection{Example}
If the user makes the data type $CusBool$ in module $Simp5$, and declares it with the example
\begin{lstlisting}
data CusBool a b = True2 a | False2 b
\end{lstlisting}

\noindent
then the corresponding $tempDelta$ should look like this.

\begin{lstlisting}
<tempDelta>
     ModPlusType ( Simp5 , CusBool ) |-> 2
</tempDelta>
\end{lstlisting}

\begin{lstlisting}
    rule makeDelta(TList(ListItem(TObject(ModName:K,A:K,Polys:K,C:K)) Rest:List),M:Map) =>
         makeDelta(TList(Rest),M[ModPlusType(ModName,A) <- size(retPolyList(Polys,.List))])
    rule makeDelta(TList(.List),M:Map) => newDelta(M)

    rule retPolyList('typeVars(A:K,,Rest:K),NewList:List) => retPolyList(Rest, ListItem(A) NewList)
    rule retPolyList(.TyVars,L:List) => L

    rule <k> newDelta(M:Map)
             => .K ...</k>
         <tempDelta> OldDelta:K => M </tempDelta>

\end{lstlisting}


\section{Definition of Substitution}
A substitution is a set of variables and their replacements. Applying a substitution to an expression means to simultaneously replace each variable in the expression with the replacement term \cite{Infer:TypeSub}.

\section{Inference Algorithm}
The inference function acquires the most general data type for the expression that is fed into it. It inducts down into an expression to the most primitive parts of the expression, and then collects information about each of the primitive parts and how they combine together. Then it passes the information back up the layers and slowly acquires all the information about the most general type of the expression. 
Much of the inference algorithm is the same as the one introduced in CS 421. This is also used in the definition of Standard ML \cite{CS421:Unif, Milner90thedefinition}.

\begin{lstlisting}
requires "haskell-syntax.k"
requires "haskell-configuration.k"
requires "haskell-preprocessing.k"

module HASKELL-TYPE-INFERENCING
    imports HASKELL-SYNTAX
    imports HASKELL-CONFIGURATION
    imports HASKELL-PREPROCESSING

    syntax KItem ::= "Bool" //Boolean

    // STEP 4 Type Inferencing
    syntax KItem ::= inferenceShell(K) [function]//Input, AlphaMap, Beta, Delta, Gamma
    //syntax KItem ::= typeInferenceFun(K,Map,Map,Map,Map,K,K) [function]//Input, Alpha, Beta, Delta, Gamma
    //syntax KItem ::= typeInferenceFun(Map,K,K) //Gamma, Expression, Guessed Type
    syntax Map ::= genGamma(K,Map,K) [function] //Apatlist, Gamma Type
    syntax KItem ::= genLambda(K,K) [function]
    syntax KItem ::= guessType(Int)
    syntax KItem ::= freshInstance(K, Int) [function]
    syntax Int ::= paramSize(K) [function]


    syntax KItem ::= mapBag(Map)
    syntax KResult ::= mapBagResult(Map)

    syntax Map ::= gammaSub(Map,Map,Map) [function]//substitution, gamma

    rule <k> performIndividualInferencing => inferenceShell(Code) ...</k>
         <tempModule> Mod:KItem </tempModule>

         <moduleName> 'moduleName(Mod) </moduleName>
         <moduleTempCode> Code:KItem </moduleTempCode>

    rule inferenceShell('topdeclslist('type(A:K,, B:K),, Rest:K)) =>
         inferenceShell(Rest) //constructalpha
    rule inferenceShell('topdeclslist('data(A:K,, B:K,, C:K,, D:K),, Rest:K)) =>
         inferenceShell(Rest)
    rule inferenceShell('topdeclslist('newtype(A:K,, B:K,, C:K,, D:K),, Rest:K)) =>
         inferenceShell(Rest)
    rule inferenceShell('topdeclslist('class(A:K,, B:K,, C:K,, D:K),, Rest:K)) =>
         inferenceShell(Rest)
    rule inferenceShell('topdeclslist('instance(A:K,, B:K,, C:K,, D:K),, Rest:K)) =>
         inferenceShell(Rest)
    rule inferenceShell('topdeclslist('default(A:K,, B:K,, C:K,, D:K),, Rest:K)) =>
         inferenceShell(Rest)
    rule inferenceShell('topdeclslist('foreign(A:K,, B:K,, C:K,, D:K),, Rest:K)) =>
         inferenceShell(Rest)

    rule inferenceShell('topdeclslist('topdecldecl(A:K),, Rest:K)) =>
         typeInferenceFun(.ElemList, .Map,A,guessType(0)) ~> inferenceShell(Rest)


    rule <k> typeInferenceFun(.ElemList, Gamma:Map, 'declFunLhsRhs(Fn:K,, Lhsrhs:K), Guess:K) =>
         typeInferenceFun(.ElemList, Gamma, Lhsrhs, Guess) ...</k>
    rule <k> typeInferenceFun(.ElemList, Gamma:Map, 'eqExpOptDecls(Ex:K,, Optdecls:K), Guess:K) =>
         typeInferenceFun(.ElemList, Gamma, Ex, Guess) ...</k>
\end{lstlisting}

\subsection{Variable Rule}
The variable rule is used whenever the inference function encounters a variable. It looks up the variable in the environment, and then acquires the corresponding polymorphic type of the variable in the environment. It then calls \texttt{freshInstance} which removes all quantifiers and converts this type to a monomorphic type. This is because we cannot induct any further on the variable \texttt{x}, so any quantified variables that the type of \texttt{x} contains should instead become free variables. This is because \texttt{x} does not act upon anything. The rule then calls unify and sets the fresh type assigned to the variable equal to the output of the \texttt{freshInstance} function.

\begin{prooftree}
\AxiomC{}
\RightLabel{Variable}
\UnaryInfC{$\Gamma \vdash x : \tau \, | \, \text{unify}\{ ( \tau , \text{freshInstance}(\Gamma(x)))\}$}
\end{prooftree}

\begin{lstlisting}
    rule <k> typeInferenceFun(.ElemList, (Var |-> Type:K) Gamma:Map, 'aexpQVar(Var:K), Guess:KItem)
          => mapBagResult(uniFun(ListItem(uniPair(Guess,freshInstance(Type, TypeIt))))) ...</k> //Variable rule
         <typeIterator> TypeIt:Int => TypeIt +Int paramSize(Type) </typeIterator>
\end{lstlisting}
\subsection{Constant Rule}
The constant rule is much like the variable rule. The constant rule is used whenever the inference function encounters a constant. It looks up the constant in the \texttt{Beta} map, and then acquires the corresponding polymorphic type of the constant in the map. It then calls \texttt{freshInstance} which removes all quantifiers and converts this type to a monomorphic type. This is because we cannot induct any further on the constant \texttt{c}, so any quantified variables that the type of \texttt{c} contains should instead become free variables. This is because \texttt{c} does not act upon anything. The rule then calls unify and sets the fresh type assigned to the constant equal to the output of the \texttt{freshInstance} function.

\begin{prooftree}
\AxiomC{}
\RightLabel{Constant}
\UnaryInfC{$\Gamma \vdash c : \tau \, | \, \text{unify}\{ ( \tau , \text{freshInstance}(\tau))\}$}
\end{prooftree}

\begin{lstlisting}
    rule <k> typeInferenceFun(.ElemList, Gamma:Map, 'aexpGCon('conTyCon(Mid:K,, Gcon:K)), Guess:KItem)
          => mapBagResult(uniFun(ListItem(uniPair(Guess,freshInstance(Type, TypeIt))))) ...</k> //Constant rule
         <tempBeta> (ModPlusType(Mid,Gcon) |-> Type:K) Beta:Map </tempBeta>
         <typeIterator> TypeIt:Int => TypeIt +Int paramSize(Type) </typeIterator>
\end{lstlisting}

\subsection{Lambda Rule}

The lambda rule is used for lambda expressions. It overwrites the type of \texttt{x} with a fresh type in the environment \texttt{$\tau_1$}, and inducts on e with a different fresh type \texttt{$\tau_2$}. When that corresponds to a substitution, it first looks up the guessed type of the lambda expression in the substitution. It then also looks up the term \texttt{$\tau_1 \rightarrow \tau_2$} within the substitution as well. This is because if the substitution reveals additional information about these fresh types, we can remove the fresh types and replace them with types that reveal more information about them instead. We then set them equal, because the type of this lambda expression is \texttt{$\tau_1 \rightarrow \tau_2$}.

Also, a lambda expression that takes in multiple variables is instead transformed into multiple lambda expressions that each take in one variable.

Also, functions that take in variables can be desugared to variables that are set equal to lambda terms within a let expression. So, the let-In rule coupled with the lambda rule can infer the type of a function in Haskell, and we do not need an extra rule.

\begin{prooftree}
\AxiomC{$[x : \tau_1] + \Gamma \vdash e : \tau_2 \, | \, \sigma$}
\RightLabel{Lambda}
\UnaryInfC{$\Gamma \vdash \text{\textbackslash \, x \textrightarrow \, e}: \tau \, | \, \text{unify}\{ ( \sigma(\tau) , \sigma(\tau_1 \rightarrow \tau_2)) \} \circ \sigma$}
\end{prooftree}

\begin{lstlisting}

   syntax KItem ::= typeInferenceFun(ElemList, Map, K, K) [strict(1)]
   syntax KItem ::= typeInferenceFunLambda(ElemList, K, K, K) [strict(1)]
/* automatically generated by the strict(1) in typeInferenceFun or typeInferenceFunAux
   rule typeInferenceFunAux(Es:ElemList, C:K, A:K, B:K) => Es ~> typeInferenceFun(HOLE, C, A, B)
        requires notBool isKResult(Es)
   rule Es:KResult ~> typeInferenceFunAux(HOLE, C:K,A:K, B:K) => typeInferenceFun(Es, C, A, B)
*/     

    //lambda rule
    rule <k> typeInferenceFun(.ElemList, Gamma:Map, 'lambdaFun(Apatlist:K,, Ex:K), Guess:KItem)
          => typeInferenceFunLambda(val(typeInferenceFun(.ElemList, genGamma(Apatlist,Gamma,guessType(TypeIt)), genLambda(Apatlist,Ex), guessType(TypeIt +Int 1))), .ElemList, Guess, guessType(TypeIt),guessType(TypeIt +Int 1)) ...</k>
         <typeIterator> TypeIt:Int => TypeIt +Int 2 </typeIterator>

    rule <k> typeInferenceFunLambda(valValue(mapBagResult(Sigma:Map)), .ElemList, Tau:K, Tauone:K, Tautwo:K)
         => mapBagResult(compose(uniFun(ListItem(uniPair(typeSub(Sigma,Tau),typeSub(Sigma,funtype(Tauone,Tautwo))))),Sigma)) ...</k>
    
\end{lstlisting}

\subsection{Application Rule}

The application is similar to the lambda rule. The rule inducts on the leftmost expression and places the constraint of the leftmost expression being a function into the recursive call. Then when it gets a substitution, it looks up the fresh type \texttt{$\tau_1$} within the substitution to get any additional information about the fresh type that we may have. Afterwards it inducts upon the rightmost expression and acquires another substitution. It then composes them and returns that substitution.

\begin{prooftree}
\AxiomC{$\Gamma \vdash e_1 : \tau_1 \rightarrow \tau \, | \, \sigma_1$}
\AxiomC{$\sigma_1(\Gamma) \vdash e_2 : \sigma_1(\tau_1) \, | \, \sigma_2$}
\RightLabel{Application}
\BinaryInfC{$\Gamma \vdash e_1 e_2 : \tau \, | \, \sigma_2 \circ \sigma_1$}
\end{prooftree}

\begin{lstlisting}

    syntax KItem ::= typeInferenceFunAppli(ElemList, Map, K, K, Map) [strict(1)]

    //application rule
    rule <k> typeInferenceFun(.ElemList, Gamma:Map, 'funApp(Eone:K,, Etwo:K), Guess:KItem)
          => typeInferenceFunAppli(val(typeInferenceFun(.ElemList, Gamma, Eone, funtype(guessType(TypeIt),Guess))), .ElemList, Gamma, Etwo, guessType(TypeIt), .Map) ...</k>
         <typeIterator> TypeIt:Int => TypeIt +Int 1 </typeIterator>

    rule <k> typeInferenceFunAppli(valValue(mapBagResult(Sigmaone:Map)), .ElemList, Gamma:Map, Etwo:KItem, guessType(TypeIt:Int), .Map)
          => typeInferenceFunAppli(val(typeInferenceFun(.ElemList, gammaSub(Sigmaone, Gamma, .Map), Etwo, typeSub(Sigmaone, guessType(TypeIt)))), .ElemList, .Map, .K, .K, Sigmaone) ...</k>

    rule <k> typeInferenceFunAppli(valValue(mapBagResult(Sigmatwo:Map)), .ElemList, .Map, .K, .K, Sigmaone:Map)
          => mapBagResult(compose(Sigmatwo, Sigmaone)) ...</k>

\end{lstlisting}

\subsection{IfThenElse Rule}

Function guards, cases, and if-then-else are all equivalent. This means that function guards and cases can both be desugared to if-then-else rules and the inference function only has to care about encountering an if-then-else rule to account for all three.

The rule is very similar to the compose rule and the lambda rule. It just keeps inducting into each term and collects information about the types from each of them and then returns back the information it acquired from all three. The only interesting constraint is that the first term must be a Boolean.

\begin{prooftree}
\AxiomC{$\Gamma \vdash e_1 : \text{bool} \, | \, \sigma_1$}
\AxiomC{$\sigma_1(\Gamma) \vdash e_2 : \sigma_1(\tau) \, | \, \sigma_2$}
\AxiomC{$T_2$}
\RightLabel{IfThenElse}
\TrinaryInfC{$\Gamma \vdash \text{if} \, e_1 \, \text{then} \, e_2 \, \text{else} \, e_3 : \tau \, | \, \sigma_3 \circ \sigma_2 \circ \sigma_1$}
\end{prooftree}

\noindent
where $T_2 = \sigma_2 \circ \sigma_1(\Gamma) \vdash e_3 : \sigma_2 \circ \sigma_1(\tau) \, | \, \sigma_3$

\begin{lstlisting}

    syntax KItem ::= typeInferenceFunIfThen(ElemList, Map, K, K, K, Map, Map) [strict(1)]

    //if_then_else rule
    rule <k> typeInferenceFun(.ElemList, Gamma:Map, 'ifThenElse(Eone:K,, Optsem:K,, Etwo:K,, Optsemtwo:K,, Ethree:K), Guess:KItem)
          => typeInferenceFunIfThen(val(typeInferenceFun(.ElemList, Gamma, Eone, Bool)), .ElemList, Gamma, Etwo, Ethree, Guess, .Map, .Map) ...</k>

    rule <k> typeInferenceFunIfThen(valValue(mapBagResult(Sigmaone:Map)), .ElemList, Gamma:Map, Etwo:KItem, Ethree:KItem, Guess:KItem, .Map, .Map)
          => typeInferenceFunIfThen(val(typeInferenceFun(.ElemList, gammaSub(Sigmaone, Gamma, .Map), Etwo, typeSub(Sigmaone, Guess))), .ElemList, Gamma, .K, Ethree, Guess, Sigmaone, .Map) ...</k>

    rule <k> typeInferenceFunIfThen(valValue(mapBagResult(Sigmatwo:Map)), .ElemList, Gamma:Map, .K, Ethree:KItem, Guess:KItem, Sigmaone:Map, .Map)
          => typeInferenceFunIfThen(val(typeInferenceFun(.ElemList, gammaSub(compose(Sigmatwo, Sigmaone), Gamma, .Map), Ethree, typeSub(compose(Sigmatwo, Sigmaone), Guess))), .ElemList, .Map, .K, .K, .K, Sigmaone, Sigmatwo) ...</k>

    rule <k> typeInferenceFunIfThen(valValue(mapBagResult(Sigmathree:Map)), .ElemList, .Map, .K, .K, .K, Sigmaone:Map, Sigmatwo:Map)
          => mapBagResult(compose(compose(Sigmathree, Sigmatwo), Sigmaone)) ...</k>
          
\end{lstlisting}

\section{Mutual Recursion}
Note that mutually recursive functions are allowed in Haskell.
For example:
$$
f x = y x
$$
$$
y x = f x
$$
This set of functions is allowed to compile. When run, the function simply runs forever. This is unlike standard ML \cite{Milner90thedefinition}, which does not allow for mutually recursive functions.

This is also the case for LetIn expressions. These expressions also allow for mutual recursion, where the inside of each declaration within the let expression can refer to other declarations within the let expression.

For instance, an expression that could be written in Haskell is

\begin{lstlisting}
let {f = \x -> y x; y = \x -> f x} in (f 2)
\end{lstlisting}

In this example, the \texttt{f} is an expression that refers to \texttt{y} and \texttt{y} is an expression that refers to \texttt{f}.

\subsection{LetIn Rule}
This let rule, unlike the let rule introduced in CS 421, allows for mutual recursion.

The let rule assigns each declaration within the let expression a new fresh monomorphic type. Each of these types is collected in a new environment called \texttt{$\Psi$}. It then inducts into each declaration and keeps collecting type information from each one. As it does this, it keeps composing the substitutions it collects from each declaration and looks up all the type variables within the substitution composition to keep adding the information gathered from each declaration. After it finishes doing this, it finally calls GEN on each type given to the declarations, to make them polymorphic for all the remaining free variables. Afterwards it maps all the variables to these new generated types within the environment. Finally, it inducts within the expression with this new environment, and gives it the type of the substitution of \texttt{$\tau$}.

\begin{prooftree}
\AxiomC{$\sigma_{i + 1} ( \Psi + \Gamma ) \vdash e_i : \Psi(x_i) \, | \, \sigma_j$}
\RightLabel{LetIn}
\UnaryInfC{$\Gamma \vdash \{ \, x_1 = e_1; \, \cdots \, x_i = e_i; \, \cdots \, x_n = e_n \, \} \, \text{in} \, \text{exp} : \Xi$}
\end{prooftree}

\noindent
where

$$\text{dom} ( \Psi ) = \{ \, x_1, \cdots, x_n \, \}$$

$$\sigma_0' = \{\}$$

$$\sigma_i' = \sigma_i \circ \sigma_{j + 1}'$$

$$\Xi = \bigcup_{i = 1}^n \, \{ \, x_i \mapsto \, \text{GEN} \, ( \sigma_n'(\Gamma),\sigma_n'(\psi_i) ) \, \} \, | \, \sigma_n'$$

\begin{prooftree}
\AxiomC{$\Gamma \vdash \{ \, \text{decls} \, \} : \Delta \, | \, \sigma$}
\AxiomC{$\sigma ( \Delta + \Gamma ) \vdash e : \tau \, | \, \sigma'$}
\RightLabel{LetIn}
\BinaryInfC{$\Gamma \vdash \text{let} \, \{ \, \text{decls} \, \} \, \text{in} \, \text{exp} : \tau \, | \, \sigma' \circ \sigma$}
\end{prooftree}

\subsubsection{Module}

This rule can then be applied to an entire module. An entire module can be inferred in the same way, if the only parts of the module that need to be inferred are the declarations within the module. This is how the semantics can begin the inference algorithm upon a Haskell module, because a module contains everything else.

\begin{prooftree}
\AxiomC{$\Gamma \vdash \{ \, \text{decls} \, \} : \Delta \, | \, \sigma$}
\RightLabel{Module}
\UnaryInfC{$\Gamma \vdash \text{module} \, \{ \, \text{decls} \, \} : \Delta \, | \, \sigma$}
\end{prooftree}

\subsubsection{K Code}

\begin{lstlisting}

    syntax KItem ::= typeInferenceFunLetIn(ElemList, Map, Map, K, K, K, Int, Int, Map, Map) [strict(1)]
    syntax KItem ::= grabLetDeclName(K, Int) [function]
    syntax KItem ::= grabLetDeclExp(K, Int) [function]
    syntax KItem ::= mapLookup(Map, K) [function]
    syntax Map ::= makeDeclMap(K, Int, Map) [function]
    syntax Map ::= applyGEN(Map, Map, Map, Map) [function]

    //Haskell let in rule (let rec in exp + let in rule combined)
    //gamma |- let rec f1 = e1 and f2 = e2 and f3 = e3 .... in e =>
    //beta, [f1 -> tau1, f2 -> tau2, f3 -> tau3,....] + gamma |- e1 : tau1 | sigma1,  [f1 -> simga1(tau1), f2 -> sigma1(tau2), f3 -> sigma1(tau3),....] + sigma1(gamma) |- e2 : sigma1(tau2) | sigma2  [f1 -> sigma2 o sigma1(tau1), f2 -> sigma2 o sigma1(tau2), f3 -> sigma2 o sigma1(tau3),....] + sigma2 o sigma1(gamma) |- e3 : sigma2 o sigma1(tau3) .....  [f1 -> gen(sigma_n o sigma2 o sigma1(tau1), sigma_n o sigma2 o sigma1(Gamma)), f2 -> gen(tau2), f3 -> gen(tau3),....] + gamma |- e : something
    rule <k> typeInferenceFun(.ElemList, Gamma:Map, 'letIn(D:K,, E:K), Guess:KItem)
          => typeInferenceFunLetIn(.ElemList, Gamma, makeDeclMap(D, TypeIt, .Map), D, E, Guess, 0, TypeIt, .Map, Beta) ...</k>
         <typeIterator> TypeIt:Int => TypeIt +Int size(makeDeclMap(D, TypeIt, .Map)) </typeIterator>
         <tempBeta> Beta:Map </tempBeta>

    rule <k> typeInferenceFunLetIn(.ElemList, Gamma:Map, DeclMap:Map, D:KItem, E:KItem, Guess:KItem, Iter:Int, TypeIt:Int, OldSigma:Map, Beta:Map)
           => typeInferenceFunLetIn(val(typeInferenceFun(.ElemList, Gamma DeclMap, grabLetDeclExp(D, Iter), mapLookup(DeclMap, grabLetDeclName(D, Iter)))), .ElemList, Gamma, DeclMap, D, E, Guess, Iter, TypeIt, OldSigma, Beta) ...</k>
          //=> typeInferenceFunLetIn(val(typeInferenceFun(DeclMap, grabLetDeclExp(D, Iter +Int TypeIt), Guess)), .ElemList, Gamma, DeclMap, D, E, Guess, Iter, TypeIt, OldSigma) ...</k>
          requires Iter <Int (size(DeclMap))

    rule <k> typeInferenceFunLetIn(valValue(mapBagResult(Sigma:Map)), .ElemList, Gamma:Map, DeclMap:Map, D:KItem, E:KItem, Guess:KItem, Iter:Int, TypeIt:Int, OldSigma:Map, Beta:Map)
          => typeInferenceFunLetIn(.ElemList, gammaSub(Sigma,Gamma,.Map), gammaSub(Sigma, DeclMap,.Map), D, E, typeSub(Sigma, Guess), Iter +Int 1, TypeIt, compose(Sigma,OldSigma), Beta) ...</k>
          requires Iter <Int (size(DeclMap))

    rule <k> typeInferenceFunLetIn(.ElemList, Gamma:Map, DeclMap:Map, D:KItem, E:KItem, Guess:KItem, Iter:Int, TypeIt:Int, OldSigma:Map, Beta:Map)
          => typeInferenceFunLetIn(val(typeInferenceFun(.ElemList, Gamma applyGEN(Gamma, DeclMap, .Map, Beta), E, Guess)), .ElemList, Gamma, DeclMap, D, E, Guess, Iter, TypeIt, OldSigma, Beta) ...</k>
          requires Iter >=Int (size(DeclMap))

    rule <k> typeInferenceFunLetIn(valValue(mapBagResult(Sigma:Map)), .ElemList, Gamma:Map, DeclMap:Map, D:KItem, E:KItem, Guess:KItem, Iter:Int, TypeIt:Int, OldSigma:Map, Beta:Map)
          => mapBagResult(compose(Sigma, OldSigma))...</k>
          requires Iter >=Int (size(DeclMap))
          
          
\end{lstlisting}
\section{Helper Functions}

These helper functions are necessary for the inference function.

\begin{lstlisting}

    rule mapLookup((Name |-> Type:KItem) DeclMap:Map, Name:KItem) => Type
    rule mapLookup(DeclMap:Map, Name:KItem) => Name
         requires notBool(Name in keys(DeclMap))

    rule makeDeclMap('decls(Dec:K), TypeIt:Int, NewMap:Map) => makeDeclMap(Dec, TypeIt, NewMap)
    rule makeDeclMap('declsList('declPatRhs('apatVar(Var:K),, Righthand:K),, Rest:K), TypeIt:Int, NewMap:Map) => makeDeclMap('decls(Rest), TypeIt +Int 1, NewMap[Var <- guessType(TypeIt)])
    rule makeDeclMap(.DeclsList, TypeIt:Int, NewMap:Map) => NewMap

    rule grabLetDeclName('decls(Dec:K), Iter:Int) => grabLetDeclName(Dec, Iter)
    rule grabLetDeclName('declsList(Dec:K,, Rest:K), Iter:Int) => grabLetDeclName(Rest, Iter -Int 1)
         requires Iter >Int 0
    rule grabLetDeclName('declsList('declPatRhs('apatVar(Var:K),, Righthand:K),, Rest:K), Iter:Int) => Var
         requires Iter <=Int 0


    rule grabLetDeclExp('decls(Dec:K), Iter:Int) => grabLetDeclExp(Dec, Iter)
    rule grabLetDeclExp('declsList(Dec:K,, Rest:K), Iter:Int) => grabLetDeclExp(Rest, Iter -Int 1)
         requires Iter >Int 0
    rule grabLetDeclExp('declsList('declPatRhs('apatVar(Var:K),, Righthand:K),, Rest:K), Iter:Int) => grabLetDeclExp(Righthand, Iter)
         requires Iter <=Int 0
    rule grabLetDeclExp('eqExpOptDecls(Righthand:K,, Opt:K), Iter:Int) => 'eqExpOptDecls(Righthand,, Opt)

    rule genGamma('apatVar(Vari:K), Gamma:Map, Guess:K) => Gamma[Vari <- Guess]
    rule genGamma('apatCon(Vari:K,, Pattwo:K), Gamma:Map, Guess:K) => Gamma[Vari <- Guess]

    rule genLambda('apatVar(Vari:K), Ex:K) => Ex
    rule genLambda('apatCon(Vari:K,, Pattwo:K), Ex:K) => 'lambdaFun(Pattwo,, Ex)


    rule gammaSub(Sigma:Map, (Key:KItem |-> Type:KItem) Gamma:Map, Newgamma:Map)
        => gammaSub(Sigma, Gamma, Newgamma[Key <- typeSub(Sigma, Type) ] )

    rule gammaSub(Sigma:Map, .Map, Newgamma:Map)
      => Newgamma
\end{lstlisting}
\section{Fresh Instance}

Fresh Instance takes in a polymorphic variable and removes all the quantifiers by taking all quantified variables and replacing them with fresh unused types.

\begin{lstlisting}
    rule freshInstance(guessType(TypeIt:Int), Iter:Int) => guessType(TypeIt)
    rule freshInstance(forAll(.Set, B:K), Iter:Int) => B
    rule freshInstance(forAll(SetItem(C:KItem) A:Set, B:K), Iter:Int) => freshInstance(forAll(A, freshInstanceInner(C, B, Iter)), Iter +Int 1)

    syntax KItem ::= freshInstanceInner(K,K,Int) [function]

    rule freshInstanceInner(Repl:KItem, funtype(A:K, B:K), Iter:Int) => funtype(freshInstanceInner(Repl,A,Iter),freshInstanceInner(Repl,B,Iter))
    rule freshInstanceInner(Repl:KItem, Repl, Iter:Int) => guessType(Iter)
    rule freshInstanceInner(Repl:KItem, Target:KItem, Iter:Int) => Target [owise]

    rule paramSize(forAll(A:Set, B:K)) => size(A)
    rule paramSize(A:K) => 0 [owise]
\end{lstlisting}

\section{GEN}

The GEN function takes in a monomorphic type and an environment. It will add quantifiers to all free variables in the type that do not appear in the environment.

The rules of GEN are as follows. Note that it just looks for free variables that are in the type that do not appear in the environment and will then add quantifiers.

$$\text{GEN}(\Gamma,\tau) = \forall \alpha_1, \cdots, \alpha_n \, . \, \tau$$
where
$$\{ \, \alpha_1, \cdots, \alpha_n \, \} = \text{freevarsty}(\tau) - \text{freevarsenv}(\Gamma)$$
$$\text{freevarsty}('\alpha) = \{ \, '\alpha \, \}$$
$$\text{freevarsty}(c) = \{\}$$ where $c$ is a type such as $Int$
$$\text{freevarsty}(c(\tau_1, \cdots, \tau_n)) = \bigcup_{i = 1}^n \text{freevarsty}(\tau_i)$$
$$\text{freevarsty}(\forall \alpha_1, \cdots, \alpha_n \, . \, \tau) = \text{freevarsty}(\tau) - \{ \, \alpha_1, \cdots, \alpha_n \, \}$$
$$\text{freevarsenv}(\Gamma) = \bigcup_{x \in \text{dom}(\Gamma)}\text{freevarsty}(\Gamma(x))$$

The K Code is as follows.

\begin{lstlisting}
     rule applyGEN(Gamma:Map, (Key:KItem |-> Type:KItem) DeclMap:Map, NewMap:Map, Beta:Map)
       => applyGEN(Gamma, DeclMap, NewMap[Key <- gen(Gamma, Type, Beta)], Beta)

     rule applyGEN(Gamma:Map, .Map, NewMap:Map, Beta:Map)
       => NewMap

    //GEN
    //GEN(Gamma, Tau) => Forall alpha

    syntax KItem ::= gen(Map, K, Map) [function]
    syntax Set ::= freeVarsTy(K, Map) [function]
    syntax Set ::= freeVarsEnv(Map, Map) [function]


    rule gen(Gamma:Map, forAll(Para:Set, Tau:KItem), Beta:Map) => forAll(freeVarsTy(forAll(Para:Set, Tau), Beta) -Set freeVarsEnv(Gamma, Beta), Tau)
    rule gen(Gamma:Map, Tau:KItem, Beta:Map) => forAll(freeVarsTy(Tau, Beta) -Set freeVarsEnv(Gamma, Beta), Tau) [owise]

    //rule gen(Gamma:Map, forAll(Para:Set, Tau:KItem), Beta:Map) => forAll(freeVarsTy(forAll(Para:Set, Tau), Beta) -Set freeVarsEnv(Gamma, Beta), Tau)

    rule freeVarsTy(guessType(TypeIt:Int), Beta:Map) => SetItem(guessType(TypeIt:Int))
    rule freeVarsTy(funtype(Tauone:KItem, Tautwo:KItem), Beta:Map) => freeVarsTy(Tauone, Beta) freeVarsTy(Tautwo, Beta)
    rule freeVarsTy(Tau:KItem, Beta:Map) => .Set
         requires (forAll(.Set, Tau)) in values(Beta)
    rule freeVarsTy(forAll(Para:Set, Tau:KItem), Beta:Map) => freeVarsTy(Tau, Beta) -Set Para
    rule freeVarsEnv(Gamma:Map, Beta:Map) => listToSet(values(Beta), .Set)
\end{lstlisting}
\section{Unification Algorithm}

The goal of the unification algorithm is to provide a substitution. This substitution is used to map variables to monomorphic types. The goal of the substitution is to look up a variable in an expression or an environment 

This unification algorithm is provided from CS 421 \cite{CS421:Unif}.

Let $S = \{(s_1 , t_1), (s_2 , t_2), \cdots, (s_n , t_n)\}$ be a
unification problem.

\subsection{Identity}
If the input is empty, then return the identity substitution.

Case $S = \{ \} : \text{Unif}(S) = \text{Identity function}$ (ie
no substitution)

\subsection{Non-Identity}

Case $S = \{(s, t)\} \cup S'$: Four main steps

\subsubsection{Delete}

If the two terms that are set equal are already equal, then they are not necessary in the substitution map. They can be removed.

Delete: if $s = t$ (they are the same term)
then $Unif(S) = Unif(S')$

\subsubsection{Decompose}

If the two terms use the same constructor and contain the same number of children, this means that each child can be set equal. 

Decompose: if $s = f(q_1, \cdots, q_m )$ and
$t = f(r_1, \cdots, r_m )$ (same f, same m!), then
$\text{Unif}(S) = \text{Unif}(\{(q_1 , r_1 ), ..., (q_m , r_m )\} \cup S')$

\subsubsection{Orient}

The substitution should map variables to non-variables, so if the equation has a non-variable mapped to a variable, it should be oriented the other way.

Orient: if $t = x$ is a variable, and s is not a
variable, $\text{Unif}(S) = \text{Unif} (\{(x,s)\} \cup S')$.

\subsubsection{Eliminate}

This rule removes an equation from the set and adds it to the substitution map if the conditions of the equation are met.

Eliminate: if s = x is a variable, and
x does not occur in t (the occurs
check), then

Let $\phi = x \mapsto t$

Let $\psi = \text{Unif}(\phi(S'))$

$\text{Unif}(S) = \{x \mapsto \psi(t) \} \circ \psi$

Note: $$\{\, x \mapsto a \, \} \, \circ \, \{ \, y \mapsto b\,\} =
\{ \, y \mapsto (\,\{ \, x \mapsto a \, \} (b) \, \} \, \circ \, \{ \, x \mapsto a \, \}$$ if $y$ not
in $a$

\cite{CS421:Unif}.

\subsection{K Code}

The following is the K code.
\begin{lstlisting}
    //Unification

    syntax Map ::= uniFun(List) [function]
    syntax Bool ::= isVarType(K) [function]
    syntax Bool ::= notChildVar(K,K) [function]
    syntax KItem ::= uniPair(K,K)

    syntax List ::= uniSub(Map,K) [function] //apply substitution to unification

    syntax KItem ::= typeSub(Map,K) [function] //apply substitution to type
    syntax Map ::= compose(Map,Map) [function]

    rule uniFun(.List) => .Map //substi(.K,.K) is id substitution

    rule uniFun(ListItem(uniPair(S:K,S)) Rest:List) => uniFun(Rest)  //delete rule

    rule uniFun(ListItem(uniPair(S:K,T:K)) Rest:List) => uniFun(ListItem(uniPair(T,S)) Rest) //orient rule
         requires isVarType(T) andBool (notBool isVarType(S))

    rule uniFun(ListItem(uniPair(funtype(A:K, B:K), funtype(C:K, D:K))) Rest:List) => uniFun(ListItem(uniPair(A, C)) ListItem(uniPair(B, D)) Rest:List) //decompose rule function type

    rule uniFun(ListItem(uniPair(S:K,T:K)) Rest:List) 
      => compose((S |-> typeSub(uniFun(uniSub((S |-> T),Rest)),T)),uniFun(uniSub((S |-> T),Rest))) //eliminate rule
    //  => compose(uniFun(uniSub((S |-> T),Rest)),(S |-> typeSub(uniFun(uniSub((S |-> T),Rest)),T))) //eliminate rule
         requires isVarType(S) andBool notChildVar(S,T)

    rule isVarType(S:K) => true
         requires getKLabel(S) ==KLabel 'guessType
    rule isVarType(S:K) => false [owise]

    rule notChildVar(S:K,T:K) => true

    rule uniSub(Sigma:Map,.List) => .List
    rule uniSub(.Map,L:List) => L
    rule uniSub(Sigma:Map, Rest:List ListItem(uniPair(A:K, B:K))) => uniSub(Sigma, Rest) ListItem(uniPair(typeSub(Sigma, A), typeSub(Sigma, B)))

    rule typeSub(Sigma:Map (Tau |-> Newtau:KItem),Tau:KItem) => typeSub(Sigma (Tau |-> Newtau),Newtau)
    rule typeSub(Sigma:Map,funtype(Tauone:KItem,Tautwo:KItem)) => funtype(typeSub(Sigma,Tauone),typeSub(Sigma,Tautwo))
    rule typeSub(Sigma:Map,Tau:KItem) => Tau [owise]
\end{lstlisting}
\section{Composition of Substitutions}

Composition of substitutions means that if the composition was applied to a type, it would first apply to the rightmost substitution and then afterwards apply to the substitution to the left of it, and so on \cite{Infer:TypeSub}.

The following is a mathematical definition where $\theta$ and $\lambda$ are substitutions.

$$ \theta = [t_1 / x_1 , t_2 / x_2 , \cdots , t_n / x_n] $$

$$ \lambda = [s_1 / y_1 , s_2 / y_2 , \cdots , s_m / y_m] $$

$$ \lambda \circ \theta = [ \lambda(t_1) /x_1 , \lambda(t_2) / x_2, \cdots, \lambda(t_n) / x_n]$$

The following is the K Code.

\begin{lstlisting}
    syntax Map ::= composeIn(Map, Map, Map, K, K) [function]

    rule compose(Sigmaone:Map, Sigmatwo:Map) => composeIn(Sigmaone, Sigmatwo, .Map, .K, .K)

    rule composeIn(Sigmaone:Map, (Key:KItem |-> Type:KItem) Sigmatwo:Map, NewMap:Map, .K, .K) => composeIn(Sigmaone, Sigmatwo, NewMap, Key, Type)

    rule composeIn((Keyone |-> Typetwo:KItem) Sigmaone:Map, Sigmatwo:Map, NewMap:Map, Keyone:KItem, Typeone:KItem) => composeIn(Sigmaone, Sigmatwo, NewMap, Keyone, Typeone)

    rule composeIn((Typeone |-> Typetwo:KItem) Sigmaone:Map, Sigmatwo:Map, NewMap:Map, Keyone:KItem, Typeone:KItem) => composeIn((Typeone |-> Typetwo) Sigmaone, Sigmatwo, NewMap[Keyone <- Typetwo], .K, .K)
         requires notBool(Keyone in keys(Sigmaone))

    rule composeIn(Sigmaone:Map, Sigmatwo:Map, NewMap:Map, Keyone:KItem, Typeone:KItem) => composeIn(Sigmaone, Sigmatwo, NewMap[Keyone <- Typeone], .K, .K) [owise]

    rule composeIn(Sigmaone:Map, .Map, NewMap:Map, .K, .K) => Sigmaone NewMap
endmodule
\end{lstlisting}

\section{Example}

The following is an example inference:

The module called \texttt{Simp5} defined a data type called \texttt{CusBool} as

\begin{lstlisting}
data CusBool = True2 | False2
\end{lstlisting}

The data structures for this data type look as follows after running the semantics:

\begin{lstlisting}
    <tempBeta>
        ModPlusType ( Simp5 , False2 ) |-> forAll ( .Set , CusBool .TyVars )
        ModPlusType ( Simp5 , True2 ) |-> forAll ( .Set , CusBool .TyVars )
    </tempBeta>
    <tempT>
        TList ( ListItem ( TObject ( Simp5 , CusBool , .TyVars , 
            ListItem ( InnerTPiece ( True2 , .List , .List , True2 
              .OptBangATypes , CusBool ) )
            ListItem ( InnerTPiece ( False2 , .List , .List , False2 
              .OptBangATypes , CusBool ) ) ) ) )
    </tempT>
    <tempDelta>
        ModPlusType ( Simp5 , CusBool ) |-> 0
    </tempDelta>

\end{lstlisting}

In the module \texttt{Simp5} there is also an example declaration:

\begin{lstlisting}
\y -> (let {f = \x -> x y} in (f (\x -> Simp5.True2)))
\end{lstlisting}

After running the inference algorithm, the substitution generated for this declaration is as follows:

\begin{lstlisting}
    <k>
        mapBagResult ( 
            guessType ( 0 ) |-> funtype ( guessType ( 1 ) , CusBool .TyVars 
              )
            guessType ( 2 ) |-> CusBool .TyVars
            guessType ( 3 ) |-> funtype ( funtype ( guessType ( 1 ) , 
              guessType ( 5 ) ) , guessType ( 5 ) )
            guessType ( 4 ) |-> funtype ( guessType ( 6 ) , guessType ( 5 ) 
              )
            guessType ( 6 ) |-> guessType ( 1 )
            guessType ( 7 ) |-> funtype ( guessType ( 9 ) , guessType ( 8 ) 
              )
            guessType ( 8 ) |-> CusBool .TyVars
            guessType ( 9 ) |-> guessType ( 10 )
            guessType ( 11 ) |-> CusBool .TyVars ) ~> inferenceShell ( 
          .TopDecls )
    </k>
\end{lstlisting}

And the example expression is inferred as 

\begin{lstlisting}
funtype ( guessType ( 1 ) , CusBool .TyVars )
\end{lstlisting}

\noindent
which should be the case.