Submission instructions:

Submit a single Haskell file.

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


1. In the lecture you have seen Church encodings of booleans and numerals in
System F. GHC supports System F-like universal types as described here:
http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#universal-quantification

To use this feature you need to add the directive

{-# OPTIONS_GHC -XRankNTypes #-}

to your Haskell file.

Test the encodings from the lecture in Haskell [you don't need to submit this]

The basic idea of Church encoding is to represent a data type as its own "fold" function.

For example, the algebraic data type for lists

data List a = Nil | Cons a (List a)

can be Church-encoded as:

nil c n = n
cons h t c n = c h (t c n)

Here are two functions that compute the length of a Church-encoded list,
and append all strings in a Church-encoded list, respectively:

lngth l = l (\_ n -> n+1) 0
append l = l (\s xs -> s ++ xs) ""

For example, evaluating 'append ( cons "ab" (cons "cd" nil) )' yields "abcd".

However, this function, which uses both functions just defined, does not pass the type-checker:

appendandlength l = (lngth l, append l)

Your first task is to fix the program by adding corresponding type annotations (don't
touch the program itself, only add types).

Now think about how you can Church-encode other algebraic data types using
universal (rank-n) types.

Your second task is the following: Church-encode the algebraic data
type for AE expressions from our first lecture:

(define-type AE
  [num (n number?)]
  [plus (lhs AE?) (rhs AE?)]
  [minus (lhs AE?) (rhs AE?)])

and write an evaluator based on this representation.

That is, your program should look like this:

type AE = ...

num :: Int -> AE
num = ...
plus :: AE -> AE -> AE
plus = ...
minus :: AE -> AE -> AE
minus = ...

eval :: AE -> Int
eval = ...

As usual, add some test cases!

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

If you are adventurous (this is optional), you can revisit the "final encoding" of
Handin 7 and try to Church-encode the AST of this language. By doing so, the meaning
of a program is no longer fixed (as in the final encoding of Handin 7), but you can
parameterize it with any denotational semantics you like (which includes "trivial"
semantics like a pretty printer - but they'll all be compositional by construction!).

If you want to be considered for a PhD position :-) (this is optional, too) think about
how to combine Church-Encoding with HOAS as described in Handin 4. For example, try to
Church-encode the following data type and write a corresponding evaluator based on your
representation:

data Expr =
  Num Int |
  App Expr Expr |
  Lam (Expr -> Expr)

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

2. Prove the following theorems by providing terms with the corresponding (via Curry-Howard)
types in Haskell. The following formulas are all implicitly universally quantified over a,b,c etc.
Hint: Use the build-in data type "Either" for disjunctions.

- a /\ a -> a
- (a -> b -> c) -> b -> a -> c
- (a -> b) -> a
- (a -> b -> a) -> a -> [b] -> a
- ((((a /\ b) -> f) ->  ((a -> f) \/ (b -> f))) -> f) -> f

*After* you have solved the exercise, you may want to google for "Djinn"