\input{../settings/settings}
\newcommand\tab[1][5mm]{\hspace*{#1}}

\begin{document}

	\klausur{Nichtprozedurale Programmierung}
	 		{Prof. M. Mendler}
	    	{Wintersemester 16/17}
	   		{90}
	    	{Wörterbuch}
	
	\begin{enumerate}
		\item 
		Let us implement a simple game of Hangman. In this game, the player has to guess letters of a word, and the correctly guessed letters are displayed are displayed in the position where they occur in the word.
		
		We will use values of type {\tt String} for two purposes: To encode the word that has to be guessed, and the characters that have already been guessed.
		
		Recall that the type {\tt String} is the same as {\tt [Char]}, the type of lists of characters. This enables you to use all functions that generically operate on lists, such as
		
		\begin{center}
			{\tt elem :: Eq a $\Rightarrow$ a $\rightarrow$ [a] $\rightarrow$ Bool}
		\end{center}
	
		which takes an element of type {\tt a}, a list containing elements of the same type, and returns a {\tt Bool} which tells you whether the element is contained in the list or not.
	
		\begin{enumerate}
			\item 
			Implement the following function:
			\begin{center}
				{\tt onlyGuessedChar :: String $\rightarrow$ Char $\rightarrow$ Char}
			\end{center}
			It checks whether the given string contains the given character, and if yes, returns the character unchanged, if no, returns '\_' (an underscore).\\
			For example:
			\begin{center}
				{\tt onlyGuessedChar \textquotedbl\textquotedbl \ 'a' == '\_'\\
					onlyGuessedChar \textquotedbl xyz\textquotedbl \ 'x' == 'x'\\
					onlyGuessedChar \textquotedbl DEFGH\textquotedbl \ 'd' == '\_'
				}
			\end{center}
			(Note: Lower- and uppercase letters count as different letters.)\par
			
			\item
			Implement the following function:
			\begin{center}
				{\tt onlyGuessed :: String $\rightarrow$ String $\rightarrow$ String}
			\end{center}
			It takes as first argument the letters that have already been guessed and as second argument the word that has to be guessed. It returns the second word, in which all letters that haven't been guessed yet (given as the characters in the first string) are replaced by the character '\_'.\\
			For example:
			\begin{center}
				{\tt onlyGuessed \textquotedbl abcde\textquotedbl \ \textquotedbl Haskell\textquotedbl \ == "\_a\_\_e\_\_"\\
					onlyGuessed \textquotedbl ePnoX\textquotedbl \ \textquotedbl NPP\textquotedbl \ == \textquotedbl\_PP \textquotedbl
				}
			\end{center}
			You may use functions from the standard library and reuse the functions defined in the previous sub-problem, if  you find this useful.\par
			
			\item 
			Define a datatype {\tt Hangman} that contains the word which the player has to guess as a {\tt String}, and the letters that the player has already guessed, without modification. (You can also use record-syntax for this part.)
			\pagebreak
			
			\item
			Recall the {\tt State} monad:\\
			\texttt{
				data State s a = State (s $\rightarrow$ (s, a))\\
				instance Monad (State s) where\\
				\tab return a = State \$ \textbackslash s $\rightarrow$ (s, a)\\
				\tab State aState $>>=$ f = State \$ \textbackslash s $\rightarrow$\\
				\tab \tab let (s', a) = aState s\\
				\tab \tab \tab State g = f a\\
				\tab \tab in g s'	
			}\\
		
			A value in the {\tt State} monad can depend on an internal state of type s, and can modify the state when computed.\\
			Here are some simple values in the state monad that read and write the internal state:\\
			
			{\tt \tab get :: State s s\\
				\tab get = State \$ \textbackslash s $\rightarrow$ (s, s)\\
				\\
				\tab put :: s $\rightarrow$ State s ()\\
				\tab put s = State \$ \textbackslash \_ $\rightarrow$ (s, ())
			}\\

			Using your previously defined datatype {\tt Hangman} and the functions {\tt get} and {\tt put}. {\bf Implement the following three functions:}
			\begin{itemize}
				\item 
				{\tt newGuessword :: String $\rightarrow$ State Hangman ()}\\
				should update the state such that the new guessword is the given argument, and the list of already guessed characters is empty.
				\item 
				{\tt guessLetter :: Char $\rightarrow$ State Hangman ()}\\
				should add the given character to the list of guessed characters.
				\item 
				{\tt onlyGuessedState :: State Hangman String}\\
				should return the guessword in which all characters that haven't been guessed yet are replaced by underscores. Reuse your function {\tt onlyGuessed} from before.
			\end{itemize}
		
			You can use do-notation, or the binding operators.
			
			\begin{center}
				{\tt $>>=$ :: State s a $\rightarrow$ (a $\rightarrow$ State s b) $\rightarrow$ State s b\\
					$>>$ :: State s a $\rightarrow$ State s b $\rightarrow$ State s b
				}
			\end{center}
		
			For testing a {\tt State} program, the following function is given:
			
			\begin{center}
				{\tt runState :: State s a $\rightarrow$ s $\rightarrow$ (s, a)\\
					runState (State f) = f s
				}
			\end{center}
		
			For example, evaluating the following expression
			
			{\tt > runState\\
				\tab (newGuessword \textquotedbl NPP\textquotedbl \ $>>$ guessLetter 'N' $>>$ onlyGuessedState)\\
				\tab (Hangman \textquotedbl Haskell\textquotedbl \ \textquotedbl is great\textquotedbl)
			}

			must yield the result:
			
			{\tt $\Longrightarrow$ (Hangman \textquotedbl N\textquotedbl \ \textquotedbl NPP\textquotedbl , \textquotedbl N\_\_\textquotedbl ).}
			
			If, in any part of the question, you aren't able to implement a function, you can go on and solve the later questions, even if they would require your earlier solutions. Just assume you had already implemented the missing functions.
			
		\end{enumerate}
		
		\item
		\begin{enumerate}
			\item
			Recall that in the $\lambda$-calculus the Church Boolean constants for True and False can be coded as follows:
			
			\begin{center}
				{\tt tt =\textsubscript{df} $\lambda t.\lambda f.t$\\
					ff =\textsubscript{df} $\lambda t.\lambda f.f$
				}
			\end{center}
		
			Equality comparison of Church Booleans is implemented by the following term:
			
			\begin{center}
				{\tt $eq$ =\textsubscript{df} $\lambda a.\lambda b. a b (b$ ff tt$)$}
			\end{center}
		
			Verify by $\beta$-reduction that $eq$ {\tt ff ff} reduces to {\tt tt}, {\bf using eager evaluation.}
			
			\item
			Recall that the first three Church Numeral constants are:
			
			\begin{center}
				{\tt \underline{0} = $\lambda s.\lambda z. z$\\
					\underline{1} = $\lambda s.\lambda z. s z$\\
					\underline{2} = $\lambda s.\lambda z. s (s z)$
				}
			\end{center}
		
			Find a $\lambda$-term {\tt pos} that takes a Church Numeral as argument and tests whether it is nonzero. For example, {\tt pos 0} must $\beta$-reduce to {\tt ff}, and {\tt pos 1} must reduce to {\tt tt}.
			
			Verify your solution by reducing {\tt pos 0} and {\tt pos 2} to normal form in {\bf lazy evaluation}.
		
			Hint: Your solution should look like {\tt pose =\textsubscript{df} $\lambda n.n ?_1 ?_2$}, and for $?_1$ and $?_2$ you need to insert the correct $\lambda$-terms. You may use Church Booleans if you find this useful.
			
		\end{enumerate}
	
		\item
		Consider the following F2-expression $e$:
		
		\begin{center}
		{\tt $e$ =\textsubscript{df} fn $x$ $\Rightarrow$ let $pair$ = fn $y$ $\Rightarrow \langle x,y\rangle$ end in $pair$ 5 end end
		}
		\end{center}
	
		\begin{enumerate}
			\item
			Show that {\tt $[(x,\alpha)]\vdash$ fn $y$ $\Rightarrow \langle x,y\rangle$ end : $\beta \rightarrow \alpha * \beta$ using the polymorphic F2 typing rules, given in the appendix.}
			
			\item
			Show that there exists a polytype $\tau$ such that $[ ] \vdash e : \tau$ using the polymorphic F2 typing rules. You can reuse your derivation in the previous question part a).
		\end{enumerate}
		
	\end{enumerate}
\end{document}