Unifying OCaml patterns through function composition

Question

Suppose that I have defined manually some code like that:

type test  = A of bool | B | C of bool * bool 
type test2 = D | E of bool * bool 
type test3 = F | G of bool | H of bool

let f = function | A(x) -> E(x,true) | B -> D | C(a,b) -> E(b,a)

let g = function  | D -> F | E(a,b) -> if a then G(b) else H(b)

Now I want to evaluate the composition g ∘ f as a function that does not require to use the intermediate representation test2. I've been thinking about structure unification, but I'm asking the following questions:

does OCaml automatically perform such unification when declaring let h x = g (f x)?
If not, does a general algorithm exist that could be implemented in OCaml in order to compile into an ml file such desired h?

Thanks in advance

ivg · Accepted Answer

Disclaimer

I'm not an OCaml compiler developer. If you want to get their opinion then it is better to contact them on the mailing list.

Part 1

Theoretically, the modern OCaml (I've tried with 4.0{3,4}+flambda) is capable of eliminating some intermediate data structures of type test2. However, to achieve this you need to pass special optimization options, and add [@@inlined always] to function f, otherwise it is not inlined even with crazy inline options like -inline 10000 and -inline-toplevel 10000.

However, in general case and for bigger functions this might not work. Here I suppose, that the example, that you've shown is a toy example, and in real life you're facing with much bigger functions and more than two compositions (i.e., hundreds of constructors with hundreds of compositions), otherwise, it is not worthwhile to optimize this at all).

Part 2

Theory

Speaking about the general algorithm, if we will be too picky, then it is impossible, as to the right of -> in the pattern match there can be any OCaml expression, i.e., a Turing-complete program. So, we have an equivalent of the decision problem. Even if we will restrict the expression language, by disallowing loops and side-effects, the problem would still be NP-hard, so it is probably not worthwhile to try to solve it. However, if we will restrict ourselves even more, by disallowing any expressions except constructor applications with trivial operands, then we will actually encode a Finite State Machine (FSM). There are plenty of well-defined FSM optimization and state minimization algorithms, so it wouldn't be hard to remove redundancy from it.

Practice

In practice, I wouldn't probably write a function, that translate ml code to ml code. Depending on my real task I will think about the following approaches.

Enumerable set of inputs

If the set of values that inhabit type test is practically finite (i.e., if it fits into OCaml array), then I would try to write a function that will enumerate all possible values of type test, and store the result of composition. You can use [@@deriving enumerate] to compute all possible values of type test

# type test  = A of bool | B | C of bool * bool [@@deriving enumerate];;
type test = A of bool | B | C of bool * bool
val all_of_test : test list =
  [A false; A true; B; C (false, false); C (true, false); C (false, true);
   C (true, true)]

Then, you can assign an ordinal to each value of type test and have an O(1) transformation to type test3. Also, there will be no allocations at all, since we already precomputed all constructors beforehand.

However, you will still need to transform test -> int for our approach to work, and this operation will require log(k) branches where k is the number of constructors in type test. From the big-O notation perspective, k is constant. But if it is really big, then you can try to make all your constructors argumentless, e.g., by representing A of bool as two constructors A_true and A_false. In this case, you will have pure O(1) transformation with no overhead (just an array dereference).

Enumerable input with uninterpreted functions

If there are constructors that bear values of type int or string, then it is practically impossible to enumerate them. However, if transformation h doesn't look at this values, but just rearrange them, i.e., treat them as Uninterpreted functions, then you should try to decouple this arguments from you input language by using GADT. Suppose you have the following data constructor:

| C of string

And result h (C s) is the same for all s. Then there is no need to pass s into h at all. However, you still want to pass a payload s to some other function, for example, to exec. It is possible to do with GADT, first we will decouple the payload from the constructor:

| C : string query

And then we will be able to pass the query to a function as two different parameters:

val exec : 'a query -> 'a -> unit

General case

If the two cases above didn't apply to you, then you need to write your own compiler :) It looks like, that you're implementing an interpreter of some language, that uses OCaml as a host language, and you're hoping that OCaml will do the optimizations for you. Well, OCaml is indeed not a bad choice to write interpreters, but it can't optimize your DSL, because it doesn't know the semantics of your DSL. And clever application of the semantics rules, is what all optimizations are about. So, that means, that if you're unsatisfied with the performance of your interpreter, then you need to write your own optimizing compiler. First of all, you will need to design, the abstract machine on which you will execute your queries, and then write an optimizer that is targeted to this machine.