Functional abstraction and instantiations

The goal of this lecture note is to illustrate the process of abstracting a computation with a function in OCaml, and to instantiate this abstracted computation by applying the corresponding function.

A concrete situation

Loki: Let’s play a game.

Dana: OK?

Loki: Can you write an OCaml function that adds 1 to its argument?

Dana: Sure:

let add_1 n =
  1 + n;;

Pablito: Should we write a unit-test function too? I mean first?

Loki: My, my. Do you see Mimer anywhere?

Pablito: Er, OK.

Loki: Can you write an OCaml function that adds 2 to its argument?

Pablito: Sure:

let add_2 n =
  2 + n;;

Loki: Can you write an OCaml function that adds 3 to its argument?

Anton: Sure:

let add_3 n =
  3 + n;;

Loki: Can you write an OCaml function that adds 4 to its argument?

Alfrothul: Sure:

let add_4 n =
  4 + n;;

Loki: Can you write an OCaml function that adds 5 to its argument?

First interlude

Alfrothul: There is a pattern here.

Anton: Right. The next thing Loki is going to ask is whether we can write an OCaml function that adds 6 to its argument.

Alfrothul: Which is the same elephant.

Anton: Hum.

Alfrothul: How about we parameterize this elephant?

Anton: Ah, as you did for the factorial numbers with their index to obtain a factorial function.

Alfrothul: Yup. Functional abstraction, here we come:

let add i n =
  i + n;;

Anton: He, he.

Alfrothul: Right. We have abstracted the varying part of the computation with a variable, namely the formal parameter of a function.

Anton: Functional instantiations, here we come:

let add_1 n =
  add 1 n;;

let add_2 n =
  add 2 n;;

let add_3 n =
  add 3 n;;

let add_4 n =
  add 4 n;;

Alfrothul: This is so cool.

Dana: Wait. These definitions can be simplified.

Anton: Simplified?

Dana: Well, yes – the only thing each of them does, given an argument, is to pass them to the result of applying add to a literal.

Alfrothul: How true:

let add_1 = add 1;;

let add_2 = add 2;;

let add_3 = add 3;;

let add_4 = add 4;;

Pablito: That’s a lot shorter.

Dana: Right – the index in each name is now the actual parameter of a call to add, which is the essence of functional abstraction and instantiations.

A concrete situation, continued (and abstracted)

Loki: So, guys, can you write an OCaml function that adds 5 to its argument?

Alfrothul: Sure:

let add_5 = add 5;;

Loki: I see. Can you write an OCaml function that multiplies its argument by 0?

Anton: Er, sure:

let mul_0 n =
  0;;

Loki: Clever. Can you write an OCaml function that multiplies its argument by 1?

Alfrothul: Sure:

let mul_1 n =
  n;;

Loki: Clever.

Second interlude

Alfrothul: Wait. The next thing Loki is going to ask is whether we can write an OCaml function that multiplies its argument by 2. And then by 3.

Anton: You mean we should anticipate? Right. It’s another same elephant, let’s parameterize it:

let mul i n =
  i * n;;

Pablito: And then let’s instantiate this function abstraction with 2 to obtain an OCaml function that multiplies its argument by 2:

let mul_2 n =
  mul 2 n;;

Pablito: By which I mean the simplified version:

let mul_2 = mul 2;;

Halcyon (happily): Ditto for 3:

let mul_3 = mul 3;;

Anton: I like my definition of mul_0, though. It exploits the property that 0 is absorbing for multiplication.

Alfrothul: Likewise for my definition of mul_1. It exploits the property that 1 is neutral for multiplication.

Anton: OK. This second interlude is about done here, let’s get back to Loki.

Dana: Wait. The next thing Loki is going to ask is whether we can write an OCaml function that, I don’t know, concatenates "a" to its argument. And then "b". And then "c".

Anton: That is likely.

Dana: And that would be a third same elephant.

Alfrothul: Hum. You mean to say that our same elephants are a same same elephant?

Anton: Hum.

Dana: We should parameterize our parameterized elephant into a generic one.

Pablito (fearlessly): Let’s. Functional abstraction, here we come:

let the_generic_elephant f i n =
  f i n;;

Anton: And functional instantiation, here we come:

let mul i n =
  the_generic_elephant ( * ) i n;;

Alfrothul: Ditto:

let add i n =
  the_generic_elephant (+) i n;;

Dana: Ditto too, at type string, even though the naming of the formal parameters is unintuitive:

let concat i n =
  the_generic_elephant (^) i n;;

A concrete situation, ended

Anton: Where is Loki?

Halcyon: He’s gone.

Postlude

Pablito: Er, guys?

The guys: Yes?

Pablito: Did you see the type of the_generic_elephant:

