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.

Brynja: OK?

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

Brynja: Sure:

let add_1 n =
  1 + n;;

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

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

Vigfus: Er, OK.

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

Vigfus: Sure:

let add_2 n =
  2 + n;;

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

Harald: 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.

Harald: 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.

Harald: Hum.

Alfrothul: How about we parameterize this elephant?

Harald: 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;;

Harald: He, he.

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

Harald: 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.

Brynja: Wait. These definitions can be simplified.

Harald: Simplified?

Brynja: 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;;

Vigfus: That’s a lot shorter.

Brynja: 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?

Harald: 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.

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

let mul i n =
  i * n;;

Vigfus: 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;;

Vigfus: By which I mean the simplified version:

let mul_2 = mul 2;;

Halcyon (happily): Ditto for 3:

let mul_3 = mul 3;;

Harald: 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.

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

Brynja: 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".

Harald: That is likely.

Brynja: And that would be a third same elephant.

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

Harald: Hum.

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

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

let the_generic_elephant f i n =
  f i n;;

Harald: 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;;

Brynja: 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

Harald: Where is Loki?

Halcyon: He’s gone.

Postlude

Vigfus: Er, guys?

The guys: Yes?

Vigfus: 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?

Brynja: And déjà programmé, oui, I mean yes, in Exercise 2.c, back in Week 04.

Harald: Harumph.

Post-postlude

Vigfus: Er, guys?

The guys: Yes?

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

let add_simplified =
  the_generic_elephant (+);;

let mul_simplified =
  the_generic_elephant ( * );;

Harald: Harumph. 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 (^);;

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

Halcyon: Well, they’re gone, right?

Post-post-postlude

Vigfus: Er, guys?

The guys: Yes?

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

Alfrothul: Well spotted, Vigfus! Indeed we can:

let the_generic_elephant f =
  f;;

Harald: But its type?

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

Harald: 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.

Harald: Harumph. But that makes sense, and -> does associate to the right.

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>
#

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

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

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

Vigfus: What do you mean?

Brynja: They only differ because of their base case.

Vigfus: So?

Brynja: 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_given =
  let () = assert (n_given >= 0) in
  let rec visit n =
    if n = 0
    then zero_case
    else not (visit (pred n))
  in visit n_given;;

Vigfus: 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.

Resources

• The OCaml code for the present lecture note (latest version: 28 Feb 2020).

Version

Added the resource file [28 Feb 2020]

Added the closing bit about parity predicates [26 Feb 2020]

Adjusted some more [22 Feb 2020]

Polished the narrative, like, a lot [21 Feb 2020]

Created [21 Feb 2020]