+ OCAML ANSWERS:
+
+ type 'a sysf_bool = 'a -> 'a -> 'a
+ let sysf_true : 'a sysf_bool = fun y n -> y
+ let sysf_false : 'a sysf_bool = fun y n -> n
+
+ type 'a sysf_nat = ('a -> 'a) -> 'a -> 'a
+ let sysf_zero : 'a sysf_nat = fun s z -> z
+
+ let sysf_iszero (n : ('a sysf_bool) sysf_nat) : 'a 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 get a polymorphic result you'll want to call `fun next -> sysf_succ sysf_zero next` *)
+
+ And here is how to get `sysf_pred`, using a System-F-style encoding of pairs. (For brevity, I'll leave off the `sysf_` prefixes.)
+
+ type 'a natpair = ('a nat -> 'a nat -> 'a nat) -> 'a nat
+ let natpair (x : 'a nat) (y : 'a nat) : 'a natpair = fun f -> f x y
+ let fst x y = x
+ let snd x y = y
+ let shift (p : 'a natpair) : 'a natpair = natpair (succ (p fst)) (p fst)
+ let pred (n : ('a natpair) nat) : 'a nat = n shift (natpair zero zero) snd
+
+ (* As before, to get polymorphic results you need to eta-expand your applications. Witness:
+ # let one = succ zero;;
+ val one : '_a nat = <fun>
+ # let one next = succ zero next;;
+ val one : ('a -> 'a) -> 'a -> 'a = <fun>
+ # let two = succ one;;
+ val two : '_a nat = <fun>
+ # let two next = succ one next;;
+ val two : ('a -> 'a) -> 'a -> 'a = <fun>
+ # pred two;;
+ - : '_a nat = <fun>
+ # fun next -> pred two next;;
+ - : ('a -> 'a) -> 'a -> 'a = <fun>
+ *)