Regras do Algoritmo unify(C):
• Se vazio: Sucesso, termina o processo.
O algoritmo retira uma equação 'S = T' do conjunto para analisar e chama o que sobrou de 'C':
• if S = T then unify(C')
• else if S = X and X ∉ FV(T):
Se o lado esquerdo for uma variável X e ela não estiver contida nas variáveis livres de T, então: unify([X ↦ T]C') ∘ [X ↦ T], o compilador aplica a substituição [X ↦ T] no restante das equações (C') e resolve o sistema restante, compondo (∘) o resultado com a descoberta atual [X ↦ T].
• else if T = X and X ∉ FV(S):
Se o lado direito for uma variável X e ela não estiver contida nas variáveis livres de S, então: unify([X ↦ S]C') ∘ [X ↦ S], faz o mesmo processo inverso, aplicando a substituição [X ↦ S] em C' e compondo com o resultado final.
• else if S = S₁→S₂ and T = T₁→T₂:
then unify(C' ∪ {S₁ = T₁, S₂ = T₂}), decomposição de Funções: Se os dois lados forem funções, para elas serem iguais, seus argumentos e retornos também devem ser. O algoritmo quebra a equação complexa em duas menores (S₁ = T₁ e S₂ = T₂) e as devolve para a lista 'C'.
• else fail, conflito de Tipos: Se nenhum dos casos anteriores se aplicar (ex: tentar igualar Nat = Bool ou Nat = X→Y), o sistema é impossível de resolver. O algoritmo falha catastróficamente (Erro de Tipo).
Se o unify(C) = sigma, então sigma é um unificador principal para C.