Seeking Unification Algorithm in F#

Question

I am transforming ASTs and need more than simple pattern matching, thus the unification algorithm.

While this is for a .NET project and I know that I could just interoperate with a .NET PROLOG implementation, I only need to embed the unification algorithm; so PROLOG is overkill.

If I could get "Martelli, Montanari: An Efficient Unification Algorithm" written in F# that would be perfect, but I will settle for it any functional language including HASKELL and translate to F#.

Answer 1

In general, it is a good practice to share your attempts when asking questions on SO. People will not generally give you a complete solution for your problems - just answers when you have specific question or hints how to approach the problem.

So, I'll share some hints about the general approach, but it is not a complete solution. First you need to represent your AST in some way. In F#, you can do that using discriminated unions. The following supports variables, values and function applications:

type Expr =
  | Function of string * Expr list
  | Variable of string
  | Value of int

Unification is a function that takes list of expressions to be unified of type (Expr * Expr) list and returns assignments to variables (assigning an expression Expr to a variable name string):

let rec unify exprs =
  match exprs with 
  // Unify two variables - if they are equal, we continue unifying 
  // the rest of the constraints, otherwise the algorithm fails
  | (Variable s1, Variable s2)::remaining ->
      if s1 = s2 then unify remaining
      else failwith "cannot unify variables"
  // Unify variable with some other expression - unify the remaining
  // constraints and add new assignment to the result
  | (Variable s, expr)::remaining 
  | (expr, Variable s)::remaining  ->
      let rest = unify remaining
      // (s, expr) is a tuple meaning that we assign 'expr' to variable 's'
      (s, expr)::rest

  // TODO: Handle remaining cases here!
  | _ -> failwith "cannot unify..."

There are a few cases that you'll need to add. Most importantly, unifying Function with Function means that you need to check that the function names are the same (otherwise fail) and then add all argument expressions as new constraints to the remaining list...

Answer 2

The final syntactic unification in Baader & Snyder uses union-find to partition the nodes of the two structures into equivalence classes. It then walks those classes building up the triangular substitution.

Since it uses union-find, if you're looking for a purely functional answer you're out of luck; no-one knows how to write a functional union-find. However, we know how to write a persistent union-find which is at least apparently functional, thanks to Conchon and Filliâtre (written in OCaml).