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
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_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:
g. let rec f () = f () in f f
h. let rec f () = f () in f ()
- ANSWER: All are well-typed except for b, e, and g, which involve self-application. d and h are well-typed but enter an infinite loop. Surprisingly, OCaml's type-checker accepts c, and it too enters an infinite loop. Not sure how to explain why OCaml's type-checker accepts that.
+ ANSWER: All are well-typed except for b, e, and g, which involve self-application. d and h are well-typed but enter an infinite loop. Surprisingly, OCaml's type-checker accepts c, and it too enters an infinite loop.
+
+ OCaml is not in principle opposed to self-application: `let id x = x in id id` works fine. Neither is it in principle opposed to recursive/infinite types. But it demands that they not be infinite chains of unbroken arrows. There have to be some intervening datatype constructors. Thus this is an acceptable type definition:
+
+ type 'a ok = Cons of ('a -> 'a ok)
+
+ But this is not:
+
+ type 'a notok = 'a -> 'a notok
+
+ (In the technical jargon, OCaml has isorecursive not equirecursive types.) In any case, the reason that OCaml rejects b, e, and g is not the mere fact that they involve self-application, but the fact that typing them would require constructing one of the kinds of infinite chains of unbroken arrows that OCaml forbids. In case c, we can already see that the type of `f` is acceptable (it was ok in case a), and the self-application doesn't impose any new typing constraints because it never returns, so it can have any result type at all.
+
+ In case g, the typing fails not specifically because of a self-application, but because OCaml has already determined that `f` has to take a `()` argument, and even before settling on `f`'s final type, one thing it knows about `f` is that it isn't `()`. So `let rec f () = f () in f f` fails for the same reason that `let rec f () = f () in f id` would.
+
24. Throughout this problem, assume that we have: