Полиномиальный функтор (теория типов)

В теории типов полиномиальный функтор (или контейнерный функтор ) — это своего рода эндофунктор категории типов , тесно связанный с понятием индуктивных и коиндуктивных типов. В частности, все W-типы (соответственно M-типы) являются (изоморфными) исходным алгебрам (соответственно конечным коалгебрам ) таких функторов.

Полиномиальные функторы изучались в более общей ситуации претопоса с Σ-типами; в этой статье рассматриваются только приложения этой концепции внутри категории типов теории типов стиля Мартина-Лёфа .

Определение

Пусть U — вселенная типов, пусть A : U и пусть B : A → U — семейство типов, A. индексированных Пару ( A , B ) иногда называют подписью. или контейнер . Полиномиальный функтор, связанный с контейнером ( A , B ), определяется следующим образом:

${\begin{aligned}P:U&\longrightarrow U\\X&\longmapsto \sum _{a:A}(B(a)\to X)\end{aligned}}$

Любой функтор, естественно изоморфный P , называется контейнерным функтором . Действие P на функции определяется формулой

${\begin{aligned}P^{*}:(X\to Y)&\longrightarrow (P^{*}X\to P^{*}Y)\\(f,(a,g))&\longmapsto (a,g\circ f)\end{aligned}}$

Обратите внимание, что это присвоение действительно функториально не только в теориях экстенсиональных типов (см. #Properties ).

Характеристики

В теориях интенсионального типа такие функции не являются настоящими функторами, поскольку тип универсума не является строго категорией (область теории гомотопических типов посвящена исследованию того, как тип универсума ведет себя скорее как более высокая категория ). Однако он функториален с точностью до пропозициональных равенств, то есть обитаются следующие типы идентичности:

${\begin{aligned}P^{*}(f\circ g)&=P^{*}f\circ P^{*}g\\P^{*}({\mathsf {id}}_{X})&={\mathsf {id}}_{PX}\end{aligned}}$

для любых функций f и g и любого типа X , где ${\mathsf {id}}_{X}$ — функция типа X. тождественная

Ссылки

• Эбботт, Майкл; Альтенкирх, Торстен; Гани, Нил (2005). «Контейнеры: построение строго положительных типов» . Теоретическая информатика . 342 (1): 4. CiteSeerX   10.1.1.166.34 . дои : 10.1016/j.tcs.2005.06.002 .
• Аренс, Бенедикт; Каприотти, Паоло; Спадотти, Режис (12 апреля 2015 г.). Необоснованные деревья в гомотопической теории типов . Международные труды Лейбница по информатике (LIPIcs). Том. 38. стр. 17–30. arXiv : 1504.02949 . doi : 10.4230/LIPIcs.TLCA.2015.17 . ISBN  9783939897873 . S2CID   15020752 .
• Программа Uniвалентных фондов (2013). Гомотопическая теория типов: одновалентные основы математики . Институт перспективных исследований. п. 159.
• Аводи, Стив; Гамбино, Никола; Соякова, Кристина (18 января 2012 г.). «Индуктивные типы в теории гомотопических типов». arXiv : 1201.3898 [ math.LO ].
• Аводи, Стив; Гамбино, Никола; Соякова, Кристина (21 апреля 2015 г.). «Гомотопически-начальные алгебры в теории типов». arXiv : 1504.05531 [ math.LO ].

Внешние ссылки

• Обширная коллекция заметок о полиномиальных функторах.