Curried function defined in terms of its own partial application

Question

The following SML code is taken from a homework assignment from a course at University of Washington. (Specifically it is part of the code provided so that students could use it to complete Homework 3 listed on the course webpage.) I am not asking for homework help here–I think I understand what the code is saying. What I don't quite understand is how a curried function is allowed to be defined in terms of its own partial application.

 datatype pattern = 
     WildcardP
   | VariableP of string
   | UnitP
   | ConstantP of int
   | ConstructorP of string * pattern
   | TupleP of pattern list

fun g f1 f2 p =
  let 
    val r = g f1 f2      (* Why does this not cause an infinite loop? *)
  in
    case p of
        WildcardP         => f1 ()
      | VariableP x       => f2 x
      | ConstructorP(_,p) => r p
      | TupleP ps         => List.foldl (fn (p,i) => (r p) + i) 0 ps
      | _                 => 0
  end

The function binding is a recursive definition that makes use of the recursive structure in the datatype binding for pattern. But when we get to the line val r = g f1 f2, why doesn't that cause the execution to think, "wait, what is g f1 f2? That's what I get by passing f2 to the function created by passing f1 to g. So let's go back to the definition of g" and enter an infinite loop?

Answer 1

With lambda calculus abstraction, the curried function g is g = (^f1. (^f2. (^p. ...body...))) and so

g a b = (^f1. (^f2. (^p. ...body...))) a      b 
      =       (^f2. (^p. ...body...)) [a/f1] 
      =             (^p. ...body...)  [a/f1] [b/f2]

Partial application just produces the inner lambda function paired with the two parameters bindings closed over -- without entering the body at all.

So defining r = g f1 f2 is just as if defining it as the lambda function, r = (^p. g f1 f2 p) (this, again, is LC-based, so doesn't deal with any of the SML-specific stuff, like types).

And defining a lambda function (a closure) is just a constant-time operation, it doesn't enter the g function body, so there is no looping at all, let alone infinite looping.