Tutorial

Sometimes the best feature in ML—the type system—is precisely the thing standing between you and what you need to get done. In this article we’ll dive into the world of discrete math to understand how to achieve a function of variable arity in OCaml, allowing for the encoding of, say, a logical proposition with any number of terms.

The Math

Consider a problem set that asks you to evaluate the truth of the following:

Applying a quick translation from set notation to formal logic notation:

• Union: A ∪ B becomes A ∨ B
• Set minus: A \ B becomes A ∧ ¬B
• Oplus: A ⊕ B stays as is, XOR
• Subset equal: A ⊆ B becomes A → B

And an encoding of these rules into OCaml:

let (!-) a = not a;; (* symbolic not *)
let (--) a b = a && (!- b);; (* logical minus *)
let (<+>) a b = (a || b) && (!- (a && b));; (* xor (oplus) *)
let (-->) a b = (a && b) || (!- a);; (* single implication *)

We can determine the truth of the posited logical expression by determining if the implication stated is or is not a tautology.

(b -- (a <+> c)) --> ((c || b) -- (c -- a))

We now have a logical representation of the given set expression that we can query within the OCaml toplevel!

To declare an expression a tautology, we must observe that every combination of terms yields a valid expression. In this case that ain’t so bad, there are only 2³ possible combinations. But what if your expression has 5 terms, or 7? Manual enumeration of these truth tables would be excruciating.

The Type System

Wouldn’t it be nice if there were a function that could spit out the truth table of a given logical expression? The naive approach to this ends with fun messages like this one:

Error: This expression has type bool -> bool -> bool -> bool
       but an expression was expected of type bool -> bool -> bool
       Type bool -> bool is not compatible with type bool

When you try to provide an expression with three terms instead of two. Does your head hurt yet? Mine does!

In a nutshell, this is the problem of variable arity in a language with a strict type system like OCaml. In the truth table function, I want to be able to evaluate a boolean expression of arbitrary terms, but the type system wants me to explicitly state from the outset how many terms it can expect.

Let’s do just that: define a standard type that won’t upset the type inference machine while still allowing an arbitrary number of terms for our logical expression. Behold the mighty power of the recursive enum:

type 'a parfun =
  | Par of ('a -> 'a parfun)
  | Expr of 'a;;

What are we looking at here? We have the type 'a parfun that allows us to define an Expr that takes an arbitrary number of arguments of type 'a and evaluates to some 'a—exactly what we need to define our logical expressions.

There’s a bit of boilerplate involved, but our expression defined in the previous section looks like this as a bool parfun:

let our_expr = Par (fun a -> Par (fun b -> Par (fun c -> Expr (
  (b -- (a <+> c)) --> ((c || b) -- (c -- a))
))));;

It’s hideous. It’s beautiful. It’s a bool parfun.

We need a special way to evaluate our parfun that doesn’t upset the sleeping beast past which we just snuck. To do this, let’s provide our arguments to the nested Expr as a list.

(* evaluate a parfun f with the given var list v *)
let eval_parfun f vars =
  List.fold_left (fun facc v ->
    match facc with
    | Par pf -> pf v
    | Expr _ -> failwith "dimension mismatch: |parfun| < |vars|"
  ) f vars
  |>  function
      | Expr result -> result
      | Par _ -> failwith "dimension mismatch: |parfun| > |vars|";;

We can now evaluate our_expr:

> eval_parfun our_expr [true; false; false];;
- : bool = true

Back to the Math

The final steps in this example are to define the truth table function. For this we need to be able to determine the arity of the Expr buried beneath all of those Pars.

let rec arity ~atom:a = function
  | Expr _ -> 0
  | Par p -> 1 + (arity ~atom:a (p a));;

let arity_of_bool_parfun = arity ~atom:true;;

Note that we have to provide a hint as to what our type variable 'a is to be able to unravel our 'a parfun.

Next up we generate the values for the terms in every row of the truth table:

let combinations n =
  let rec comb_loop acc i =
    if i = 0 then acc
    else comb_loop ((List.map (fun l -> true :: l) acc)
         @ (List.map (fun l -> false :: l) acc)) (i-1) in
  comb_loop [[true];[false]] (n-1);;

Then defining the truth table function:

let truthtable expr =
  let open List in
  let b2i b = if b then 1 else 0 in
  let nvars = arity_of_bool_parfun expr in
  iter (printf "v%d\t") (1|..|nvars);
  printf "expr\n";
  iter (fun c ->
    iter (fun b -> printf "%d\t" (b2i b)) c;
    printf "%d\n" (b2i (eval_parfun expr c))
  ) (combinations nvars);;

To yield:

> truthtable our_expr;;
v1      v2      v3      expr
1       1       1       1
1       1       0       1
1       0       1       1
1       0       0       1
0       1       1       1
0       1       0       1
0       0       1       1
0       0       0       1
- : unit = ()

It’s a tautology!

Wrapping Up

Now we can generate all the truth tables our hearts desire without leaving the padded box of utop. It’s a tad verbose, but without macro capabilities there’s not much that can be done about that within the confines of the type system. Never change, OCaml.

If you want to fiddle around with it yourself, you can find the code here.

If you liked the article, found something I overlooked, came up with a novel application for your parfun, or want to discuss further, let me know in the comments!