types.tex

\section{Thursday morning - Types}


These exercises are about \emph{types} in Haskell. In a nutshell, the type of an expression tells you what sort of value an expression eventually evaluates to. Not all expressions can be typed! If an expression cannot be reduced to a normal form, such as \haskellIn{not 7}, then it does not have a type and the compiler will refuse to compile the program. We use the following notation to say that an expression \texttt{\small expression} has type \texttt{\small type} -- this is referred to as a \emph{typing}:
\begin{center}
	\begin{tabular}{lcl}
		\texttt{\small expression} & \texttt{\small ::} & \texttt{\small type}
	\end{tabular}
\end{center}
Some examples of typings are:
\begin{minted}{haskell}
True                       :: Bool
'a'                        :: Char 
\x -> x                    :: a -> a
\x -> False                :: a -> Bool 
\x -> \y -> y              :: a -> b -> b
if 5 > 6 then 'a' else 'b' :: Char 
42                         :: Num a => a
4 + 8 * 15 - 16            :: Num a => a
(\x -> x) True             :: Bool
\end{minted}
As you can see, the size or complexity of a term does not necessarily correspond to that of a type. It only matters what an expression evaluates to. Some expressions have multiple permissible types. For example, the expression \haskellIn{42} could have type \haskellIn{Int} (the type of signed integers where the precision depends on your platform), \haskellIn{Integer} (the type of arbitrary precision integers), \haskellIn{Num a => a} (a polymorphic type \haskellIn{a} constrained to all numeric types by the constraint \haskellIn{Num a}), as well as others.

If an expression can be typed, the Haskell compiler can \emph{infer} the \emph{most general} type for us. For example, for numbers such as \haskellIn{42}, the \haskellIn{Int} type is permissible, but \haskellIn{Num a => a} is a more general type. ``More general'' generally means ``more polymorphic''. There is a command in the REPL which we can use to ask for the type of an expression:
\begin{center}
\begin{tabular}{|l|l|}
	\hline 
	\texttt{\small :t EXPRESSION}   & Shows the type of \texttt{\small EXPRESSION}. \\ 
	\hline 
\end{tabular}  
\end{center}

\taskLine

\task{Launch the REPL with \texttt{\small stack repl} (or \texttt{\small ghci} if you are using replit) and try it for yourself by asking for the types of the following expressions with the \texttt{\small :t} command:}
\begin{itemize}
	\item \haskellIn{'a'}
	\item \haskellIn{[True, True, False]}
	\item \haskellIn{[1,2,3,4,5]}
	\item \haskellIn{[]}
	\item \haskellIn{\x -> x}
	\item \haskellIn{1+1}
\end{itemize}

\task{Since the Haskell compiler always infers the most general type for an expression, you may sometimes want to validate whether a less general type is also permissible. You can annotate expressions with typings for that purpose and get the Haskell compiler to validate your annotations. For example, try to ask for the types of the following three expressions:}
\begin{itemize}
	\item \haskellIn{108}
	\item \haskellIn{(108 :: Int)}
	\item \haskellIn{(True :: Int)}
\end{itemize}
As you can see, you get the most general type for \haskellIn{108}. For \haskellIn{(108 :: Int)}, the compiler validates that \haskellIn{Int} is indeed a permissible type for \haskellIn{108}. For the last expression, we get a type error since \haskellIn{Int} is not a permissible type for \haskellIn{True}.

\taskLine

\task{Some expressions cannot be reduced to values and therefore do not have a type. Try asking for the types of the following expressions. Each expression will result in the type error which is explained below:} 
\begin{itemize}
\item \haskellIn{not 7} \\
As mentioned in the lecture, the literal \haskellIn{7} has the most general type \haskellIn{Num a => a}. The Haskell compiler also knows that the \haskellIn{not} function has type \haskellIn{Bool -> Bool} so it expects its argument to be of type \haskellIn{Bool}. Because \haskellIn{Bool} is less polymorphic than \haskellIn{a}, the Haskell compiler deduces that \haskellIn{7} should be of type \haskellIn{Bool}. However, this results in a constraint of \haskellIn{Num Bool} which cannot be resolved because there is no instance of \haskellIn{Num} for the \haskellIn{Bool} type.
\item \haskellIn{[1,True,3]} \\
This results in the same error.
\item \haskellIn{['a', False]} \\
Lists in Haskell are \emph{homogeneous}. That is, they can only contain elements which have the same type. Neither \haskellIn{'a'} nor \haskellIn{False} have a polymorphic type and both have different types. Therefore, the Haskell compiler will tell you that the two types do not match.
\end{itemize}

\taskLine

If you are working on your own machine, open Visual Studio Code and open the \texttt{\small lab-types} folder you have extracted from the \texttt{thursday.zip} archive (File > Add folder to workspace) and then open a terminal window inside of Visual Studio Code (Terminal > New Terminal) which should appear at the bottom. 

If you are using replit, copy the contents of \texttt{\small lab-types/src/Lab.hs} into the editor there.

