По моему опыту, учебники и вводные материалы по теории типов (или системам конструктивной логики) на удивление лишены метафор. Я так и не нашел ни одного вводного текста в тех областях, которые развивались бы аналогично другим областям логики, основанным на теории множеств, где вы можете выбрать введение предмета «интуитивно» (метафорически) и постепенно продвигаться к более абстрактным и сухим подходам. .
Мой вопрос заключается в том, является ли это существенной лингвистической особенностью трактовки теории типов в текстах (другими словами, невосприимчивость к метафорам является эпистемологическим вопросом) или это просто предпочтительная, рекомендуемая теоретическая стратегия.
Я сомневаюсь, что это что-то существенное для теории типов как таковой; но в большей степени из-за повсеместного распространения математического и научного письма; искусство изложения, я думаю, было постепенно утрачено.
Лагранж, например, гордился тем, что в его математических работах не было диаграмм. Владимир Арнольд жаловался на чрезмерный бурбакистский подход к математике, который вместо того, чтобы прояснить основные идеи и обозначить значение, скорее скрыл все под толстой коркой формализма; большинство из которых скрыло то немногое, что было сказано.
Некоторые теории типов связаны с определенными категориями — например, просто типизированное лямбда-исчисление с закрытыми декартовыми категориями , и некоторые из них могут быть более естественно представлены в виде диаграмм струн; и их можно понять топологически естественным образом.
Я бы сказал, что это своего рода диаграммная аналогия.
В теории множеств элементы и множества являются базовыми; и выводится понятие функции; Теория топосов берет множества и функции (т.е. объекты и морфизмы) в качестве базовых; и элементы как производные: Ловер сказал, что хочет создать теорию множеств без элементов.
Это не совсем метафора и даже не аналогия, но она работает очень хорошо, переворачивая теорию множеств «с ног на голову»; подобно тому, как марксизм как экономическая философия перевернул Гегеля «с ног на голову». Можно назвать это лозунгом; возможно, даже «заявление о миссии».
Джозеф Вайсман
Андре Соуза Лемос