Как извлечь второй элемент сигмы в исчислении построений?

Я пытаюсь сделать это следующим образом:

λ (A : *) ->
λ (B : (A -> *)) ->
λ (t : (∀ (r : *) -> (∀ (x : a) -> (B x) -> r)) -> r) ->
(t (B (t A (λ (x : A) -> λ (y : (B x)) -> x)))
    (λ (x : A) -> λ (y : (B x)) -> y))

Обратите внимание: поскольку значение, возвращаемое этой функцией, зависит от значения внутри самой сигмы, мне нужно извлечь это значение. Этот код не проверяет, потому что я считаю, что он не может унифицировать тип, извлеченный из Sigma, с типом внутри него.

Есть ли обходной путь?


functional-programming haskell idris coq agda
person MaiaVictor    schedule 13.05.2017    source источник
comment
Думаю, без зависимого исключения это невозможно. Церковные кодировки в CoC допускают только независимое исключение, IIRC. Индуктивные типы (как в CiC), конечно, позволяют это. (Возможно, типы Self также позволяют лучше кодировать, включая зависимое исключение)   -  person chi    schedule 14.05.2017
comment
@chi ... блин. Но как это поможет? Я много думал об этом, и у меня нет творческих возможностей.   -  person MaiaVictor    schedule 14.05.2017
comment
При зависимом исключении тип возвращаемого значения r не является типом *, а является семейством типов r :: (x:a) -> B x -> *, позволяющим второй проекции иметь желаемый тип. Проверить, например, книга HoTT на страницах 31-32 для некоторого обсуждения типов сигм, а также зависимого и независимого исключения.   -  person chi    schedule 14.05.2017
comment
Мне действительно нужно прочитать книгу о HoTT, @chi. В частности, есть ли у вас что-нибудь еще, что я могу посоветовать мне почитать в свободное время? При том, что вы знаете более или менее то, о чем я прошу.   -  person MaiaVictor    schedule 14.05.2017
comment
Хотелось бы, чтобы было несколько исчерпывающих книг / статей для обобщения основных результатов теории типов - литература слишком скудная :-( В любом случае, мне лично понравился ITT Мартина-Лофа примечания и книга HoTT. Кроме того, Видео Роберта Харпера хороши. Также полезна книга Barendregt Typed Lambda Calculi.   -  person chi    schedule 14.05.2017
comment
@chi, это серьезная проблема! Я не могу дождаться убийственного DApp, который сделает научные знания тем же, что Youtube сделал с креативным контентом. Википедия - это скорее архив. Универсальный способ говорить о математике в целом, что-то, что легко выбрать и поделиться. Бумаги - отстой. Серьезно, их слишком много. На переваривание статьи, которую в конечном итоге можно было бы объяснить несколькими предложениями после расшифровки, уходит несколько недель. (Вздыхает.) Спасибо за рекомендации.   -  person MaiaVictor    schedule 15.05.2017
comment
Теоретически для этого и предназначены обзорные статьи: вы берете результаты из многих статей и резюмируете ключевые моменты каждой из них. На практике материала слишком много. Даже книги не рассказывают всей истории. И, да, иногда вам нужно потратить слишком много времени на технические детали, чтобы получить общее представление. Я нормально отношусь к тому, что мне нужно много времени, чтобы переварить какой-то результат, но не тогда, когда мне нужно много времени только для того, чтобы увидеть, является ли бумага P тем, что я искал (особенно когда спросить какого-нибудь эксперта по SE быстрее :-( ...)   -  person chi    schedule 15.05.2017
comment
@chi вздыхает, могу я задать еще один вопрос, обещаю? Причина, по которой я ищу эти вещи, заключается в том, что мне нужно простое ядро, достаточно выразительное, чтобы доказать многие вещи. Причина в том, что я бы скомпилировал его в JS и EVM (Ethereum) и с его помощью смогу изучить и изучить концепцию доказательства вещей о моих реальных программах. Существующие языки (coq / idris / agda) не работают, потому что они не компилируются для этих целей удовлетворительно. Сам CoC этого не делает, потому что он недостаточно выразителен (индукция и т. Д.). Что бы вы сделали? Мне сейчас не нужна PHD TT. Я могу программировать ядро ​​- это все, что мне нужно!   -  person MaiaVictor    schedule 15.05.2017
comment
Я не могу рекомендовать конкретный фреймворк. Либо вы пытаетесь скомпилировать CiC, либо использовать дополнительные аксиомы CoC + для зависимого исключения (или какой-то вариант ITT Мартина-Лёфа ...?). Может быть, вам стоит попробовать спросить о CS или TCS, где более опытные люди могут предоставить информацию.   -  person chi    schedule 15.05.2017