A fairly simple example of an algebraic data type is the following:
\begin{minted}{haskell}
data IntPos = IntPos Int Int
\end{minted}
This type, named \haskellIn{IntPos}, has a single constructor, also named \haskellIn{IntPos} with two parameters of type \haskellIn{Int}. The purpose of this type is to represent 2-dimensional positions.

\task{What is the type of the \haskellIn{IntPos} constructor? Use the REPL and \texttt{\small :t IntPos} to check your answer.}

\task{It would be useful to test whether two values of type \haskellIn{IntPos} are the same. Complete the instance of the \haskellIn{Eq} type class for \haskellIn{IntPos}. Ensure that your implementation is correct by checking that both tests for it pass.}

\task{It would also be useful to be able to turn values of type \haskellIn{IntPos} into corresponding \haskellIn{String} representations so that we can show them in the REPL. Complete the \haskellIn{Show} instance for \haskellIn{IntPos}. For example:}
\begin{minted}{haskell}
*Lab Lab> show (IntPos 4 15)
"IntPos 4 15"
\end{minted}

\task{Complete the definition of \haskellIn{zeroPos}, which should represent the position where both coordinates are 0.}

\task{Complete the definitions of the \haskellIn{x} and \haskellIn{y} functions, which should extract the first and second coordinate from an \haskellIn{IntPos} value, respectively. For example:}
\begin{minted}{haskell}
*Lab Lab> y (IntPos 4 15)
15
\end{minted} 

\taskLine 

Often it is useful to define types as generically as possible. While our \haskellIn{IntPos} type is fine if we only ever want to represent positions using integer coordinates, we would have to duplicate a lot of code if we ever wanted to \emph{e.g.} represent positions using floating point numbers as coordinates.
\begin{minted}{haskell}
data Pos a = Pos a a 
\end{minted}

\task{What is the type of the \haskellIn{Pos} constructor? Use the REPL and \texttt{\small :t Pos} to check your answer.}

\task{It would be useful to test whether two values of type \haskellIn{Pos} are the same. Complete the instance of the \haskellIn{Eq} type class for \haskellIn{Pos}. Ensure that your implementation is correct by checking that both tests for it pass.}

\task{It would also be useful to be able to turn values of type \haskellIn{Pos} into corresponding \haskellIn{String} representations so that we can show them in the REPL. Complete the \haskellIn{Show} instance for \haskellIn{Pos}. For example:}
\begin{minted}{haskell}
*Lab Lab> show (Pos 4.2 15.16)
"Pos 4.2 15.16"
\end{minted}

\task{Complete the definition of \haskellIn{zero}, which should represent the position where both coordinates are 0.}

\task{Complete the definitions of the \haskellIn{left} and \haskellIn{top} functions, which should extract the first and second coordinate from an \haskellIn{Pos} value, respectively. For example:}
\begin{minted}{haskell}
*Lab Lab> top (Pos 4.2 15.16)
15.16
\end{minted} 
Ensure that the tests for \haskellIn{left} and \haskellIn{top} succeed before proceeding.

\task{The Haskell compiler can construct \emph{projection functions} like \haskellIn{left} and \haskellIn{top} which extract individual components from a data constructor automatically. Remove the definitions of \haskellIn{left} and \haskellIn{top} and change the definition of \haskellIn{Pos} to:}
\begin{minted}{haskell}
data Pos a = Pos { left :: a, top :: a } 
\end{minted}

\taskLine

\task{It is important to remember that there are virtually no restrictions on the types of things that we can store in data constructors or that type variables can be instantiated with. For example, the following is a valid use of the \haskellIn{Pos} type we defined:}
\begin{minted}{haskell}
*Lab Lab> :t Pos (\x -> True) odd
Pos (\x -> True) odd :: Integral p => Pos (p -> Bool)
\end{minted}
\emph{I.e.} functions can be stored inside of data constructors. To practice this, we have defined the following data type:
\begin{minted}{haskell}
data DocumentItem = ListItem (Int -> String)

doc :: [DocumentItem]
doc = 
  [ ListItem (\n -> show n ++ ". An item")
  , ListItem (\n -> concat ["I am item #", show n])
  , ListItem (\n -> concat ["There. Are. ", show n, ". Items." ])
  ]
\end{minted}
What is the type of \haskellIn{ListItem}? Verify your answer in the REPL.

\task{Complete the definition of the \haskellIn{render} function so that it produces the results shown below. The idea is that \haskellIn{render} goes through a list of \haskellIn{DocumentItem} values and calls the functions contained in the \haskellIn{ListItem} constructors with the current value of a counter (the second argument to \haskellIn{render}) that should be incremented for each recursive call:}
\begin{minted}{haskell}
*Lab Lab> render [] 1
""

*Lab Lab> render (tail doc) 2
"I am item #2\nThere. Are. 3. Items.\n"

*Lab Lab> render doc 1
"1. An item\nI am item #2\nThere. Are. 3. Items.\n"
\end{minted}