Eta expansion eliminates an infinite recursion

Learning
1

Hi all,

I was trying to play around with these articles https://blog.sumtypeofway.com/posts/introduction-to-recursion-schemes.html that I discovered through this question : Attempting to create 'recursion schemes' in ocaml and I ran into an unexpected issue. I give you the entire code :

type 'a expr = LiteralF of int | UnaryF of 'a | BinaryF of 'a * 'a

let fmap f = function
  | LiteralF i -> LiteralF i
  | UnaryF e -> UnaryF (f e)
  | BinaryF (e1, e2) -> BinaryF (f e1, f e2)

module Term(F:sig type 'a t  val fmap: ('a -> 'b) -> 'a t -> 'b t end) = struct
  type 'a t = In of 'a t F.t

  let out = function In term -> term

  let in_ t = In t

  let (%>) f g x = g (f x)

  let rec bottomUp fn =
    out
    %>  F.fmap (bottomUp fn)
    %> in_
    %> fn

  let rec bottomUp_eta fn =
    out
    %> (fun x ->  F.fmap (bottomUp_eta fn) x)
    %> in_
    %> fn
end

module Expr  = Term(struct type 'a t = 'a expr  let fmap = fmap  end)
open Expr

let _ = bottomUp_eta Fun.id (in_ @@ LiteralF 1)
let () = print_endline "Passed test 1"
let _ = bottomUp Fun.id (in_ @@ LiteralF 1)
let () = print_endline "Passed test 2"

I took batteries included syntax for forward function composition.
The problem is that while the function bottomUp_eta works completely fine, bottomUp apparently triggers an infinite recursion (it ends up with a stack overflow), I am completely puzzled by this behaviour, I was aware that sometimes eta expansion could help type checking (by ruling out the possibility of a weird reference behaviour) but until now I thought that as soon as some code compiles, eta expanded version against standard one would not make any runtime difference. The only thing I could have imagined would be related to tail-call optimization (maybe easier in the eta-expanded version) but in this case the example is so trivial that I can’t imagine I would exhaust the stack this way.

Can anyone help me ? Thanks !

1 Like
2 
(* loops when called with a single parameter *)
let rec loop x = loop x

let () = loop () (* loops *)
let _ = loop (fun x -> x + 1) (* still loops *)

(* eta-expanded version *)
let rec loop_eta x = fun y -> loop_eta x y

let _ = loop_eta (fun x -> x + 1) (* does not loop anymore *)
2 Likes
3

Oh, is it because in the second case, as the compiler knows loop_eta x is supposed to be a function it doesn’t try to evaluate it further as it is still missing one argument ?

4

I was trying to play around with these articles adventures in uncertainty: An Introduction to Recursion Schemes

This very thing caught me out when I read this post a while back :slightly_smiling_face:

Oh, is it because in the second case, as the compiler knows loop_eta x is supposed to be a function it doesn’t try to evaluate it further as it is still missing one argument ?

Close. The evaluation doesn’t really depend on whether “loop_eta x is supposed to be a function”, but whether it reduces to a value or not. In both cases, the code behaves the same way: expressions are reduced until they are values.

  • Function applications are not values: they must be reduced to values by first reducing their arguments, applying the function, and continuing to evaluate from there. When evaluating loop (fun x -> x + 1), (fun x -> x + 1) is already a value, so the function is applied causing the body of loop to be reduced. This requires evaluating loop (fun x -> x + 1) again and so the evaluation never terminates.

  • Lambdas are values: the body of the lambda is reduced only when it is applied. Evaluating loop_eta (fun x -> x + 1) again involves applying the function (the argument is still a value). The difference is that the body of loop_eta doesn’t need to be reduced: it’s already the lambda value fun y -> loop_eta x y. So we’re done. (If you pass two arguments to loop_eta, it’s a different story.)

In short, eta-expansion in OCaml delays the evaluation of the expression you’re expanding around. If your code never applies the eta-expanded term, the body will never be reduced. This is important when either (a) there are side-effects associated with the reduction or (b) the reduction is non-terminating (as is the case for your code above).

The Haskell code relies on the fact that fmap will eventually not need its first argument (for the ground terms in the algebra). In Haskell, this is enough, since the first argument is evaluated lazily (only when it is required). In OCaml, you need to ensure that the recursive call doesn’t happen until fmap actually needs it, which you can do by eta-expanding.

  let rec bottomUp fn =
    out
    %> F.fmap (fun x -> bottomUp fn x)
    %> in_
    %> fn

As you’ve seen, it also works to eta-expand around the fmap. In this case, the code will make one more recursive call for ground terms, but since fmap never actually applies the function constructed by that recursive call there is no more work to do.

2 Likes