В статье Simpler, Easier! утверждается, что можно кодировать системы зависимых типов даже без присутствия «Pi», то есть вы можете повторно использовать конструктор Lam для него. Но как это может быть верно, если в некоторых случаях «Пи» и «Лам» рассматриваются по-разному?Действительно ли можно удалить «Pi» из Исчисления Конструкций?
Кроме того, может быть удалена «Звезда»? Я думаю, вы могли бы заменить все его появления на «λ x. X» (id).
Это просто перегрузка, как (a, b) в Haskell: это может быть как тип, так и значение. Вы можете использовать одно и то же связующее для Π и λ, и typechecker определит контекст, который вы имеете в виду. Если вы typecheck одно связующее вещество против другого, то первое является λ и последний Π - и именно поэтому вы не можете однозначно заменить * с λ x . x - потому что тогда бывший Связующее может быть Π и последний * (* в качестве связующего не имеет никакого смысла для меня). Существует большая проблема с ∀ = λ и * = λ x . x: по транзитивности * = ∀ x . x, что является обычным способом постулирования False - этот тип должен быть необитаемым в звуковой системе, поэтому у вас не будет никаких типов вообще.
Был недавний поток на Кок-клубе «Сходство между FORALL и весело» (gmane.org не дает мне «Нет такого сообщения», это только у меня?), Вот некоторые выдержки:
Dominic Маллиган:
А вот еще с небольшой список литературы, указывающие на аналогичные работы:
http://www.macs.hw.ac.uk/~fairouz/forest/papers/journals-publications/jfp05.pdf
По иронии судьбы, согласно этой статье Кокванд впервые представил Исчисление Конструкции с единым унифицированным связующим, согласно соглашению , установленному De Bruijn в AutoMath.
Торстен Altenkirch:
Функция и ее тип очень разные понятия, даже если они имеют некоторые поверхностные синтаксические сходства.
Специально для новичка эта идентификация очень запутанна и полностью вводит в заблуждение. Я думаю, что нужно понимать теоретические концепции, исходя из того, что они означают, а не как они выглядят.
Андреас Абель:
Мой студент Матиас Benkard также работал на такой системе, в разделе "Тип Проверка без типов"
Обратите внимание, что система, описанная в первой ссылке, имеет Π-редукцию (т.е.вы можете применять pi-типы так же, как lambdas) - ваша система тоже будет иметь это, если вы объедините Π и λ внутренне (в отличие от синтаксически). А система, описанная на второй линии унифицирует типы и значения
Непосредственным следствием этого является отсутствие каких-либо различий между типов и их жителей: Каждое значение представляет собой тип, содержащий себя и все его части; и, наоборот, каждый тип представляет собой составное значение , состоящее из его жителей.
так есть на самом деле только одно связующее (для let и, может быть, за исключением fix).
Извините, я не понимаю, как вы можете знать, когда это должно быть Pi, и когда это должно быть λ по контексту. Не могли бы вы немного разобраться в этом различии? – MaiaVictor
В качестве простого примера используется «λ (a: *) -> λ (x: a) -> a'. Что случилось бы? Поскольку 'a: *' и все это тип, не будет ли этот термин принимать все? – MaiaVictor
@ Viclib, у меня есть небольшая инструкция для базовой теории зависимых типов, я попытаюсь объединить 'Π' и' λ'. Если у вас есть '[a: *] -> [x: a] -> a', и вы применяете его к себе, тогда первое связующее действует как лямбда, а результат - [[x: [a: *] -> [x: a] -> a] -> a'. – user3237465