Unification algorithm in Elixir.

unification.ex

# Discussed in https://www.ericpfahl.com/from-pattern-matching-to-unification/

defmodule Var do
  alias Var

  @type t :: %Var{id: any}
  defstruct [:id]

  @spec new(any) :: Var.t()
  def new(id), do: %Var{id: id}
end

defmodule Unification do
  @type variable :: Var.t()
  @type atomic :: number | atom | binary
  @type uterm :: atomic | variable | [uterm]
  @type substitution :: %{} | %{variable => uterm}

  @spec unify(substitution, uterm, uterm) :: {:ok, substitution} | :error
  def unify(sub, term1, term2) do
    do_unify(sub, walk(sub, term1), walk(sub, term2))
  end

  defp do_unify(sub, term1, term2) when term1 == term2, do: {:ok, sub}
  defp do_unify(sub, %Var{} = var, term), do: extend(sub, var, term)
  defp do_unify(sub, term, %Var{} = var), do: extend(sub, var, term)

  defp do_unify(sub, [h1 | t1], [h2 | t2]) do
    with {:ok, sub} <- unify(sub, h1, h2) do
      unify(sub, t1, t2)
    end
  end

  defp do_unify(_sub, _term1, _term2), do: :error

  @spec extend(substitution, variable, uterm) :: {:ok, substitution}
  defp extend(sub, var, term), do: {:ok, Map.put(sub, var, term)}

  @spec walk(substitution, uterm) :: uterm
  def walk(sub, term) do
    case Map.fetch(sub, term) do
      {:ok, t} -> walk(sub, t)
      :error -> term
    end
  end

  @spec simplify(substitution, uterm) :: uterm
  def simplify(sub, term) do
    case walk(sub, term) do
      [h | t] -> [simplify(sub, h) | simplify(sub, t)]
      term -> term
    end
  end
end