La proposta più recente per i tipi di Rank-N è la carta FPH collegata a Don. Secondo me è anche il più bello del gruppo. L'obiettivo principale di tutti questi sistemi è quello di richiedere il minor numero possibile di annotazioni di testo. Il problema è che quando si passa da Hindley/Milner a System F perdiamo tipi principali e l'inferenza di tipo diventa indecidibile - da qui la necessità di annotazioni di tipo.
L'idea di base dei "tipi di boxe" è di propagare le annotazioni di tipo il più lontano possibile. Il controllo del tipo consente di passare dalla verifica del tipo alla modalità di inferenza del tipo e, auspicabilmente, non sono necessarie ulteriori annotazioni. Il rovescio della medaglia qui è che l'annotazione del tipo è richiesta o meno è difficile da spiegare perché dipende dai dettagli di implementazione.
Il sistema MLF di Remy è finora la proposta più bella; richiede la minima quantità di annotazioni di tipo ed è stabile in molte trasformazioni di codice. Il problema è che estende il sistema di tipi. Il seguente esempio illustra questa norma:
choose :: forall a. a -> a -> a
id :: forall b. b -> b
choose id :: forall c. (c -> c) -> (c -> c)
choose id :: (forall c. c -> c) -> (forall c. c -> c)
Entrambi i tipi di cui sopra sono admissable in System F. Il primo è il tipo Hindley/Milner standard utilizza istanziazione predicativo, la seconda utilizza istanziazione impredicativa. Nessuno dei due tipi è più generale dell'altro, quindi l'inferenza di tipo dovrebbe indovinare quale tipo l'utente desidera e di solito è una cattiva idea.
MLF estende invece il sistema F con quantificazione limitata.Il principale (= più generale) tipo per l'esempio di cui sopra potrebbe essere:
choose id :: forall (a < forall b. b -> b). a -> a
si può leggere questo come "choose id è digitare a-a dove a deve essere un'istanza di forall b. b -> b".
È interessante notare che questo da solo non è più potente del normale Hindley/Milner. Pertanto MLF consente anche la quantificazione rigida. I due tipi seguenti sono equivalenti:
(forall b. b -> b) -> (forall b. b -> b)
forall (a = forall b. b -> b). a -> a
quantificazione rigide è introdotta da annotazioni di tipo ei dettagli tecnici sono infatti piuttosto complicato. Il vantaggio è che MLF ha bisogno solo di poche annotazioni di tipo e c'è una semplice regola per quando è necessario. I lati negativi sono:
tipi possono diventare difficili da leggere, perché il lato destro della '<' può contenere quantificazioni ulteriormente nidificate.
Fino a poco tempo fa non esisteva una variante esplicita di MLF. Questo è importante per le trasformazioni del compilatore digitato (come fa GHC). La parte 3 di Boris Yakobowski's PhD thesis ha un primo tentativo con una tale variante. (Parti 1 & 2 sono interessanti, descrivono una rappresentazione più intuitiva FML tramite "Tipi grafici".)
Tornando FPH, la sua idea di base è quella di utilizzare tecniche MLF internamente, ma richiedono tipo annotazioni su attacchi let. Se si desidera solo il tipo Hindley/Milner, non sono necessarie annotazioni. Se si desidera un tipo di rango più elevato, è necessario specificare il tipo richiesto, ma solo al bind di let (o di livello superiore).
FPH (come MLF) supporta l'istanziazione impredicativa, quindi non penso che il problema si applichi. Non dovrebbe quindi esserci alcun problema a digitare la tua espressione f . g sopra. Tuttavia, FPH non è ancora stato implementato in GHC e molto probabilmente non lo sarà. Le difficoltà derivano dall'interazione con le coercizioni di uguaglianza (e possibilmente scrivono vincoli di classe). Non sono sicuro di quale sia l'ultimo stato, ma ho sentito che SPJ vuole allontanarsi dall'impredicatività. Tutto quel potere espressivo ha un costo, e finora non è stata trovata alcuna soluzione economica e onnicomprensiva.
Come si può rendere funzionanti i tipi di (runST per sempre)? – Peaker