add some stuff

diff --git a/exercises/assignment5_answers.mdwn b/exercises/assignment5_answers.mdwn
index 2b29695..b591330 100644 (file)
--- a/exercises/assignment5_answers.mdwn
+++ b/exercises/assignment5_answers.mdwn
@@ -546,11 +546,6 @@ any type `α`, as long as your function is of type `α -> α` and you have a bas
     It's especially useful for you to implement a version of a System F encoding `pred`, starting with one of the (untyped) versions available in [[assignment3 answers]].
 
 
     It's especially useful for you to implement a version of a System F encoding `pred`, starting with one of the (untyped) versions available in [[assignment3 answers]].
 
 

-
------
-`sysf_bool`, `sysf_true`, `sysf_false`,
-`sysf_nat`, `sysf_zero`, `sysf_iszero`, `sysf_succ`, and `sysf_pred`.
-

     OCAML ANSWERS:
 
         type ('a) sysf_bool = 'a -> 'a -> 'a
     OCAML ANSWERS:
 
         type ('a) sysf_bool = 'a -> 'a -> 'a


@@ -559,13 +554,29 @@ any type `α`, as long as your function is of type `α -> α` and you have a bas
 
         type ('a) sysf_nat = ('a -> 'a) -> 'a -> 'a
         let sysf_zero : ('a) sysf_nat = fun s z -> z
 
         type ('a) sysf_nat = ('a -> 'a) -> 'a -> 'a
         let sysf_zero : ('a) sysf_nat = fun s z -> z

+

         let sysf_iszero (n : 'a sysf_nat) : 'b sysf_bool = n (fun _ -> sysf_false) sysf_true
         (* Annoyingly, though, if you just say sysf_iszero sysf_zero, you'll get an answer that isn't fully polymorphic.
            This is explained in the comments linked below. The way to get a polymorphic result is to say instead
            `fun next -> sysf_iszero sysf_zero next`. *)
         let sysf_iszero (n : 'a sysf_nat) : 'b sysf_bool = n (fun _ -> sysf_false) sysf_true
         (* Annoyingly, though, if you just say sysf_iszero sysf_zero, you'll get an answer that isn't fully polymorphic.
            This is explained in the comments linked below. The way to get a polymorphic result is to say instead
            `fun next -> sysf_iszero sysf_zero next`. *)

+

         let sysf_succ (n : 'a sysf_nat) : 'a sysf_nat = fun s z -> s (n s z)
         (* Again, to use this you'll want to call `fun next -> sysf_succ sysf_zero next` *)
         let sysf_succ (n : 'a sysf_nat) : 'a sysf_nat = fun s z -> s (n s z)
         (* Again, to use this you'll want to call `fun next -> sysf_succ sysf_zero next` *)

-        let sysf_pred (n : 'a sysf_nat) : 'a sysf_nat = (* LEFT UNDONE *)
+
+        let sysf_pred (n : 'a sysf_nat) : 'a sysf_nat = (* NOT DONE *)
+
+<!--
+        (* Using a System F-style encoding of pairs, rather than native OCaml pairs ... *)
+          let pair a b = fun f -> f a b in
+          let snd x y next = y next in
+          let shift p next = p (fun x y -> pair (sysf_succ x) x) next in (* eta-expanded as in previous definitions *)
+          fun next -> n shift (pair sysf_zero sysf_zero) snd next
+
+    let pair = \a b. \f. f a b in
+    let snd = \x y. y in
+    let shift = \p. p (\x y. pair (succ x) x) in
+    let pred = \n. n shift (pair 0 err) snd in
+-->

 
 
 Consider the following list type, specified using OCaml or Haskell datatypes:
 
 
 Consider the following list type, specified using OCaml or Haskell datatypes: