[Haskell] "Quale parte di Milner-Hindley non capisci?"



Answers

Questa sintassi, sebbene possa sembrare complicata, è in realtà abbastanza semplice. L'idea di base viene dalla logica: l'intera espressione è un'implicazione con la metà superiore delle ipotesi e la metà inferiore è il risultato. Cioè, se sai che le espressioni migliori sono vere, puoi concludere che anche le espressioni di fondo sono vere.

simboli

Un'altra cosa da tenere a mente è che alcune lettere hanno significati tradizionali; in particolare, Γ rappresenta il "contesto" in cui ti trovi - cioè, quali sono i tipi di altre cose che hai visto. Quindi qualcosa come Γ ⊢ ... significa "l'espressione ... quando conosci i tipi di ogni espressione in Γ .

Il simbolo significa essenzialmente che puoi provare qualcosa. Quindi Γ ⊢ ... è una dichiarazione che dice "Posso provare ... in un contesto Γ . Queste affermazioni sono anche chiamate giudizi di tipo.

Un'altra cosa da tenere a mente: in matematica, proprio come ML e Scala, x : σ significa che x ha tipo σ . Puoi leggerlo proprio come Haskell's x :: σ .

Cosa significa ogni regola

Quindi, sapendo questo, la prima espressione diventa facile da capire: se sappiamo che x : σ ∈ Γ (cioè, x ha qualche tipo σ in qualche contesto Γ ), allora sappiamo che Γ ⊢ x : σ (cioè, in Γ , x ha tipo σ ). Quindi, davvero, questo non ti sta dicendo niente di super-interessante; ti dice solo come usare il tuo contesto.

Anche le altre regole sono semplici. Ad esempio, prendi [App] . Questa regola ha due condizioni: e₀ è una funzione da qualche tipo τ ad un certo tipo τ' ed e₁ è un valore di tipo τ . Ora sai che tipo otterrai applicando e₀ a e₁ ! Spero che questa non sia una sorpresa :).

La prossima regola ha qualche altra nuova sintassi. In particolare, Γ, x : τ significa semplicemente il contesto costituito da Γ e il giudizio x : τ . Quindi, se sappiamo che la variabile x ha un tipo di τ e l'espressione e ha un tipo τ' , conosciamo anche il tipo di una funzione che accetta x e restituisce e . Questo ci dice solo cosa fare se abbiamo capito che tipo ha una funzione e che tipo restituisce, quindi non dovrebbe sorprendere neanche.

Il prossimo ti dice come gestire le istruzioni let . Se sai che qualche espressione e₁ ha un tipo τ fintanto che x ha un tipo σ , allora un'espressione let che lega localmente x ad un valore di tipo σ farà sì che e₁ abbia un tipo τ . In realtà, questo ti dice solo che un'istruzione Let ti consente essenzialmente di espandere il contesto con un nuovo binding, che è esattamente ciò che let fa!

La regola [Inst] riguarda la sottotipizzazione. Dice che se si ha un valore di tipo σ' ed è un sottotipo di σ ( rappresenta una relazione di ordinamento parziale) allora quell'espressione è anche di tipo σ .

La regola finale riguarda i tipi di generalizzazione. Un rapido accostamento: una variabile libera è una variabile che non viene introdotta da un'istruzione let o lambda all'interno di un'espressione; questa espressione ora dipende dal valore della variabile libera dal suo contesto. La regola sta dicendo che se c'è qualche variabile α che non è "libera" in qualcosa nel tuo contesto, allora è sicuro di dire che qualsiasi espressione di cui tu sei tipo sappiamo e : σ avrà quel tipo per qualsiasi valore di α .

Come usare le regole

Quindi, ora che capisci i simboli, cosa fai con queste regole? Bene, puoi usare queste regole per capire il tipo di vari valori. Per fare ciò, guarda la tua espressione (ad esempio fxy ) e trova una regola che ha una conclusione (la parte inferiore) che corrisponde alla tua affermazione. Chiamiamo la cosa che stai cercando di trovare il tuo "obiettivo". In questo caso, osserveresti la regola che finisce in e₀ e₁ . Quando hai trovato questo, ora devi trovare regole che dimostrino tutto al di sopra della linea di questa regola. Queste cose generalmente corrispondono ai tipi di sottoespressioni, quindi stai essenzialmente ricorrendo a parti dell'espressione. Lo fai solo fino a quando non hai terminato la prova dell'albero, che ti fornisce una prova del tipo di espressione.

