Assignment 3 – Term and typelevel recursion
The GitHub Classrooms link for this assignment is here
The deadline for the assignment is 20230301 @ 23:59. The deadline for the peer reviews is 20220308 @ 23:59.
Exercise 1 – Termlevel fixpoints (2 pts)

Given the function
fix :: (a > a) > a fix f = f (fix f)
Define the function
foldr
as an application offix
to a term that is not recursive. 
The lambda term which corresponds to the Ycombinator in untyped lambda calculus
y = \f > (\x > f (x x)) (\x > f (x x))
does not type check in Haskell. Try it and explain the error message you get.
Interestingly though, recursion on the type level can be used to introduce recursion on the value level. If we define the recursive type:
data F a = F { unF :: F a > a }
then we can “annotate” the definition of
y
with applications ofF
andunF
such thaty
typechecks. Do it!NOTE: Attempting to optimise this function will cause GHC’s simplifier to diverge. Sometimes you can avoid this by adding
{# OPTIONS_GHC fmaxsimplifieriterations=1 #}
to the top of the file.
Exercise 2 – Nested types (4 pts)
Here is a nested data type for square matrices:
type Square = Square' Nil  note that it is etareduced
data Square' t a = Zero (t (t a))  Succ (Square' (Cons t) a)
data Nil a = Nil
data Cons t a = Cons a (t a)
Question 1. Give Haskell code that represents the following two square matrices as elements of the Square
data type:
Let’s investigate how we can derive an equality function on square matrices. We do so very systematically by deriving an equality function for each of the four types. We follow a simple, yet powerful principle: type abstraction corresponds to term abstraction, and type application corresponds to term application.
What does this mean? If a type f
is parameterized over an argument a
, then in general, we have to know how equality is defined on a
in order to define equality on f a
. Therefore we define
eqNil :: (a > a > Bool) > (Nil a > Nil a > Bool)
eqNil eqA Nil Nil = True
In this case, the a
is not used in the definition of Nil
, so it is not surprising that we do not use eqA
in the definition of eqNil
. But what about Cons
? The data type Cons
has two arguments t
and a
, so we expect two arguments to be passed to eqCons
, something like
eqCons eqT eqA (Cons x xs) (Cons y ys) = eqA x y && ...
But what should the type of eqT
be? The t
is of kind * > *
, so it can’t be t > t > Bool
. We can argue that we should use t a > t a > Bool
, because we use t
applied to a
in the definition of Cons
. However, a better solution is to recognise that, being a type constructor of kind * > *
, an equality function on t
should take an equality function on its argument as a parameter. And, moreover, it does not matter what this parameter is! A function like eqNil
is polymorphic in type a
, so let us require that eqT
is polymorphic in the argument type as well:
eqCons :: (forall b . (b > b > Bool) > (t b > t b > Bool))
> (a > a > Bool)
> (Cons t a > Cons t a > Bool)
eqCons eqT eqA (Cons x xs) (Cons y ys) = eqA x y && eqT eqA xs ys
Now you can see how we apply eqT
to eqA
when we want equality at type t a
– the type application corresponds to term application.
Question 2. A type with a forall
on the inside requires the extension RankNTypes
to be enabled. Try to understand what the difference is between a function of the type of eqCons
and a function with the same type but the forall
omitted. Can you omit the forall
in the case of eqCons
and does the function still work?
Now, on to Square'
. The type of eqSquare'
follows exactly the same idea as the type of eqCons
:
eqSquare' :: (forall b . (b > b > Bool) > (t b > t b > Bool))
> (a > a > Bool)
> (Square' t a > Square' t a > Bool)
We now for the first time have more than one constructor, so we actually have to give multiple cases. Let us first consider comparing two applications of Zero
:
eqSquare' eqT eqA (Zero xs) (Zero ys) = eqT (eqT eqA) xs ys
Note how again the structure of the definition follows the structure of the type. We have a value of type t (t a)
. We compare it using eqT
, passing it an equality function for values of type t a
. How? By using eqT eqA
. The remaining cases are as follows:
eqSquare' eqT eqA (Succ xs) (Succ ys) = eqSquare' (eqCons eqT) eqA xs ys
eqSquare' eqT eqA _ _ = False
The idea is the same – let the structure of the recursive calls follow the structure of the type.
Question 3. Again, try removing the forall
from the type of eqSquare'
. Does the function still
type check? Try to explain!
Now we’re done:
eqSquare :: (a > a > Bool) > Square a > Square a > Bool
eqSquare = eqSquare' eqNil
Test the function. We can now also give an Eq
instance for Square
– this requires the minor language extension TypeSynonymInstances
, because Haskell 98 does not allow type synonyms like Square
to be used in instance declarations:
instance Eq a => Eq (Square a) where
(==) = eqSquare (==)
Question 4. Systematically follow the scheme just presented in order to define a Functor
instance for square matrices. I.e., derive a function mapSquare
such that you can define
instance Functor Square where
fmap = mapSquare
This instance requires Square
to be defined in etareduced form in the beginning, because Haskell does not allow partially applied type synonyms. If we had defined Square
differently
type Square a = Square' Nil a
we cannot make Square
an instance of the class Functor
.
Question 5. Why is this restriction in place? Try to find problems arising from partially applied type synonyms, and describe them (as concisely as possible) with a few examples.
Exercise 3 – Teletype IO (4 pts)
Consider the following data type:
data Teletype a = End a
 Get (Char > Teletype a)
 Put Char (Teletype a)
A value of type Teletype
can be used to describe programs that read and write characters and return a final result of type a
. Such a program can end immediately (End
). If it reads a character, the rest of the program is described as a function depending on this character (Get
). If the program writes a character (Put
), the value to show and the rest of the program are recorded.
For example, the following expression describes a program that continuously echo characters:
echo = Get (\c > Put c echo)
Question 1. Write a Teletype
program getLine
which reads characters until it finds a newline character, and returns the complete string.
A map function for Teletype
can be defined as follows:
instance Functor Teletype where
fmap f (End x) = End (f x)
fmap f (Get g) = Get (fmap f . g)
fmap f (Put c x) = Put c (fmap f x)
Question 2. Define sensible Applicative
and Monad
instances for Teletype
.
The definition of Teletype
is not directly compatible with do
notation. Usually, you have getChar
and putChar
primitives which allow you to write instead:
echo = do c < getChar
putChar c
echo
Question 3. Define those functions getChar :: Teletype Char
and putChar :: Char > Teletype ()
.
Question 4. Define a MonadState
instance for Teletype
. How is the behavior of this instance different from the usual State
type?
Question 5. A Teletype
program can be thought as a description of an interaction with the console. Write a function runConsole :: Teletype a > IO a
which runs a Teletype
program in the IO
monad. A Get
should read a character from the console and Put
should write a character to the console.
One of the advantages of separating the description of Teletype
programs from their executions is that we can interpret them in different ways. For example, the communication might take place throught a network instead of console. Or we could mock user input and output for testing purposes.
Question 6. Write an interpretation of a Teletype
program into the monad RWS [Char] () [Char]
(documentation). In other words, write a function,
type TeletypeRW = RWS [Char] () [Char]
runRWS :: Teletype a > TeletypeRW a
Using it, write a function mockConsole :: Teletype a > [Char] > (a, [Char])
.