# let the_generic_elephant f i n = f i n;;
val the_generic_elephant : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = <fun>
#

Alfrothul: Déjà vu, right?

Dana: And déjà programmé, oui, I mean yes, in Exercise 08.e, back in Week 04.

Anton: Harrumph.

Post-postlude

Pablito: Er, guys?

The guys: Yes?

Pablito: I think we could simplify the definitions of add and mul. Look:

let add_simplified =
  the_generic_elephant (+);;

let mul_simplified =
  the_generic_elephant ( * );;

Anton: Harrumph. But you are right. The only thing add does, given two arguments, is to pass them to the_generic_elephant (+), so yes, we can simplify it, and likewise for mul as well as for concat:

let concat_simplified =
  the_generic_elephant (^);;

Dana: Hear me saying nothing about the intuitiveness of the formal parameters of concat_simplified.

Halcyon: Well, they’re gone, right?

Post-post-postlude

Pablito: Er, guys?

The guys: Yes?

Pablito: Actually, by that book, we can simplify the_generic_elephant too, can’t we?

Alfrothul: Well spotted, Pablito! Indeed we can:

let the_generic_elephant f =
  f;;

Anton: But its type?

Alfrothul: Well, its type has become the type of the identity function. In fact, the_generic_elephant implements the identity function.

Anton: Go figure.

Mimer: That is because OCaml computes the most general type of any term, and 'd -> 'd is more general than ('a -> 'b -> 'c) -> 'a -> 'b -> 'c, which is the type of the identity function over functions of type 'a -> 'b -> 'c.

Anton: Harrumph. But that makes sense, and -> does associate to the right.

Pablito: Exercise 19 in Week 04...

Alfrothul: Wait. So what would happen if we only simplified away the last argument of the_generic_elephant:

# let the_generic_elephant f i = f i;;
val the_generic_elephant : ('a -> 'b) -> 'a -> 'b = <fun>
#

Anton: Ah, it has the type of the identity function over functions of type 'a -> 'b. That makes sense too.

Dana: Déjà programmé, encore, I mean again, in the Interlude about functions applied to other functions, back in Week 04.

Halcyon (frowning): Is it because of the identity function that it is the same elephant?

Dana: Not necessarily. The same point applies to the parity predicates, i.e., evenp and oddp.

Pablito: What do you mean?

Dana: They only differ because of their base case.

Pablito: So?

Dana: So we can implement a generic version of parity predicates, one that is parameterized with the base case:

let make_parity_predicate zero_case n =
  let () = assert (n >= 0) in
  let rec visit i =
    if i = 0
    then zero_case
    else not (visit (pred i))
  in visit n;;

Pablito: Ah, I see:

let evenp = make_parity_predicate true;;

let oddp = make_parity_predicate false;;

Halcyon (diligent): These implementations pass the unit tests.

Mimer: The accompanying resource file also contains a generic version of traced parity predicates.

Post-post-post-postlude

Anton: Gesundheit.

Mimer: Thank you.

Dana: Wait. More déjà vu.

Loki: More déjà vu? This is getting to be nearly too much, ain’t it. When are we going to read about something new in these lecture notes?

Dana (doggedly): make_parity_predicate denotes a function with two arguments.

Alfrothul: That it does.

Dana: And we define evenp by applying this function to a first argument.

Alfrothul: Yes. We have abstracted the base case with the first parameter of make_parity_predicate.

Dana: But initially, in the section about the even predicate, we defined the even predicate with one argument.

Alfrothul (patiently): Yes, the second argument of make_parity_predicate, since it is a generalized version of the even predicate that is parameterized by its base case.

Dana: So conversely, the even predicate is a version of make_parity_predicate that is specialized with respect to its first argument.

Alfrothul (laughing): So a partial evaluator would map the definition of make_parity_predicate and true to the definition of the even predicate.

Dana: Yes, modulo the fact that make_parity_predicate denotes a curried function rather than an uncurried one, and therefore takes its arguments one at a time, not in a tuple.

Alfrothul (reflecting): So, generalization by parameterizing a function further and specialization by providing an argument for this further parameter.

Dana: Right, modulo the fact that a partial evaluator works on the program implementing the function, not on the function. The program is intensional, i.e., about the “how” of the computation, and the function is extensional, i.e., about the “what” of the computation.

Anton: Harrumph. Again.

Halcyon (worried): Not to interfere with your little Socratic dialogue here, but, huh, are we going to see even more déjà vu?

Mimer (sagely): In a piece of tissue made with one thread, we get to see the same thread times and again. The more so, the stronger the tissue.

Loki: Déjà vu as a source of foresight, I see.

Mimer (pragmatic): More like the more useful, the more reused.

Resources

• The OCaml code for the present lecture note (latest version: 16 Sep 2022).

Version

Created [16 Sep 2022]