Submission instructions:

Submit a single (Text/Haskell) file.

------------------------------------------------------------------------------------------


1. Consider the counter counterADT example on slide 4 of the lecture notes on existential types.

Rewrite the example using universal types, using the encoding on slide 7 and 8.

You can do this either in the formal System F notation, or you can write a little Haskell
program using Rank-N types. In the latter case the type applications are implicit.

------------------------------------------------------------------------------------------

2. (You don't need to submit this one; this is just a simple "sanity check")

Make sure you understand the difference between the type-level expressions
forall X. X-> X and lambda X. X -> X.

Why doesn't an arrow type like Nat -> Nat have an arrow kind like * => * ?
------------------------------------------------------------------------------------------

3. In F_omega, the universe of kinds can be separated into kind _levels_ as follows:

K(1) = {}
K(i+1) = {*} U { J => K | J in K(i) and K in K(i+1) }

For example, * => * is in K(3), K(4) etc. but not in K(2).

Corresponding to these levels, F_omega can be divided into sublanguages F_i, where
the language F_i only permits kinds from kind level K(i).

In this terminology, the simply-typed LC is F_1, and System F is F_2.

Your task is to write a useful program that can be written in F_4 but not in F_3.