From 1c184042007c8578ddabcc5590d372b1e469cb91 Mon Sep 17 00:00:00 2001
From: jim <jim@web>
Date: Sun, 1 Mar 2015 16:54:02 -0500
Subject: [PATCH] tweak types for list encoding

---
 exercises/_assignment5.mdwn | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/exercises/_assignment5.mdwn b/exercises/_assignment5.mdwn
index e081c671..7765a7e7 100644
--- a/exercises/_assignment5.mdwn
+++ b/exercises/_assignment5.mdwn
@@ -351,10 +351,10 @@ any type `α`, as long as your function is of type `α -> α` and you have a bas
 Consider the following list type, specified using OCaml or Haskell datatypes:
 
     (* OCaml *)
-    type ('a) my_list = Nil | Cons of 'a * 'a my_list
+    type ('t) my_list = Nil | Cons of 't * 't my_list
 
      -- Haskell
-     data My_list a = Nil | Cons a (My_list a)  deriving (Show)
+     data My_list t = Nil | Cons t (My_list t)  deriving (Show)
 
 We can encode that type into System F in terms of its right-fold, just as we did in the untyped Lambda Calculus, like this:
 
@@ -364,27 +364,27 @@ We can encode that type into System F in terms of its right-fold, just as we did
 
 As with `Nat`s, the natural recursion on the type is built into our encoding of it.
 
-There is some awkwardness here, because System F doesn't have any parameterized types like OCaml's `('a) list` or Haskell's `[a]`. For those, we need to use a more complex system called System F<sub>ω</sub>. System F *can* already define a more polymorphic list type:
+There is some awkwardness here, because System F doesn't have any parameterized types like OCaml's `('t) my_list` or Haskell's `My_list t`. For those, we need to use a more complex system called System F<sub>ω</sub>. System F *can* already define a more polymorphic list type:
 
-    list ≡ ∀β. ∀α. (β -> α -> α) -> α -> α
+    list ≡ ∀τ. ∀α. (τ -> α -> α) -> α -> α
 
 But this is more awkward to work with, because for functions like `map` we want to give them not just the type:
 
-    (S -> T) -> list -> list
+    (T -> S) -> list -> list
 
 but more specifically, the type:
 
-    (S -> T) -> list [S] -> list [T]
+    (T -> S) -> list [T] -> list [S]
 
 Yet we haven't given ourselves the capacity to talk about `list [S]` and so on as a type in System F. Hence, I'll just use the more clumsy, ad hoc specification of `map`'s type as:
 
-    (S -> T) -> list_S -> list_T
+    (T -> S) -> list_T -> list_S
 
 <!--
-    = λf:S -> T. λxs:list. xs [S] [list [T]] (λx:S. λys:list [T]. cons [T] (f x) ys) (nil [T])
+    = λf:T -> S. λxs:list. xs [T] [list [S]] (λx:T. λys:list [S]. cons [S] (f x) ys) (nil [S])
 -->
 
-19. Convert this list encoding and the `map` function to OCaml or Haskell. Again, call the type `sysf_list`, and the functions `sysf_nil`, `sysf_cons`, and `sysf_map`, to avoid collision with the names for native lists and functions in these languages. (In OCaml and Haskell you *can* say `('a) sysf_list` or `Sysf_list a`.)
+19. Convert this list encoding and the `map` function to OCaml or Haskell. Again, call the type `sysf_list`, and the functions `sysf_nil`, `sysf_cons`, and `sysf_map`, to avoid collision with the names for native lists and functions in these languages. (In OCaml and Haskell you *can* say `('t) sysf_list` or `Sysf_list t`.)
 
 20. Also give us the type and definition for a `sysf_head` function. Think about what value to give back if its argument is the empty list. It might be cleanest to use the `option`/`Maybe` technique explored in questions 1--2, but for this assignment, just pick a strategy, no matter how clunky. 
 
-- 
2.11.0