Дают ли зависимые типы все, что делает подтип?

Типы и языки программирования довольно сильно фокусируются на подтипах, но, насколько я могу судить, подтипы не кажутся особенно фундаментальными. Дает ли подтип что-то большее, чем зависимые типы? Работа с зависимыми типами должна быть более трудоемкой, поэтому я могу понять, почему подтипы могут быть полезны на практике. Однако меня больше интересует теория типов как основа математики, а не основа языков программирования. Должен ли я уделять много внимания подтипам?

lo.logic pl.programming-languages type-theory Джон Сальватье
источник

Ответы:

Подтипы и зависимые типы являются ортогональными понятиями.

Подтип обычно снабжен понятием подтипа, благодаря которому выражение одного типа может появиться в месте, где ожидается супертип.

Субтипирование, скорее всего, будет решаемо, и его легче будет реализовать при реализации.

Зависимая типизация гораздо более выразительна. Но если вы когда-нибудь захотите считать группу моноидом, вам нужно понятие подчинения, чтобы забыть о дополнительной структуре. Часто, например, при использовании Coq, создается тривиальное обязательное доказательство для борьбы с этим типом принуждения, поэтому на практике подтипирование может ничего не добавлять. Более важно иметь способы объединения различных теорий, чтобы сделать их многократно используемыми, например, повторное использование теории моноидов при разговоре о группах. Классы типов в Coq - недавнее новшество для таких вещей. Модули - более старый подход.

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

Дэйв Кларк
источник

Спасибо, это именно то, что я искал. Теперь я задал пару вопросов о новичках, которые, кажется, были восприняты несколько лучше, хотя cstheory. SE не является подходящим местом для таких вопросов. По шкале от -5 до +5 вы бы поощряли или не поощряли подобные вопросы в будущем? В качестве примечания, насколько я понимаю (из чтения Роберта Харпера), классы типов являются подкатегорией модулей, верно?

Джон Сальватье

Этот вопрос находится справа от границы того, что подходит для cstheory.SE. Классы типов на самом деле не являются подкатегорией модулей. Это больше похоже на то, что классы типов - это модули + вывод типов + free_plumbing.

Дейв Кларк

Я полагаю, что вы всегда можете довольно легко смоделировать / смоделировать подтип с зависимыми типами. Например, в Haskell HList (который построен только на разрешимом равенстве типов) дает вам подтип (см. «Система пропущенных объектов Haskell»). Единственная сложная часть о подтипировании - это вывод типов, и как только вы работаете с зависимыми типами, вы все равно отбрасываете 90% этого.

sclv

(изменено с комментария на ответ)

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

Теория подмножеств теории типов Мартина-Лофа - это в основном то, что вам нужно для моделирования структуры забвения, и это восходит к 1980-м годам. Я думаю, что это то, что @Neel получает в своем ответе.

Чарльз Стюарт

Однако меня больше интересует теория типов как основа математики, а не основа языков программирования. Должен ли я уделять много внимания подтипам?

Еще одна вещь, которую дает подтип, - это то, что подразум подразумевает, что множество свойств когерентности имеют место. Теория зависимого типа также нуждается в понятии неуместности доказательства, чтобы моделировать все, что вы можете делать с подтипами. Например, в теории зависимых типов вы можете приблизить формирование подмножества с зависимой записью:

{x \in S |; P (x)} vs. Σ x : S . P (x)

$\{x \in S \;|; P(x)\} \mbox{ vs. } \Sigma x:S.\;P(x)$

$S$ $P(x)$ $x:$

$X <: Y$ $x:X$ $x:Y$ $P(x)$ $P(x)$

Получив это, вы можете систематически разрабатывать подтипы в теории зависимых типов. См. Тезис Уильяма Ловаса для примера добавления подтипов к теории зависимых типов (в данном случае, Twelf).

Нил Кришнасвами
источник