Comprensione dei politipi in un'inferenza di tipo Hindley-Milner

Question

Sto leggendo l'articolo di Wikipedia su Hindley–Milner Type Inference cercando di dare un senso a questo. Finora questo è quello che ho capito:

1. I tipi sono classificati come monotipi o politipi.
2. I monotipi sono inoltre classificati come costanti di tipo (come int o string) o variabili di tipo (come α e β).
3. Le costanti di tipo possono essere tipi concreti (come int e string) o tipi costruttori (come Map e Set).
4. Le variabili di tipo (come α e β) si comportano come segnaposti per tipi di calcestruzzo (come int e string).

Ora sto avendo un po 'di difficoltà a capire politipi ma dopo aver appreso un po' di Haskell questo è quello che farne:

1. Tipi stessi hanno tipi. Formalmente tipi di tipi sono chiamati tipi (cioè ci sono diversi tipi di tipi).
2. tipi di calcestruzzo (come int e string) e digitare variabili (come α e β) sono di tipo *.
3. Tipo costruttori (come Map e Set) sono astrazioni lambda di tipo (per esempio Set è di tipo * -> * e Map è di tipo * -> * -> *).

Quello che non capisco è cosa significano i qualificatori. Ad esempio cosa rappresenta ∀α.σ? Non riesco a fare testa o croce di esso e più leggevo il seguente paragrafo il più confuso ottengo:

Una funzione con polytype ∀α.α -> α per contro, può mappare qualsiasi valore dello stesso tipo su se stesso e il valore identity function è un valore per questo tipo. Come altro esempio ∀α. (Set α) -> int è il tipo di una funzione che associa tutti gli insiemi finiti a numeri interi. Il conteggio dei membri è un valore per questo tipo. Nota che i qualificatori possono apparire solo di livello superiore, ovvero un tipo ∀α.α -> ∀α.α per esempio, è escluso dalla sintassi dei tipi e che i monotipi sono inclusi nei politipi, quindi un tipo ha il generale modulo ∀α₁. . . ∀αₙ.τ.

Answer 1

In primo luogo, tipi e tipi polimorfici sono cose diverse. Puoi avere un sistema di tipo HM in cui tutti i tipi sono dello stesso tipo (*), potresti anche avere un sistema senza polimorfismo ma con tipi complessi.

Se un termine M è di tipo ∀a.t, significa che per qualsiasi tipo di s possiamo sostituire s per a a t (spesso scritto come t[a:=s] e avremo che M è di tipo t[a:=s]. Questo è in qualche modo simile a logica, dove siamo in grado di sostituire qualsiasi termine di una variabile universalmente quantificata, ma qui abbiamo a che fare con i tipi.

Questo è esattamente ciò che accade in Haskell, solo che in Haskell non si vedono i quantificatori. Tutto le variabili di tipo che appaiono in una firma di tipo sono quantificate implicitamente, solo a s se avevi forall di fronte al tipo. Ad esempio, map avrebbe tipo

map :: forall a . forall b . (a -> b) -> [a] -> [b] 

ecc Senza questo quantificazione universale implicita, variabili di tipo a e b avrebbe dovuto avere un significato fisso e map non sarebbe polimorfica.

L'algoritmo HM distingue tipi (senza quantificatori, monotipi) e tipo schemi (tipi universaly quantificati, politipi). È importante che in alcuni punti utilizzi schemi di tipi (come in let), ma in altri luoghi sono consentiti solo tipi. Questo rende l'intera cosa decidibile.

Ti suggerisco inoltre di leggere l'articolo su System F. Si tratta di un sistema più complesso, che consente forall ovunque nei tipi (quindi tutto ciò che è appena chiamato tipo), ma digitare inferenza/controllo è indecidibile. Può aiutarti a capire come funziona forall. Il sistema F è descritto in profondità in Girard, Lafont e Taylor, Proofs and Types.

Answer 2

Considerare l = \x -> t in Haskell. È un lambda, che rappresenta un termine t per una variabile x, che verrà sostituita in un secondo momento (ad esempio l 1, qualunque cosa significherebbe). Allo stesso modo, ∀α.σ rappresenta un tipo con una variabile di tipo α, ovvero f : ∀α.σ se una funzione è parametrizzata da un tipo α. In un certo senso, σ dipende da α, quindi f restituisce un valore di tipo σ(α), dove α verrà sostituito in σ(α) in seguito e otterremo del tipo concreto.

In Haskell è possibile omettere ∀ e definire le funzioni come id : a -> a. La ragione per consentire di omettere il quantificatore è fondamentalmente dal momento che sono consentiti solo di livello superiore (senza estensione RankNTypes). Si può provare questo pezzo di codice:

id2 : a -> a -- I named it id2 since id is already defined in Prelude 
id2 x = x 

Se chiedete ghci per il tipo di id (:t id), verrà restituito a -> a. Per essere più precisi (più teorico del tipo), id ha il tipo ∀a. a -> a.Ora, se si aggiunge al codice:

val = id2 3 

, 3 ha il tipo Int, così il tipo Int sarà sostituito in σ e noi otterrà il tipo concreto Int -> Int.