From 2a7b99413dbcdb336e57c222f79e2ce85ddbb9f8 Mon Sep 17 00:00:00 2001 From: jim Date: Sat, 21 Mar 2015 08:56:50 -0400 Subject: [PATCH] add some more --- exercises/assignment5_answers.mdwn | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/exercises/assignment5_answers.mdwn b/exercises/assignment5_answers.mdwn index b591330b..9c30527e 100644 --- a/exercises/assignment5_answers.mdwn +++ b/exercises/assignment5_answers.mdwn @@ -667,7 +667,20 @@ Do these last three problems specifically with OCaml in mind, not Haskell. Analo 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: -- 2.11.0