Ho appena letto su row polymorphism e su come può essere utilizzato per i record estensibili e le varianti polimorfiche.perché OCaml usa la sottotipizzazione per le varianti polimorfiche?
Tuttavia, Ocaml utilizza la sottotipizzazione per le varianti polimorfiche. Perché? È più potente del polimorfismo di riga?
Per completare la risposta di Gabriel, un modo di pensare a questo è che subtyping fornisce una forma debole di entrambi universale e esistenziali polimorfismo. Quando entrambe le direzioni del polimorfismo parametrico sono disponibili, allora l'espressività della sottotipizzazione è per lo più sussunta (specialmente quando non c'è sottotipizzazione di profondità). Ma non è il caso di Ocaml.
Ocaml sostituisce l'aspetto universale con il polimorfismo universale effettivo, ma mantiene la sottotipizzazione per fornire una forma di quantificazione esistenziale che altrimenti non avrebbe. Questo è necessario per formare ad es. raccolte eterogenee, come ad esempio <a: int> list in cui si desidera poter archiviare oggetti arbitrari che abbiano almeno un metodo a di tipo corretto.
vorrei andare anche oltre e dire che, mentre questo è di solito spiegata come subtyping nel mondo OCaml, si potrebbe in realtà interpretare le righe chiusi come esistenzialmente quantificata su una coda (sconosciuto). La coercizione tramite :> sarebbe quindi un'introduzione esistenziale, rimanendo quindi più fedele al mondo del polimorfismo parametrico su cui sono costruite le righe. (Naturalmente, con questa interpretazione, lo # farebbe un'eliminazione esistenziale implicita.) Se dovessi progettare un sistema simile a Ocaml da zero, probabilmente proverei a modellarlo in quel modo.
OCaml utilizza sia in polimero che in sottotipo per le varianti polimorfiche (e gli oggetti, per quella materia). Il polimorfismo di riga è coinvolto per tipi di oggetti "aperti" < m1 : t1; m2 : t2; .. > (il .. letteralmente parte del tipo) o tipi di varianti "aperti" [> `K1 of t1 | `K2 of t2 ]. La sottotipizzazione viene utilizzata per eseguire il cast tra tipi chiusi non polimorfi <m1:t1; m2:t2> :> <m1:t1> o [ `K1 of t1 ] :> [ `K1 of t1 | `K2 of t2 ].
Il polimorfismo di riga consente di evitare la necessità di quantificazione limitata per esprimere tipi come "prendere un oggetto che ha almeno il metodo m e restituire un oggetto dello stesso tipo": la sottotipizzazione è quindi piuttosto semplice, esplicita e non può essere astratto. Al contrario, il polimorfismo di riga è più facile da dedurre e funzionerà meglio con il resto del sistema di tipi. Raramente dovrebbe essere necessario utilizzare tipi chiusi e sottotipi espliciti, ma a volte è conveniente - e in particolare, mantenendo chiuso il tipo può produrre messaggi di errore che sono più facili da capire.
Grazie! Mai pensato di sottotipizzare le coercizioni come quantificazione universale/esistenziale sulla variabile di riga ... –
In effetti, abbiamo dei mezzi per la quantificazione esistenziale in OCaml; attraverso la solita (ma pesante) codifica con un doppio strato di quantificatori universali di prima classe in campi di record polimorfici, o ora attraverso record di prima classe o GADT. È giusto che nel loro vecchio lavoro di Objective ML, Jérôme Vouillon e Didier Rëmy giustificassero i tipi chiusi in questo modo; ma notiamo che esiste un utilizzo diverso con le altre esistenziali che abbiamo: con i tipi chiusi, sia l'impacchettamento e il disimballaggio degli elementi esistenziali sono impliciti (l'impacchettamento avviene attraverso l'istanziazione (dedotta)), sia gli altri esistenziali sono più espliciti. – gasche