Jakie są główne różnice między polimorfizmem wierszy a podtypami

Często słyszę, że polimorfizm szeregowy jest lepszym podejściem niż podliczanie, ale mam trudności ze znalezieniem czegokolwiek porównującego je szczegółowo. Szczególnie interesuje mnie perspektywa użytkownika systemu.

Natrafiłem na ten post na blogu, ale pozostawia mi więcej pytań niż wcześniej. Na przykład twierdzi, że system z podtypami przypisuje jeden typ, podczas gdy system z typowaniem wierszy przypisze inny; czy to oznacza, że ​​jeśli system, który rzekomo ma podtypy, przypisuje typ „typowania wiersza”, to rzekomo błędnie?

Jedną z głównych różnic, jakie widzę, jest to, że typowanie wierszy umożliwia wyrównanie typów argumentów (tzn. Napisanie funkcji dwóch argumentów, która dotyczy samego apola argumentów, ale wymaga, aby jej argumenty miały takie same pola) .

Subtyping mówi, że biorąc pod uwagę wyrażenie jednego typu, możemy nadać mu również inny typ. Mówimy, że ten pierwszy jest podtypem tego drugiego, a ten związek podsieci wywołuje wiele innych związków. W symbolach

$(\forall \alpha.\tau) <: \tau[T/\alpha]$$T$

$\{\ell_1:A,\ell_2:B\} <: \{\ell_2:B,\ell_1:A\}$$\{\ell_1:A,\ell_2:B\} \cong \{\ell_2:B,\ell_1:A\}$$S \cong T \iff S <: T \land T <: S$$\{\ell_1:A,\ell_2:B\} = \{\ell_2:B,\ell_1:A\}$$T <: T$

Zwykle, gdy mówimy o języku z podtypami, mamy na myśli nietrywialny związek podtypów na typach podłoża , tj. Typy bez zmiennych swobodnych (które oczywiście mogą i będą generować relacje podtypów dla typów nie gruntowych). Tak więc system z polimorfizmem wierszy, taki jak Roy, nie jest językiem z podtypami w tym sensie, chociaż ma nietrywialną zależność podtypów, która pochodzi z dowolnego pośrednio utworzonego parametrycznego języka polimorficznego. Z drugiej strony, podtypowanie strukturalne wyraźnie określa nietrywialne relacje podtypów dla typów podłoża.

Przez typy wierszy mam na myśli nietrywialne zjednoczenie, jak opisano powyżej lub równoważne. Bez tego typy wierszy to niewiele więcej niż zagnieżdżone krotki. Uwaga: typy wierszy są niezależne od polimorfizmu parametrycznego; Nie mam na myśli sugerowania zmiennych wierszy. Z argumentu o $(\cong)$powyżej, podsieci strukturalne implikują typy wierszy, ale nie odwrotnie. Polimorfizm parametryczny jest ortogonalny (w tym sensie, że możesz go mieć lub nie, są zdecydowanie interakcje) z typami wierszy lub podtypami strukturalnymi. System z podtypem strukturalnym + polimorfizm parametryczny obejmuje typ wiersza + polimorfizm parametryczny (przy założeniu pewnego rodzaju „rekordowej unii”) w tym sensie, że każdy termin w tym drugim typie można wpisać tym samym typem w pierwszym. Ten pierwszy jest w stanie pisać także z dodatkowymi typami. Korzystanie przykład Briana, w systemie z podtypy strukturalnego i polimorfizm parametryczny answermiałby taki sam typ jak w wersji rząd typowania, ale to też rodzaj wersji Subtyping jest jako dobrze .

$\rho${ c : Number }informacja: przejście z podtypu do nadtypu powoduje utratę (typ) informacji. Często może to być to, czego chcesz: istnieje wspólny typ, na którym Ci zależy, a wszystko inne jest nieistotnymi szczegółami. Moje nastawienie polega na utrzymywaniu jak największej ilości informacji o typie i odrzucaniu ich tylko jawnie. Wady podejścia do podtypów są często dowodzone przez programy, które są poprawne pod względem typu, ale tylko dlatego, że typy zostały wypchnięte do typu „n” bez informacji, „górnego”, np. Pusty rekord. Powtarzanie, parametryczny polimorfizm (ogólnie) zachowuje informacje o typie, podtypowanie celowo je traci.