Quindi tutte queste regole sono specificate esattamente e nel solito dettaglio matematicamente pedante: P: come capire i tipi di espressioni.

Ora, questo dovrebbe sembrare familiare se tu abbia mai usato Prolog - stai essenzialmente calcolando l'albero delle prove come un interprete umano di Prolog. C'è una ragione per cui Prolog si chiama "programmazione logica"! Questo è importante anche perché il primo modo in cui sono stato introdotto nell'algoritmo di inferenza HM è stato implementandolo in Prolog. Questo è in realtà sorprendentemente semplice e rende chiaro ciò che sta succedendo. Dovresti sicuramente provarlo.

Nota: probabilmente ho fatto alcuni errori in questa spiegazione e mi piacerebbe che qualcuno li indicasse. In realtà mi occuperò di questo in classe tra un paio di settimane, quindi sarò più sicuro allora: P.

Question

Non riesco a trovarlo ora, ma giuro che c'era una maglietta in vendita con le parole immortali:

Quale parte di

non capisci?

Nel mio caso, la risposta sarebbe ... tutto!

In particolare, vedo spesso una notazione come questa nei documenti di Haskell, ma non ho idea di cosa significhi. Non ho idea di quale branca della matematica debba essere.

Riconosco ovviamente le lettere dell'alfabeto greco e simboli come "∉" (che di solito significa che qualcosa non è un elemento di un set).

D'altra parte, non ho mai visto "⊢" prima ( Wikipedia afferma che potrebbe significare "partizione" ). Anche io non ho familiarità con l'uso del vinculum qui. (Di solito denota una frazione, ma non sembra essere il caso qui.)

Immagino che SO non sia un buon posto per spiegare l'intero algoritmo di Milner Hindley. Ma se qualcuno potrebbe almeno dirmi dove iniziare a cercare di capire cosa significhi questo mare di simboli, sarebbe utile. (Sono sicuro di non poter essere l'unica persona che si sta chiedendo ...)




Come faccio a capire le regole di Hindley-Milner?

Hindley-Milner è un insieme di regole sotto forma di calcolo sequenziale (non deduzione naturale) che dice che è possibile dedurre il tipo (più generale) di un programma dalla costruzione del programma senza dichiarazioni di tipo esplicite.

I simboli e la notazione

