Формализуем изоморфизм Карри-Говарда на Agda

Nick Yurchenko
Jul 21, 2017 · 1 min read

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

сделать_Δ_из : Список Φ → Список Связка
сделать_Δ_из формулы =
отобразить (λ φ → ("x_" конкатенировать φ встроку) типа Φ→Π φ)
на формулы

Фулл версия (для нашего и вашего увеселения):

http://zelinskiy.github.io/agda/%D0%A4%D0%9E%D0%A0%D0%9C%D0%90%D0%9B%D0%98%D0%97%D0%A3%D0%95%D0%9C_%D0%98%D0%97%D0%9E%D0%9C%D0%9E%D0%A0%D0%A4%D0%98%D0%97%D0%9C_%D0%9A%D0%90%D0%A0%D0%A0%D0%98-%D0%93%D0%9E%D0%92%D0%90%D0%A0%D0%94%D0%90_%D0%92_AGDA.html

)
    Nick Yurchenko
    Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch
    Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore
    Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade