checks.tex

\chapter{Context-Sensitive Checks}
The standard Haskell Compiler is called the Glasgow Haskell Compiler \cite{GHC}. It is otherwise known as GHC. By testing GHC, it is apparent that the compiler will check and reject programs that are syntactically valid, but have additional issues that make the programs invalid. This means that GHC does in fact make additional context-sensitive checks that are not part of the context free grammar. In the semantics in this paper, there are also context-sensitive checks that are made prior to type inference to reject programs that GHC rejects.

\section{Data Types}
Within the context of a computer program, a data type is a property of data that tells the compiler or interpreter more about how the data is supposed to be used within the context of the program. This is useful for having the compiler find bugs that occur from the programmer misusing data \cite{Foldoc:Type}.
In Haskell, a user can create a custom data type. This is referred to as a user-defined type. Then when the user creates functions or any other expression, they can operate on their own data type.

\subsection{Polymorphim}
A polymorphic data type is a data type that can generalize over other data types.
A monomorphic data type is a data type that does not do this.

\section{Datatype Constructors}

In order to perform context-sensitive checks to make sure that the user did not have errors when creating types, the types are placed into data structures that make context-sensitive checks easy to perform.

Section 4 of the Haskell 2010 report \cite{Report:Report} specifies the Haskell type system.

In the \texttt{TopDecl} sort, there are three type constructors that are used to create user-defined data types. These are \texttt{data}, \texttt{type}, and \texttt{newtype}.

\begin{lstlisting}
    syntax TopDecl ::= Decl [klabel('topdecldecl)]
                     > "type" SimpleType "=" Type [klabel('type)]
                     | "data" OptContext SimpleType OptConstrs OptDeriving  [klabel('data)]
                     | "newtype" OptContext SimpleType "=" NewConstr OptDeriving [klabel('newtype)]
\end{lstlisting}

These three type constructors are used to create user-defined types.

\subsection{Type}
The first one is \texttt{type},
	\begin{lstlisting}
type simpletype = type 
	\end{lstlisting}
This is used in a Haskell program to declare a new type as a single type. In effect, it renames the type where both names now can be used to refer to the type.
	\begin{lstlisting}
type Username = String
	\end{lstlisting}
Is one such example usage of \texttt{type}, it creates a new type \texttt{Username}, which is defined as just a string. Now the programmer can refer to \texttt{Username} or \texttt{String} to make a string.

\subsection{Data}
The second one is \texttt{data},
\begin{lstlisting}
data [context =>] simpletype [= constrs] [deriving]
\end{lstlisting}
This allows a user to declare a new type that may include many fields and polymorphic types.

For instance:
\begin{lstlisting}
data Date = Date Int Int Int
\end{lstlisting}
This is a new type that includes the type constructor \texttt{Date} followed by three integers.
\begin{lstlisting}
data Poly a = Number a
\end{lstlisting}
This is a new polymorphic type with polymorphic parameter a, that has the type constructor $Number$.

\subsection{Newtype}
The third one is \texttt{newtype},
\begin{lstlisting}
newtype [context =>] simpletype = newconstr [deriving]
\end{lstlisting}
This is very similar to data except it only parses when the newtype has only one typecon and one field.

\subsection{Context}
Another thing to note is that the
\begin{lstlisting}
[context =>]
\end{lstlisting}
part of the syntax for the types is deprecated \cite{Stack:Depre}.

\section{Initial Data Structures}

The semantics includes a map, called alpha, of new type names as the keys and their declared types as the entries. It collects all appearances of the type constructor \texttt{type} in the program, and puts \texttt{simpletype $\mapsto$ type} in the alpha map. However, one of the checks that is made, is whether a user declared multiple definitions with texttt{type}, but maps in K only allow for unique keys. So initially the semantics creates a set of tuples, and after checking for multiple type declarations, it then changes the alpha set to a map.


The second data structure that the semantics creates is called T. T holds the user-defined types created using \texttt{data} and \texttt{newtype}.

\begin{lstlisting}
syntax KItem ::= TList(K) //list of T objects for every new type introduced by data and newtype
syntax KItem ::= TObject(K,K,K,K) //(module name, type name, entire list of poly type vars, list of inner T pieces)
syntax KItem ::= InnerTPiece(K,K,K,K,K) //(type constructor, poly type vars, argument sorts, entire constr block, type name)
\end{lstlisting}

The structure, \texttt{T}, is a list of TObjects. Each TObject represents a single user-defined datatype. It holds the name, the list of polymorphic parameters, and a list of inner T pieces.
An inner T piece represents an option of what a type could be. It consists of a type constructor, a list of polymorphic parameters required for this option, the fields for this option, the entire subtree of the AST for this option unedited, and the type name again.
The semantics then uses these data structures to perform these checks, and afterwards uses different data structures to perform type inference.

\subsection{Example T}

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

\noindent
then the corresponding \texttt{tempT} should look like this.
\begin{lstlisting}
    <tempT>
        TList ( ListItem ( TObject ( Simp5 , CusBool , .TyVars , 
            ListItem ( InnerTPiece ( True2 , .List , .List , True2 
              .OptBangATypes , CusBool ) )
            ListItem ( InnerTPiece ( False2 , .List , .List , False2 
              .OptBangATypes , CusBool ) ) ) ) )
    </tempT>
\end{lstlisting}

\subsection{K Code}
The following parses the tree and searches for the user-defined types to place into the data structures.

\begin{lstlisting}
    //get alpha and beta
    syntax KItem ::= Module(K, K)
    syntax KItem ::= preModule(K,K) //(alpha, T)

    // STEP 1 CONSTRUCT T AND ALPHA
    // alpha = type
    // T = newtype and data, temporary data structure

    syntax KItem ::= initPreModule(K) [function]
    syntax KItem ::= getPreModule(K, K) [function] //(Current term, premodule)
    syntax KItem ::= makeT (K,K,K,K)

    syntax KItem ::= fetchTypes (K,K,K,K)

    syntax List ::= makeInnerT (K,K,K) [function] //LIST
    syntax List ::= getTypeVars(K) [function] //LIST

    syntax KItem ::= getCon(K) [function]
    syntax List ::= getArgSorts(K) [function] //LIST

    syntax KItem ::= AList(K)
    syntax KItem ::= AObject(K,K) //(1st -> 2nd) map without idempotency
    syntax KItem ::= ModPlusType(K,K)

    syntax KItem ::= TList(K) //list of T objects for every new type introduced by data and newtype
    syntax KItem ::= TObject(K,K,K,K) //(module name, type name, entire list of poly type vars, list of inner T pieces)
    syntax KItem ::= InnerTPiece(K,K,K,K,K) //(type constructor, poly type vars, argument sorts, entire constr block, type name)

    rule initPreModule(J:K) => getPreModule(J,preModule(AList(.List),TList(.List)))

    rule getPreModule('bodytopdecls(I:K), J:K) => getPreModule(I,J)
    rule getPreModule('topdeclslist('type(A:K,, B:K),, Rest:K),J:K) => fetchTypes(A,B,Rest,J) //constructalpha


    rule getPreModule('topdeclslist('data(A:K,, B:K,, C:K,, D:K),, Rest:K),J:K) => makeT(B,C,Rest,J)
    rule getPreModule('topdeclslist('newtype(A:K,, B:K,, C:K,, D:K),, Rest:K),J:K) => makeT(B,C,Rest,J)


    rule getPreModule('topdeclslist('topdecldecl(A:K),, Rest:K),J:K) => getPreModule(Rest,J)
    rule getPreModule('topdeclslist('class(A:K,, B:K,, C:K,, D:K),, Rest:K),J:K) => getPreModule(Rest,J)
    rule getPreModule('topdeclslist('instance(A:K,, B:K,, C:K,, D:K),, Rest:K),J:K) => getPreModule(Rest,J)
    rule getPreModule('topdeclslist('default(A:K,, B:K,, C:K,, D:K),, Rest:K),J:K) => getPreModule(Rest,J)
    rule getPreModule('topdeclslist('foreign(A:K,, B:K,, C:K,, D:K),, Rest:K),J:K) => getPreModule(Rest,J)
    rule getPreModule(.TopDecls,J:K) => J

    rule <k> fetchTypes('simpleTypeCon(I:TyCon,, H:TyVars), 'atypeGTyCon(C:K), Rest:K, preModule(AList(M:List), L:K)) => getPreModule(Rest,preModule(AList(ListItem(AObject(ModPlusType(ModName,I),C)) M), L)) ...</k>
         <tempModule> ModName:KItem </tempModule>

    rule <k> makeT('simpleTypeCon(I:TyCon,, H:TyVars), D:K, Rest:K, preModule(AList(M:List), TList(ListInside:List))) => getPreModule(Rest,preModule(AList(M),TList(ListItem(TObject(ModName,I,H,makeInnerT(I,H,D))) ListInside))) ...</k>
         <tempModule> ModName:KItem </tempModule>

    rule makeInnerT(A:K,B:K,'nonemptyConstrs(C:K)) => makeInnerT(A,B,C)
    rule makeInnerT(A:K,B:K,'singleConstr(C:K)) => ListItem(InnerTPiece(getCon(C),getTypeVars(C),getArgSorts(C),C,A))
    rule makeInnerT(A:K,B:K,'multConstr(C:K,, D:K)) => ListItem(InnerTPiece(getCon(C),getTypeVars(C),getArgSorts(C),C,A)) makeInnerT(A,B,D)

    rule getTypeVars('constrCon(A:K,, B:K)) => getTypeVars(B)
    rule getTypeVars('optBangATypes(A:K,, Rest:K)) => getTypeVars(A) getTypeVars(Rest)
    rule getTypeVars('optBangAType('emptyBang(.KList),, Rest:K)) => getTypeVars(Rest)
    rule getTypeVars('atypeGTyCon(A:K)) => .List
    rule getTypeVars('atypeTyVar(A:K)) => ListItem(A)
    rule getTypeVars(.OptBangATypes) => .List

    rule getCon('constrCon(A:K,, B:K)) => A

    rule getArgSorts('constrCon(A:K,, B:K)) => getArgSorts(B)
    rule getArgSorts('optBangATypes(A:K,, Rest:K)) => getArgSorts(A) getArgSorts(Rest)
    rule getArgSorts('optBangAType('emptyBang(.KList),, Rest:K)) => getArgSorts(Rest)
    rule getArgSorts('atypeGTyCon(A:K)) => ListItem(A)
    rule getArgSorts('atypeTyVar(A:K)) => .List
    rule getArgSorts(.OptBangATypes) => .List
\end{lstlisting}

\section{context-sensitive Checks}
For the context-sensitive checks, the semantics performs several checks that are not inclusive to all context-sensitive checks that need to be made in a complete Haskell semantics, but enough for some sanity of the type inference function.

\subsubsection{K Code}
The following code introduces all checks that need to be made.

\begin{lstlisting}
    // STEP 2 PERFORM CHECKS

    syntax KItem ::= "error"

    syntax KItem ::= "startChecks"
    syntax KItem ::= "checkNoSameKey"
        //Keys of alpha and keys of T should be unique
    syntax KItem ::= "checkTypeConsDontCollide"
        //Make sure typeconstructors do not collide in T
    syntax KItem ::= "makeAlphaMap"
        //make map for alpha
    syntax KItem ::= "checkAlphaNoLoops"
        //alpha check for no loops
        //check alpha to make sure that everything points to a T
    syntax KItem ::= "checkArgSortsAreTargets"
           //Make sure argument sorts [U] [W,V] are in the set of keys of alpha and targets of T, (keys of T)
    syntax KItem ::= "checkParUsed"
//NEED TO CHECK all the polymorphic parameters from right appear on left. RIGHT SIDE ONLY
//NEED TO CHECK UNIQUENESS FOR POLY PARAM ON LEFT SIDE ONLY

    rule <k> startChecks
             => checkNoSameKey
                ~> (checkTypeConsDontCollide
                ~> (makeAlphaMap
                ~> (checkAlphaNoLoops
                ~> (checkArgSortsAreTargets
                ~> (checkParUsed))))) ...</k>

\end{lstlisting}

\subsection{Name Collision}
The programmer should not be able to make two user-defined datatypes with the same name, even if one is created using the constructor \texttt{data} and another is created using the constructor \texttt{type} for instance.

The following example should not be allowed.
\begin{lstlisting}
data Date = Date Int
;type Date = Contwo Int
\end{lstlisting}

\subsubsection{K Code}
The following is the code for the check.
\begin{lstlisting}
    rule <k> checkTypeConsDontCollide
             => tyConCollCheck(T,.List,.Set) ...</k>
         <tempT> T:K </tempT>

    syntax KItem ::= tyConCollCheck(K,K,K) [function] //(TList,List of Tycons,Set of Tycons) 
    syntax KItem ::= lengthCheck(K,K) [function]

    rule tyConCollCheck(TList(ListItem(TObject(ModName:K, A:K,B:K,ListItem(InnerTPiece(Ty:K,E:K,F:K,H:K,G:K)) Inners:List)) Rest:List),J:List,D:Set) => 
                    tyConCollCheck(TList(ListItem(TObject(ModName,A,B,Inners)) Rest),ListItem(Ty) J, SetItem(Ty) D)
    rule tyConCollCheck(TList(ListItem(TObject(ModName:K, A:K,B:K,.List)) Rest:List),J:List,D:Set) => 
                    tyConCollCheck(TList(Rest),J,D)
    rule tyConCollCheck(TList(.List),J:List,D:Set) => 
                    lengthCheck(size(J),size(D))

    rule lengthCheck(A:Int, B:Int) => .K
                    requires A ==Int B

    rule lengthCheck(A:Int, B:Int) => error
                    requires A =/=Int B
\end{lstlisting}

\subsection{Type Constructor Collision}
The programmer should not be able to use the same type constructors when making different options for their types or use the same type constructors for different types.

The following example should not be allowed.
\begin{lstlisting}
data Date = Date Int | Date Bool
\end{lstlisting}

The following example should also not be allowed.
\begin{lstlisting}
data Date = Date Int
;data Datetwo = Date Int
\end{lstlisting}

\subsubsection{K Code}
The following is the code for the check.

\begin{lstlisting}
    syntax KItem ::= keyCheck(K,K,K,K) [function] //(Alpha, T, List of names, Set of names)

    rule <k> checkNoSameKey
             => keyCheck(A, T, .Set, .List) ...</k>
         <tempAlpha> A:K </tempAlpha>
         <tempT> T:K </tempT>

    rule keyCheck(AList(ListItem(AObject(A:K,B:K)) C:List), T:K, D:Set, G:List) => keyCheck(AList(C), T, SetItem(A) D, ListItem(A) G)
    rule keyCheck(AList(.List), TList(ListItem(TObject(ModName:K, A:K,B:K,C:K)) Rest:List), D:Set, G:List) => keyCheck(AList(.List), TList(Rest), SetItem(A) D, ListItem(A) G)
    rule keyCheck(AList(.List), TList(.List), D:Set, G:List) => lengthCheck(size(G),size(D))


    syntax KItem ::= makeAlphaM(K,K) [function] //(Alpha, AlphaMap)
    syntax KItem ::= tAlphaMap(K) //(AlphaMap) temp alphamap

    rule <k> makeAlphaMap
             => makeAlphaM(A, .Map) ...</k>
         <tempAlpha> A:K </tempAlpha>

    rule makeAlphaM(AList(ListItem(AObject(A:K,B:K)) C:List), M:Map) => makeAlphaM(AList(C), M[A <- B])
    rule makeAlphaM(AList(.List), M:Map) => tAlphaMap(M)

    rule <k> tAlphaMap(M:K) => .K ...</k>
         <tempAlphaMap> OldAlphaMap:K => M </tempAlphaMap>
\end{lstlisting}

\subsection{Alpha Cycle Check}
There should be no cycles in type renaming using \texttt{type}, and the type renaming chains using \texttt{type} should terminate with a type defined with \texttt{data} or \texttt{newtype}.

The following example should not be allowed.
\begin{lstlisting}
type Birthday = Date
;type Date = Birthday
\end{lstlisting}

The following example should also not be allowed if Date is not defined anywhere.
\begin{lstlisting}
type Birthday = Date
\end{lstlisting}

\subsubsection{K Code}
The following is the code for the check.

\begin{lstlisting}
    syntax KItem ::= aloopCheck(K,K,K,K,K,K,K) [function] //(Alpha,List of Alpha,Set of Alpha,CurrNode,lengthcheck,T,BigSet)

    rule <k> checkAlphaNoLoops
             => aloopCheck(A,.List,.Set,.K,.K,T,.Set) ...</k>
         <tempAlphaMap> A:K </tempAlphaMap>
         <tempT> T:K </tempT>

    //aloopCheck set and list to check cycles
    rule aloopCheck(Alpha:Map (A:KItem |-> B:KItem), D:List, G:Set, .K, .K,T:K,S:Set) => aloopCheck(Alpha, ListItem(B) ListItem(A) D, SetItem(B) SetItem(A) G, B, .K,T,S)
    rule aloopCheck(Alpha:Map (H |-> B:KItem), D:List, G:Set, H:KItem, .K,T:K,S:Set) => aloopCheck(Alpha, ListItem(B) D, SetItem(B) G, B, .K,T,S)

    rule aloopCheck(Alpha:Map, D:List, G:Set, H:KItem, .K,T:K,S:Set) => aloopCheck(Alpha, .List, .Set, .K, lengthCheck(size(G),size(D)),T,G S) //type rename loop ERROR
         requires (notBool H in keys(Alpha)) andBool (H in typeSet(T, .Set) orBool H in S) 

    rule aloopCheck(Alpha:Map, D:List, G:Set, H:KItem, .K,T:K,S:Set) => error //terminal alpha rename is not in T ERROR
         requires (notBool H in keys(Alpha)) andBool (notBool (H in typeSet(T, .Set) orBool H in S))


    syntax Set ::= typeSet(K,K) [function] //(K, KSet)
    rule typeSet(TList(ListItem(TObject(ModName:K, A:K,B:K,C:K)) Rest:List), D:Set) => typeSet(TList(Rest), SetItem(A) D)
    rule typeSet(TList(.List), D:Set) => D

    rule aloopCheck(.Map, .List, .Set, .K, .K,T:K, S:Set) => .K
\end{lstlisting}

\subsection{Argument Sort Check}
The argument sorts for types defined using the \texttt{data} keyword or the \texttt{newtype} keyword should be types that exist.

The following example should not be allowed if \texttt{Date} is not defined anywhere.
\begin{lstlisting}
Data Birthday = Birthday Date
\end{lstlisting}

\subsubsection{K Code}
The following is the code for the check.

\begin{lstlisting}
//Make sure argument sorts [U] [W,V] are in the set of keys of alpha and targets of T, (keys of T)

    syntax KItem ::= argSortCheck(K,K,K) [function] //(T,AlphaMap)

    rule <k> checkArgSortsAreTargets
             => argSortCheck(T,A,typeSet(T,.Set)) ...</k>
         <tempAlphaMap> A:K </tempAlphaMap>
         <tempT> T:K </tempT>
    
    rule argSortCheck(TList(ListItem(TObject(ModName:K, A:K,B:K,ListItem(InnerTPiece(C:K,D:K,ListItem(Arg:KItem) ArgsRest:List,E:K,F:K)) InnerRest:List)) TListRest:List),AlphaMap:Map,Tset:Set) => argSortCheck(TList(ListItem(TObject(ModName,A,B,ListItem(InnerTPiece(C,D,ArgsRest,E,F)) InnerRest)) TListRest),AlphaMap,Tset)
         requires ((Arg in keys(AlphaMap)) orBool (Arg in Tset))

    rule argSortCheck(TList(ListItem(TObject(ModName:K,A:K,B:K,ListItem(InnerTPiece(C:K,D:K,ListItem(Arg:KItem) ArgsRest:List,E:K,F:K)) InnerRest:List)) TListRest:List),AlphaMap:Map,Tset:Set) => error
         requires (notBool ((Arg in keys(AlphaMap)) orBool (Arg in Tset)))

    rule argSortCheck(TList(ListItem(TObject(ModName:K,A:K,B:K,ListItem(InnerTPiece(C:K,D:K,.List,E:K,F:K)) InnerRest:List)) TListRest:List),AlphaMap:Map,Tset:Set) => argSortCheck(TList(ListItem(TObject(ModName,A,B,InnerRest)) TListRest),AlphaMap,Tset)

    rule argSortCheck(TList(ListItem(TObject(ModName:K,A:K,B:K,.List)) TListRest:List),AlphaMap:Map,Tset:Set) => argSortCheck(TList(TListRest),AlphaMap,Tset)

    rule argSortCheck(TList(.List),AlphaMap:Map,Tset:Set) => .K
\end{lstlisting}

\subsection{Polymorphic Parameter Check}

The polymorphic parameters that appear on the right-hand side of a \texttt{data} declaration need to appear on the left-hand side as well.

The following example should not be allowed.
\begin{lstlisting}
Data Newtype = New a b
\end{lstlisting}

Also, The polymorphic parameters that appear on the left-hand side of a \texttt{data} declaration need to be unique. However, the parameters that appear on the right-hand side do not need to be unique.

The following example should not be allowed.
\begin{lstlisting}
Data Newtype a a = New a
\end{lstlisting}

However, the following example should be allowed.
\begin{lstlisting}
Data Newtype a = New a a
\end{lstlisting}

\subsubsection{K Code}
The following is the code for the check.

\begin{lstlisting}
//NEED TO CHECK all the polymorphic parameters from right appear on left. RIGHT SIDE ONLY
//NEED TO CHECK UNIQUENESS FOR POLY PARAM ON LEFT SIDE ONLY

    syntax KItem ::= parCheck(K,K) [function] //(T,AlphaMap)
    syntax KItem ::= makeTyVarList(K,K,K) [function] //(TyVars, NewList)
    syntax KItem ::= lengthRet(K,K,K) [function]

    rule <k> checkParUsed
             => parCheck(T,.K) ...</k>
         <tempT> T:K </tempT>

    rule parCheck(TList(ListItem(TObject(ModName:K,A:K,B:K,C:K)) Rest:List),.K) => parCheck(TList(ListItem(TObject(ModName,A:K,B:K,C:K)) Rest:List),makeTyVarList(B,.List,.Set))

    rule parCheck(TList(ListItem(TObject(ModName:K,A:K,B:K,ListItem(InnerTPiece(C:K,ListItem(Par:KItem) ParRest:List,D:K,E:K,F:K)) InnerRest:List)) Rest:List),NewSet:Set) =>
         parCheck(TList(ListItem(TObject(ModName,A,B,ListItem(InnerTPiece(C,ParRest,D,E,F)) InnerRest)) Rest),NewSet)
            requires Par in NewSet

    rule parCheck(TList(ListItem(TObject(ModName:K,A:K,B:K,ListItem(InnerTPiece(C:K,ListItem(Par:KItem) ParRest:List,D:K,E:K,F:K)) InnerRest:List)) Rest:List),NewSet:Set) => error
            requires notBool (Par in NewSet)

    rule parCheck(TList(ListItem(TObject(ModName:K,A:K,B:K,ListItem(InnerTPiece(C:K,.List,D:K,E:K,F:K)) InnerRest:List)) Rest:List),NewSet:Set) =>
         parCheck(TList(ListItem(TObject(ModName,A,B,InnerRest)) Rest),NewSet)

    rule parCheck(TList(ListItem(TObject(ModName:K,A:K,B:K,.List)) Rest:List),NewSet:Set) =>
         parCheck(TList(Rest),NewSet)

    rule parCheck(TList(.List),NewSet:Set) => .K

    rule makeTyVarList('typeVars(A:K,,Rest:K),NewList:List,NewSet:Set) => makeTyVarList(Rest, ListItem(A) NewList, SetItem(A) NewSet)

    rule makeTyVarList(.TyVars,NewList:List,NewSet:Set) => lengthRet(size(NewList),size(NewSet),NewSet)

    rule lengthRet(A:Int, B:Int, C:K) => C
                    requires A ==Int B

    rule lengthRet(A:Int, B:Int, C:K) => error
                    requires A =/=Int B
\end{lstlisting}