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

24

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

Джон Сальватье
источник

Ответы:

22

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

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

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

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

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

Дэйв Кларк
источник
3
Спасибо, это именно то, что я искал. Теперь я задал пару вопросов о новичках, которые, кажется, были восприняты несколько лучше, хотя cstheory. SE не является подходящим местом для таких вопросов. По шкале от -5 до +5 вы бы поощряли или не поощряли подобные вопросы в будущем? В качестве примечания, насколько я понимаю (из чтения Роберта Харпера), классы типов являются подкатегорией модулей, верно?
Джон Сальватье
3
Этот вопрос находится справа от границы того, что подходит для cstheory.SE. Классы типов на самом деле не являются подкатегорией модулей. Это больше похоже на то, что классы типов - это модули + вывод типов + free_plumbing.
Дейв Кларк
2
Я полагаю, что вы всегда можете довольно легко смоделировать / смоделировать подтип с зависимыми типами. Например, в Haskell HList (который построен только на разрешимом равенстве типов) дает вам подтип (см. «Система пропущенных объектов Haskell»). Единственная сложная часть о подтипировании - это вывод типов, и как только вы работаете с зависимыми типами, вы все равно отбрасываете 90% этого.
sclv
(изменено с комментария на ответ)
Нил Кришнасвами
Теория подмножеств теории типов Мартина-Лофа - это в основном то, что вам нужно для моделирования структуры забвения, и это восходит к 1980-м годам. Я думаю, что это то, что @Neel получает в своем ответе.
Чарльз Стюарт
22

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

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

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

SP(x)x:

X<:Yx:Xx:YP(x)P(x)

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

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