Digitare l'inferenza sul problema di unificazione

Question

Qualcuno ha idea di come il problema di inferenza del tipo

E > hd (cons 1 nil) : α0

con l'ambiente di digitazione

                E={
                   hd : list(α1 ) → α1 ,
                   cons : α2 → list(α2 ) → list(α2 ),
                   nil : list(α3 ),
                   1 : int
                }

può essere trasferito in un problema di unificazione?

Qualsiasi aiuto sarebbe davvero apprezzato!

Answer 1

Innanzitutto, rinomina le variabili di tipo in modo che nessuna delle variabili nell'espressione si scontrino con le variabili nell'ambiente di digitazione. (Nel tuo esempio, questo è già stato fatto poiché l'espressione fa riferimento a {a0} e l'ambiente di digitazione fa riferimento a {a1, a2, a3}.

In secondo luogo, usando nuove variabili di tipo, crea una variabile di tipo per ogni sottoespressione all'interno della tua espressione, producendo qualcosa del tipo:

nil : a4
1 : a5
cons : a6
(cons 1 nil) : a7
hd : a8
hd (cons 1 nil) : a0 // already had a type variable

Terzo, genera un insieme di equazioni tra le variabili di tipo che devono contenere. Puoi farlo dal basso verso l'alto, dall'alto verso il basso o in altri modi. Vedi Heeren, Bastiaan. Messaggi di errore di alta qualità. 2005. per maggiori dettagli sul perché potresti voler scegliere in un modo o nell'altro. Ciò si tradurrà in qualcosa di simile:

a4 = list(a3) // = E(nil)
a5 = int // = E(1)
a6 = a2 -> list(a2) -> list(a2) // = E(cons)

// now it gets tricky, since we need to deal with application for the first time
a5 = a2 // first actual param of cons matches first formal param of cons
a4 = list(a2) // second actual param of cons matches type of second formal param of cons
a7 = list(a2) // result of (cons 1 nil) matches result type of cons with 2 params

a8 = list(a1) -> a1 // = E(hd)    

// now the application of hd
a7 = list(a1) // first actual param of hd matches type of first formal param of hd
a0 = a1 // result of hd (cons 1 nil) matches result type of hd with 1 param

Nota attentamente che se la stessa funzione venisse usata due volte dall'ambiente di tipo, avremmo bisogno di più nuove variabili di tipo (nel secondo passaggio sopra) per unificarci, in modo da non effettuare accidentalmente tutte le chiamate ai contro lo stesso tipo. Non sono sicuro di come spiegare più chiaramente questa parte, scusa. Eccoci nel caso semplice poiché hd e contro sono usati solo una volta.

Quarto, unifica queste equazioni, risultando (se non ho fatto un errore) qualcosa del tipo:

a4 = list(int)
a5 = int
a6 = int -> list(int) -> list(int)
a7 = list(int)
a8 = list(int) -> int
a0 = int

Rallegrati, ora conosci il tipo di ogni sottoespressione nella tua espressione originale.

(Avviso equo, sono un po 'un dilettante in queste faccende, e potrei aver fatto un errore tipografico o inavvertitamente imbrogliato da qualche parte qui.)