Digite para "maneiras pelas quais os valores podem ser diferentes"

Estou procurando um conceito na teoria dos tipos que, com certeza, já foi explorado, mas não sei o nome por trás.

Vamos considerar uma linguagem do tipo ML com tipos de produto e soma e um sistema de tipo Hindley-Milner. Vou usar a sintaxe do OCaml.

Estou me perguntando sobre maneiras como dois valores diferentes podem ser diferentes.

Usar

Meu caso de uso está escrevendo mensagens de erro "mais claras" em uma biblioteca semelhante ao xUnit: se dois valores forem diferentes quando se espera que sejam iguais, isso poderá ajudar a criar uma mensagem melhor e mais clara:

Antes:

Valores diferentes: esperado {x = [1;2;3;4], y = "a long string"}, obtido{x = [1;2;3;3], y = "a long string"}

Depois de:

Os valores diferem: na posição .x[3]esperada 4, obtém 3.

(pode haver uma relação com as lentes funcionais, já que estamos construindo uma lente com um valor menor que difere).

Tipos de produtos

Por exemplo:

type p =
  { x : int
  ; y : string
  }

Igualdade pode ser definida como:

let equal a b =
  equal_int a.x b.x && equal_string a.y b.y

Mas também é possível reificar as diferenças:

type delta_p =
  | Equal
  | Diff_x of int * int
  | Diff_y of string * string

let diff_p a b =
  if not (equal_int a.x b.x) then
    Diff_x (a.x, b.x)
  else if not (equal_string a.y b.y) then
    Diff_y (a.y, b.y)
  else
    Equal

(pode fazer sentido definir um delta_inttipo int * intpara mostrar que é recursivo)

Tipos de soma

Para um tipo de soma, há mais maneiras de diferir: ter um construtor diferente ou um valor diferente

type s = X of int | Y of string

type ctor_s =
  | Ctor_X
  | Ctor_Y

type delta_s =
  | Equal
  | Diff_ctor of ctor_s * ctor_s
  | Diff_X of int * int
  | Diff_Y of string * string

let diff_s a b = match (a, b) with
  | X xa, X xb ->
    if equal_int xa xb then
      Equal
    else
      Diff_X (xa, xb)
  | (* Y case similar *)
  | X _, Y _ -> Diff_ctor (Ctor_X, Ctor_Y)
  | Y _, X _ -> Diff_ctor (Ctor_Y, Ctor_X)

Qual o nome desse conceito? Onde posso aprender mais sobre isso?

Obrigado!

Eu acho que você está procurando uma variante digitada de anti-unificação . A anti-unificação pode ser descrita da seguinte forma. Primeiro, suponha que tenhamos uma gramática de termos da seguinte maneira:

t ::= () | (t, t) | C t | X 

Aqui, ()e (t, t)denotam unidades e pares, C té um termo com um construtor principal e Xé uma variável de termo que pode ser substituída por qualquer termo.

O problema anti-unificação diz, se você der dois termos t1e t2, qual é o termo menos geral para tque haja substituições s1e para s2que s1(t) = t1e s2(t) = t2.

Como exemplo concreto, dados dois termos

t1 = Cons(3, Cons(2, Cons(1, Nil)))
t2 = Cons(1, Cons(2, Cons(3, Nil)))

o algoritmo anti-unificação retornaria o anti-unificador

t = Cons(X, Cons(2, Cons(Y, Nil)))

porque as substituições s1 = [X:3, Y:1]e as s2 = [X:1, Y:3]candidatas tlhe dariam t1e t2devolveriam. Como um aparte, precisávamos especificar "menos geral" porque caso contrário:

t' = Z 

com as substituições s1 = [Z:t1]e s2 = [Z:t2]faria o truque.

A anti-unificação foi inventada por Gordon Plotkin e é um algoritmo deliciosamente simples. Suponha que você tenha uma função injetora de geração de nome . Então podemos encontrar um antiunificador da seguinte maneiragen $: \mathrm{Term} \times \mathrm{Term} \to \mathrm{Var}$

antiunify ()       ()         = ()
antiunify (t1, t2) (t1', t2') = (antiunify t1 t1', antiunify t2 t2')
antiunify (C t)    (C t')     = C (antiunify t t')
antiunify t        t'         = gen(t, t') -- default: t and t' dissimilar 

Aumentando este algoritmo para retornar as duas substituições s1e s2deixo como um exercício.