Podpisywanie niejawne a jawne

Ta strona to potwierdza

wiele języków nie używa ukrytego podtytułu (równoważność strukturalna), preferując jawne / zadeklarowane podtypy (równoważność deklaracji)

Najczęściej używałem języków programowania, które używają jawnego podtytułu . Jakie są zalety ukrytego podtypu, jak opisano w uwagach powyżej.

pl.programming-languages type-theory Frankie Ribery
źródło

Z FAQ na temat zakresu tej wymiany: „Praca w tej dziedzinie często wyróżnia się naciskiem na technikę matematyczną i dyscyplinę”. Oddaję głos, ponieważ w odpowiedziach na to pytanie nie widzę miejsca na rygor.

David Eppstein

Niestety, odpowiedź na to pytanie jest o wiele bardziej rygorystyczna niż można się początkowo spodziewać. Wielu wybitnych ludzi paliło wiele lat 90. zmagając się z pozornie trywialnymi pytaniami o subtypy. Niestety jest to obszar o bardzo złym stosunku nakładu do nagrody.

Neel Krishnaswami,

Tak, tam jest dużo miejsca na matematyce i dyscypliny w odpowiedzi na to pytanie, lub przynajmniej wyjaśnić matematycznie co ukryte podtypów jest . Nie jestem pewien stosunku wysiłku do nagrody.

Noam Zeilberger,

Prawdopodobnie powinienem był powiedzieć, że to „bardzo trudne”, ponieważ po zastanowieniu zdaję sobie sprawę, że jestem bardzo zainteresowany odpowiedziami.

Neel Krishnaswami

Ok, jestem przekonany. Chciałbym usunąć moją opinię, ale system mi na to nie pozwala.

David Eppstein

Odpowiedzi:

Krótka odpowiedź brzmi „zweryfikować dodatkowe właściwości istniejącego kodu”. Następuje dłuższa odpowiedź.

Nie jestem pewien, czy „domyślna” kontra „wyraźna” jest dobrą terminologią. To rozróżnienie jest czasem nazywane podtypem „strukturalnym” vs. Istnieje również drugie rozróżnienie w możliwych interpretacjach podtypu strukturalnego (krótko opisanych). Zauważ, że wszystkie trzy interpretacje podtypów są w rzeczywistości ortogonalne, więc nie ma sensu porównywanie ich ze sobą, zamiast zrozumienia ich zastosowania.

Głównym rozróżnieniem operacyjnym w interpretacji strukturalnego stosunku podsieci A <: B jest to, czy świadczy o tym rzeczywisty przymus z treścią obliczeniową (środowisko uruchomieniowe / kompilacja), czy też może być świadkiem przymusu tożsamości. Jeśli to pierwsze, ważną właściwością teoretyczną, którą musi się zachować, jest „spójność”, tj. Jeśli istnieje wiele sposobów wykazania, że A jest podstrukturalnym podtypem B, każda z towarzyszących koercji musi mieć tę samą treść obliczeniową.

Podany link wydaje się mieć na uwadze drugą interpretację podtypu strukturalnego, w której A <: B można zaobserwować poprzez przymus tożsamości. Jest to czasami nazywane „interpretacją podzbioru” podtypu, biorąc naiwny pogląd, że typ reprezentuje zestaw wartości, a więc A <: B na wszelki wypadek, gdy każda wartość typu A jest również wartością typu B. Jest to również czasem nazywany „pisaniem na uszlachetnianiu”, a dobrym tekstem do przeczytania na temat oryginalnej motywacji są typy wyrafinowania Freeman & Pfenning dla ML . Aby zapoznać się z najnowszym wcieleniem w języku F #, przeczytaj Bengston i in., Typy wyrafinowania dla bezpiecznych implementacji. Podstawową ideą jest wzięcie istniejącego języka programowania, który może (ale nie musi) już mieć typy, ale w którym typy nie gwarantują aż tyle (np. Tylko bezpieczeństwa pamięci), i rozważenie drugiej warstwy typów, wybierając podzbiory programów z dodatkowe, bardziej precyzyjne właściwości.

