π 1 : A × B → A π 2 : A × B → B
Это не так удивительно, хотя естественное чтение типа F - это пара с исключением в стиле let , потому что два вида пары взаимозависимы в интуиционистской логике.
Теперь в теории зависимых типов с нечетким количественным определением вы можете следовать тому же шаблону для кодирования зависимого типа записи as
Однако, если теория типов является параметрической, вы можете использовать параметричность, чтобы показать, что определимо. Кажется, это известно - см., Например, эту разработку Agda Дэна Доэла, в которой он выводит ее без комментариев, - но я не могу найти ссылку на этот факт.
Кто-нибудь знает ссылку на тот факт, что параметричность позволяет определять проективные исключения для зависимых типов?
РЕДАКТИРОВАТЬ: Самая близкая вещь, которую я нашел до сих пор, это статья 2001 года Германа Гойверса, « Индукция» не выводима в теории зависимых типов второго порядка , в которой он доказывает, что вы не можете сделать это без параметризации.
источник
Ответы:
Я только что поговорил с Дэном Доэлом, и он объяснил, что на самом деле он упоминал Нила Кришнасвами. Он увидел ваш комментарий о n-cafe, что можно сделать сильную индукцию, используя параметричность, поэтому он пошел дальше и сделал это в качестве упражнения, не понимая, что выполнение этого для сигмы, по-видимому, является новым результатом.
Точная цитата: «Моя ссылка была на него. Я думал, он сказал, что это возможно, поэтому я сделал это».
источник