pattern matching of variant tag in OCaml

Question

I have the following OCaml substitution function.

let rec subst x a f =                                                                                                                                    
    match f with                                                                                                                                           
    | Var s -> if s = x then a else Var s                                                                                                                 
    | Implies (f1, f2) -> Implies (subst x a f1, subst x a f2)                                                                                            
    | And (f1, f2) -> And (subst x a f1, subst x a f2)                                                                                                     
    | Or (f1, f2) -> Or (subst x a f1, subst x a f2)                                                                                                                                                                                   
    | True | False as e -> e

Some cases are almost identical and I'm wondering if there's a way to factorize them somehow.

Ideally, I'm thinking of a construct of the form:

match f with
| tag (f1, f2) -> tag (subst x a f1, subst x a f2)
| ... 

that would match all my binary operations.

An other use case would be in a to_string function where we could have:

match f with
| tag (f1, f2) -> print_string ((tag_to_string tag) ^ ...  )
| ... 

I know this isn't possible in OCaml, but is there a pattern or a language construct that goes in that direction?

Answer 1

You can't, but you can create one Binop constructor that you could use more easily. So your type definition would become something like:

type binop = Implies | And | Or
type t =
  | Var of string
  | Binop of binop * t * t
  | True | False

Then your function could be:

let rec subst x a f =
  match f with
  | Var s -> if s = x then a else f
  | Binop (b, f1, f2) -> Binop (b, subst x a f1, subst x a f2)
  | True | False -> f

Note that this makes Binop use one more word than your version, which is (at most times) a good price to pay for less codelines.

Answer 2

Nope, you can't bind constructor. If you find yourself tired from this, you can write mapper/folder classes, so that you don't need to repeat yourself.

For example, in mine project substitution function looks like this (for much more complex language)

let substitute x y = (object inherit mapper
  method! map_exp z = if Exp.(x = z) then y else z
end)#run

Answer 3

(Disclaimer: I am more familiar with Haskell than Ocaml, so I may not be doing things in the most idiomatic way)

I don't know of a general way (besides some sort of macro) to solve this problem, but a type of encoding that I have learned and find helpful is the following:

type t =
  | Var of t
  | Implies of t * t
  | And of t * t
  | Or of t * t
  | True
  | False

let apply_t var implies and_t or_t true_t false_t = function
  | Var s -> var s
  | Implies (a, b) -> implies a b
  | And (a, b) -> and_t a b
  | Or (a, b) -> or_t a b
  | True -> true_t
  | False -> false_t

This should help the definition of some functions and an abstract use of the type. In this case, it only results in less code if you have to define more of these kinds of functions. Nevertheless, it may give you some ideas. With a few more helpers, we can see how a function like subst could easily be implemented

(* Ocaml constructors behave oddly *)
let impliest (a, b) = Implies (a, b)
let andt (a, b) = And (a, b)
let ort (a, b) = Or (a, b)

let rec subst x a =
  let varf s = if s = x then a else Var s in
  let bin_subst tag f1 f2 = tag (subst x a f1, subst x a f2) in
  apply_t varf (bin_subst impliest) (bin_subst andt) (bin_subst ort) True False

Another possibility that probably fits some use cases better is to encode both True and False as a single parameter taking the value as a parameter in the apply_t function.

Answer 4

One simple approach would be to write a nested function just above your match expression, but you have to modify your variant:

type t =
  | Var of t
  | Implies of (t * t) (* NOTE the parens around the arguments *)
  | And of (t * t)
  | Or of (t * t)
  | True
  | False

let rec subst x a f =
  let g f1 f2 = (subst x a f1, subst x a f2) in
  match f with
  | Var s -> if s = x then a else Var s
  | Implies (f1, f2) -> Implies (g f1 f2)
  | And (f1, f2) -> And (g f1 f2)
  | Or (f1, f2) -> Or (g f1 f2)
  | True | False as e -> e

There is some code duplication so it doesn't scale as well as PatJ's, but it's also clearer in some sense since you only have three binary operations.

Regarding your tag idea, I don't believe there is a way to bind constructors based on the number of arguments. For details, see http://caml.inria.fr/pub/docs/manual-ocaml-400/patterns.html