Неявный или явный подтип

Эта страница утверждает, что

многие языки не используют неявный подтип (структурная эквивалентность), предпочитая явный / объявленный подтип (декларационная эквивалентность)

Я в основном использовал языки программирования, которые используют явные подтипы . Каковы преимущества неявного подтипирования, как описано в примечаниях выше.

pl.programming-languages type-theory Фрэнки Рибери
источник

Из часто задаваемых вопросов о масштабах этого обмена: «Работа в этой области часто отличается акцентом на математическую технику и строгость». Я опускаю голос, потому что я не вижу возможности для строгости в ответах на этот вопрос.

Дэвид Эппштейн

К сожалению, для ответа на этот вопрос гораздо больше возможностей для строгости, чем вы могли бы изначально надеяться. Многие выдающиеся люди сожгли борьбу 90-х, видимо, тривиальные вопросы о подтипах. Это область с очень низким отношением усилий к вознаграждению, к сожалению.

Нил Кришнасвами

да, есть много места для математики и строгости, отвечая на этот вопрос, или по крайней мере объяснить математически , что неявное подтипов является . Я не уверен насчет соотношения усилий и вознаграждений.

Ноам Цайлбергер

Я, наверное, должен был просто сказать, что это «очень тяжело», так как, подумав, я понимаю, что мне очень интересны ответы.

Нил Кришнасвами

Хорошо, я убежден. Я бы убрал свое понижение, но система не позволила мне.

Дэвид Эппштейн

Ответы:

Краткий ответ - «проверить дополнительные свойства существующего кода». Более длинный ответ следует.

Я не уверен, что «неявный» против «явный» является хорошей терминологией. Это различие иногда называют «структурным» и «номинальным» подтипом. Тогда есть и второе различие в возможных интерпретациях структурных подтипов (описано ниже). Обратите внимание, что все три интерпретации подтипов действительно ортогональны, и поэтому не имеет смысла сравнивать их друг с другом, вместо того, чтобы понимать использование каждого из них.

Основное операционное различие в интерпретации отношения структурного подтипа A <: B состоит в том, засвидетельствовано ли оно реальным принуждением с вычислительным контентом (во время выполнения / времени компиляции), или оно может быть засвидетельствовано насильственным принуждением. Если первое, важное теоретическое свойство, которое должно соблюдаться, - это «когерентность», т. Е. Если есть несколько способов показать, что A является субструктурным подтипом B, каждое из сопутствующих приведений должно иметь одинаковое вычислительное содержание.

Ссылка, которую вы дали, похоже, имеет в виду вторую интерпретацию структурного подтипа, где A <: B может быть засвидетельствовано принуждением к идентичности. Это иногда называют «интерпретацией подмножества» подтипов, принимая наивное представление о том, что тип представляет набор значений, и поэтому A <: B на всякий случай, когда каждое значение типа A также является значением типа B. Это также иногда называемый «типизацией уточнения», и хорошая статья для оригинальной мотивации - это « Уточнение типов» Фримена и Пфеннинга для ML . Для более позднего воплощения в F # вы можете прочитать Bengston и др., Типы уточнения для безопасных реализаций., Основная идея состоит в том, чтобы взять существующий язык программирования, который может (или может не иметь) уже иметь типы, но в которых типы не гарантируют всего этого (например, только безопасность памяти), и рассмотреть второй уровень типов, выбирающий подмножества программ с дополнительные, более точные свойства.

(Теперь я бы сказал, что математическая теория, лежащая в основе этой интерпретации подтипирования, все еще не так хорошо понята, как следовало бы, и, возможно, это связано с тем, что ее использование не так широко ценится, как следовало бы. интерпретация типов слишком наивна, и поэтому иногда от нее отказываются, а не уточняют. Для еще одного аргумента, что эта интерпретация подтипов заслуживает большего математического внимания, прочитайте введение к подпространствам Пола Тейлора в книге «Абстрактная каменная двойственность» .)

Ноам Цайлбергер
источник

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

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

C

$C$

A

$A$

B

$B$

Задача оптимизатора состоит в том, чтобы определить оптимальное расположение памяти, поэтому принуждения, которые являются идентичностями, действительно должны быть результатом оптимизации.

Андрей Бауэр

так что просто чтобы прояснить комментарий Андрея относительно моего ответа, в интерпретации типизации уточнения отношения подтипов всегда засвидетельствованы приведением идентичности по определению , потому что типы уточнения не несут дополнительного вычислительного содержания. Другими словами, если A и B являются двумя уточнениями («подмножествами» / «свойствами») типа значений X, A <: B утверждает, что для каждого значения x в X, если x: A, то также x: B. Такое утверждение может быть проверено или сфальсифицировано, но оно не имеет никакого эффекта во время выполнения, поскольку доказательства того, что x: A и x: B не существуют во время выполнения.

Ноам Цайлбергер

N

$\mathbb{N}$

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

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

N

$N$

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

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

N

$N$

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

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

Ноам Цайлбергер

Этот ответ является своего рода минимальным дополнением к отличному ответу Ноама. Интересным моментом для данных является судьба концепций C ++, которые основывались на попытке объединения номинальных и структурных понятий типа.

Здесь есть отличная рецензия со ссылками на большую часть соответствующей дискуссии: http://bartoszmilewski.wordpress.com/2010/06/24/c-concepts-a-postmortem/

Тем не менее, приведенная выше статья не обсуждает номинальную и структурную проблему в какой-либо глубине. Здесь есть еще одна статья, которая делает: http://nerdland.net/2009/07/alas-concepts-we-hardly-knew-ye/

Ключевым документом, на который указывают оба документа, является «Упрощение использования концепций» Бьярна Страуструпа: http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2009/n2906.pdf , который входит в практическую проблемы встречаются в некоторой глубине.

В целом дискуссия скорее прагматичная, чем строгая. Тем не менее, это дает хорошее представление о видах компромиссов, связанных с этими вопросами, особенно в контексте большого существующего языка.

sclv
источник