OCaml Haskell ========================================================== ========================================================= type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show) let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I)) reduce_one_step :: Term -> Term let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of FA(I,a) -> a FA I a -> a | FA(FA(K,a),b) -> a FA (FA K a) b -> a | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c) | _ -> t _ -> t is_redex :: Term -> Bool let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t) reduce2 :: Term -> Term let rec reduce2 (t:term):term = match t with reduce2 t = case t of I -> I I -> I | K -> K K -> K | S -> S S -> S | FA (a, b) -> FA a b -> let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t') else t' else t'There are some differences in the way types are made explicit, and in the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for Haskell). But the two programs are essentially identical. Yet the Haskell program finds the normal form for `KIΩ`: *Main> reduce2 (FA (FA K I) skomega) I Woa! First of all, this is wierd. Haskell's evaluation strategy is called "lazy". Apparently, Haskell is so lazy that even after we've asked it to construct t' by evaluating `reduce2 a` and `reduce2 b`, it doesn't bother computing `reduce2 b`. Instead, it waits to see if we ever really need to use the result. So the program as written does NOT fully determine evaluation order behavior. At this stage, we have defined an evaluation order that still depends on the evaluation order of the underlying interpreter. There are two questions we could ask: Can we adjust the OCaml evaluator to exhibit lazy behavior? and Can we adjust the Haskell evaluator to exhibit eager behavior? The answer to the first question is easy and interesting, and we'll give it right away. The answer to the second question is also interesting, but not easy. There are various tricks available in Haskell we could use (such as the `seq` operator), but a fully general, satisifying resolution will have to wait until we have Continuation Passing Style transforms. The answer to the first question (Can we adjust the OCaml evaluator to exhibit lazy behavior?) is quite simple:

let rec reduce3 (t:term):term = match t with I -> I | K -> K | S -> S | FA (a, b) -> let t' = FA (reduce3 a, b) in if (is_redex t') then reduce3 (reduce_one_step t') else t'There is only one small difference: instead of setting `t'` to `FA (reduce a, reduce b)`, we omit one of the recursive calls, and have `FA (reduce a, b)`. That is, we don't evaluate the right-hand subexpression at all. Ever! The only way to get evaluated is to somehow get into functor position. # reduce3 (FA(FA(K,I),skomega));; - : term = I # reduce3 skomega;; C-c C-cInterrupted. The evaluator now has no trouble finding the normal form for `KIΩ`, but evaluating skomega still gives an infinite loop. As a final note, we can clarify the larger question at the heart of this discussion: *How can we can we specify the evaluation order of a computational system in a way that is completely insensitive to the evaluation order of the specification language?*