Per prima cosa, spieghiamo i simboli

  • 𝑥 è un identificatore (informalmente, un nome di variabile).
  • : means è un tipo di (informalmente, un'istanza di, o "is-a").
  • σ (sigma) è un'espressione che è una variabile o una funzione.
  • ∈ significa è un elemento di
  • Γ (Gamma) è un ambiente.
  • (il segno di asserzione) significa asserzioni (o prove, ma contestualmente "asserisce" legge meglio).
  • Γ⊦ 𝑥 : σ è quindi letto Γ asserisce 𝑥, a σ
  • 𝑒 è un'istanza reale (elemento) di tipo σ .
  • τ (tau) è un tipo: di base, variabile ( α ), funzionale τ → τ ' , o prodotto τ × τ'
  • τ → τ ' è un tipo funzionale in cui τ e τ' sono tipi.
  • λ𝑥.𝑒 significa λ (lambda) è una funzione anonima che accetta un argomento, 𝑥 , e restituisce un'espressione, 𝑒 .
  • Sia 𝑥 = 𝑒₀ in 𝑒₁ significa nell'espressione, 𝑒₁ , sostituisci 𝑒₀ ovunque 𝑥 appare.
  • significa che l'elemento precedente è un sottotipo (informalmente - sottoclasse) di quest'ultimo elemento.
  • α è una variabile di tipo.
  • α.σ è un tipo, ∀ (per tutti) variabili di argomento, α , che restituisce un'espressione σ
  • libero (Γ) significa non un elemento delle variabili di tipo libero di Γ definite nel contesto esterno. (Le variabili associate sono sostituibili).

Tutto sopra la linea è la premessa, tutto sotto è la conclusione ( Per Martin-Löf )

Quelle che seguono sono interpretazioni in inglese delle affermazioni logiche, seguite da una spiegazione.

Variabile

Dato 𝑥 è un tipo di σ (sigma), un elemento di Γ (Gamma),
concludere Γ afferma 𝑥 è un σ.

Questa è fondamentalmente una tautologia: un nome identificatore è una variabile o una funzione.

Applicazione della funzione

Dato Γ asserisce che 𝑒₀ è un tipo funzionale e Γ asserisce 𝑒₁ è un τ
conclude Γ afferma che l'applicazione della funzione 𝑒₀ a 𝑒₁ è un tipo τ '

Ciò significa che se sappiamo che una funzione restituisce un tipo e lo applichiamo a un argomento, il risultato sarà un'istanza del tipo che sappiamo che restituisce.

Astrazione della funzione

Dato Γ e 𝑥 di tipo τ afferma 𝑒 è un tipo, τ '
concludere Γ asserisce una funzione anonima, λ di 𝑥 espressione di ritorno, 𝑒 è di tipo τ → τ '.

Ciò significa che se sappiamo che 𝑥 è di tipo τ e quindi un'espressione 𝑒 è di tipo τ ', allora una funzione di 𝑥 restituisce espressione 𝑒 è di tipo τ → τ'.

Lasciare una dichiarazione variabile

Dato Γ asserisce 𝑒₀, di tipo σ, e Γ e 𝑥, di tipo σ, asserisce 𝑒₁ di tipo τ
concludi Γ asserisce let 𝑥 = 𝑒₀ in 𝑒₁ di tipo τ

Questo significa che se abbiamo un'espressione 𝑒₀ che è a σ (essendo una variabile o una funzione), e qualche nome, 𝑥, anche a σ, e un'espressione 𝑒₁ di tipo τ, allora possiamo sostituire 𝑒₀ per 𝑥 ovunque appaia dentro di 𝑒₁.

la creazione di istanze

Dato Γ asserisce che 𝑒 di tipo σ 'e σ' è un sottotipo di σ
concludere Γ afferma 𝑒 è di tipo σ

Questo significa che se un'istanza è di un tipo che è un sottotipo di un altro tipo, è anche un'istanza di quel super-tipo.

Questo ci consente di utilizzare l'istanza del tipo nel senso più generale che un'espressione può restituire un tipo più specifico.

Generalizzazione

Dato Γ asserisce 𝑒 è un σ e α non è un elemento delle variabili libere di Γ,
conclude Γ asserisce 𝑒, scrivi per tutte le espressioni argomento α restituendo un'espressione σ

Ciò significa che possiamo generalizzare un programma per accettare tutti i tipi per argomenti non già associati all'ambito di contenimento (variabili che non sono non locali). Queste variabili associate sono sostituibili.

Conclusione

Queste regole combinate ci permettono di dimostrare il tipo più generale di un programma affermato, senza richiedere annotazioni di tipo, permettendo che vari tipi siano accettati correttamente come input (polimorfismo parametrico).




La notazione viene dalla deduzione naturale .

⊢ il simbolo si chiama turnstile .

Le 6 regole sono molto semplici.

Var regola del Var è una regola piuttosto banale - dice che se il tipo per l'identificatore è già presente nell'ambiente del tuo tipo, allora per dedurre il tipo lo prendi semplicemente dall'ambiente così com'è.

App regola App dice che se si hanno due identificatori e0 ed e1 e si può inferire il loro tipo, allora si può inferire il tipo di applicazione e0 e1 . La regola si legge in questo modo se si conosce che e0 :: t0 -> t1 e e1 :: t0 (lo stesso t0!), Quindi l'applicazione è ben tipizzata e il tipo è t1 .

Abs e Let sono regole per inferire i tipi per lambda-astrazione e let-in.

Inst regola Inst dice che puoi sostituire un tipo con uno meno generale.




Links