(Teraz argumentowałbym, że teoria matematyczna leżąca u podstaw tej interpretacji podtypów wciąż nie jest tak dobrze rozumiana, jak powinna być, a być może dlatego, że jej zastosowania nie są tak powszechnie doceniane, jak powinny. Jednym z problemów jest to, że zestaw interpretacja typów "jest zbyt naiwna, dlatego czasami jest raczej porzucana niż dopracowywana. Na inny argument, że ta interpretacja podtypów zasługuje na więcej uwagi matematycznej, przeczytaj wprowadzenie do Podprzestrzeni Paula Taylora w abstrakcyjnym dualności kamienia .)

Noam Zeilberger
źródło

Cześć Noam, fajna odpowiedź! Dodam, że nominalne podporządkowanie a la OO jest zasadniczo sposobem na zdefiniowanie klasy przymusów nieidentyfikujących, które są jednak realizowane przez brak operacji. Oznacza to, że podtypowanie szerokości obiektów wywołanych przez dziedziczenie formalnie wiąże się z przymusem braku tożsamości (np. Przymus

oznacza wyrzucenie

), ale poprzez sekwencyjne układanie zapisów w pamięci może używać tego samego kodu binarnego do wyświetlania komponentów

dla obu typów.

A \times B \times C <: A \times B

$A \times B \times C <: A \times B$

C

$C$

A

$A$

B

$B$

Neel Krishnaswami

Optymalizacja układu pamięci polega na tym, aby optymalizować układ pamięci, więc koercje, które są tożsamościami, powinny naprawdę być wynikiem optymalizacji.

Andrej Bauer,

więc tylko dla wyjaśnienia komentarza Andreja w odniesieniu do mojej odpowiedzi, w interpretacji piszącej na maszynie, relacje podsieci są zawsze obserwowane przez przymus tożsamości z definicji , ponieważ typy dopracowania nie zawierają żadnej dodatkowej treści obliczeniowej. Innymi słowy, jeśli A i B są dwoma udoskonaleniami („podzbiorami” / „właściwościami”) typu wartości X, A <: B zapewnia, że dla każdej wartości x w X, jeśli x: A, to także x: B. Takie oświadczenie można zweryfikować lub sfałszować, ale nie ma ono wpływu na środowisko wykonawcze, ponieważ dowody, że x: A i x: B nie istnieją w czasie wykonywania.

Noam Zeilberger

@Noam: Zgadzam się, ale tylko wtedy, gdy mówimy o metateheorii jednego języka, a nie, jeśli mówimy o kompilacji. Koercje tożsamościowe mogą być realizowane przez procedury, które wykonują dużo pracy, a koercje nieidentyfikacyjne mogą być realizowane przez procedury, które nic nie robią. Konkretnie, załóżmy, że mamy typ

i udoskonalenie

N

$\mathbb{N}$

. Następnie moglibyśmy zaimplementować elementy udoskonalenia za pomocą jednego rozpakowanego słowa, nawet jeśli pełny typ wymaga alokacji pamięci do reprezentowania. Wymuszone tu tożsamości muszą być zrealizowane przez prawdziwe obliczenia.

{x : N | x < 2^{32}}

$\{x:N\;\;|\;\;x < 2^{32}\}$

Neel Krishnaswami

N

$N$

{x : N | x < 2^{32}}

$\{x:N | x < 2^{32}\}$

N

$N$

{x : N | x < 2^{32}}

$\{x:N | x < 2^{32}\}$

Noam Zeilberger

Ta odpowiedź jest rodzajem minimalnego uzupełnienia doskonałej odpowiedzi Noama. Jednym z interesujących danych jest los koncepcji C ++, które powstały w wyniku próby ujednolicenia nominalnych i strukturalnych pojęć typu.

Tutaj jest doskonały opis, z linkami do wielu istotnych dyskusji: http://bartoszmilewski.wordpress.com/2010/06/24/c-concepts-a-postmortem/

Jednak powyższy zapis nie omawia szczegółowo kwestii nominalnej vs. strukturalnej. Jest tu kolejny napis: http://nerdland.net/2009/07/alas-concepts-we-hardly-knew-ye/

Kluczowym dokumentem, na który oba wskazują, jest „Uproszczenie użycia pojęć” Bjarne'a Stroustrupa: http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2009/n2906.pdf , który zawiera praktyczne problemy napotkane dogłębnie.

Dyskusja jako całość jest bardziej pragmatyczna niż rygorystyczna. Daje to jednak dobry wgląd w rodzaje kompromisów związanych z tymi zagadnieniami, szczególnie w kontekście dużego istniejącego języka.

sclv
źródło