Практическая польза зависимых типов

Зависимые типы по выразительной силе эквивалентны проверяемым исключением (семантически это одно и то же, на самом деле).

Поясни мысль. Проверяемые исключения позволяют лишь указать типы исключений, которые может кидать код и запретить кидать исключения типов, которые не соответствуют этому списку.

Ты тупая, шлюшка?

Поясни мысль.

Давай на примере. Допустим, у нас есть зависимая ф-я деления, которая гарантирует, что у нее делитель будет ненулевой. Что вообще это по факту значит? Лишь то, что где-то сверху этого аргумента в результате ифа/паттерн-матчинга етц. мы разделили control-flow на две ветки исполнения, в одной из которых у нас аргумент будет гарантированно ненулевой, а во второй - нулевой, с-но все что делают зависимые типы - это гарантируют что подобные ситуации (деление на ноль, неравные длины списков и т.п.) будут обработаны. Но точно то же самое гарантируют и чекаемые исключения - если у тебя деление бросает исключение, то оно необходимо будет обработано.

Иными словами, любую программу с зависимыми типами можно переписать на языке с чекаемыми исключениями, при этом автоматически и так, что:

1. программа с исключениями чекается тогда и только тогда, когда чекается исходная программа с зависимыми типами

2. если программы чекаются, то результат их выполнения совпадает

В случае зависимых типов у тебя никаких ошибок уже не будет. Совсем. Тебе компилятор не даст написать код, который приведёт к делению на 0.

Что-то ты не то пишешь. Проверяемые исключения лишь заставят или обработать исключение или описать, что мы его прокидываем дальше. Они не гарантируют ничего. 0 все равно будет передан в функцию деления и никто не заставит проверить на ноль перед вызовом. Доцент Зависимые типы заставят.

Хотя если ты покажешь, как на проверяемых исключениях повторить код ТС, то будет здорово.

Ты неимоверно тупое жывотное. Ты не понимаешь зависимые типы. С зависимыми типами у тебя есть ДОКАЗАТЕЛЬСТВО, что аргумент ни в одном вызове не будет нулевым никогда.

В случае зависимых типов у тебя никаких ошибок уже не будет. Совсем. Тебе компилятор не даст написать код, который приведёт к делению на 0.

Чекаемые исключения тоже не дадут, о чем и речь.

Проверяемые исключения лишь заставят или обработать исключение или описать, что мы его прокидываем дальше.

Именно. То ровно то же самое, что заставят делать зависимые типы.

Они не гарантируют ничего.

Они гарантируют, так же как и зависимые типы, что ситуация с делением на ноль будет либо обработана внутри твоей ф-и (в catch-блоке вокруг деления) либо исключение будет прокинуто дальше (то есть компилятор будет знать что твоя ф-я потенциально может его бросить).

В случае зависимых типов все рвоно то же самое - либо ситуация с делением на ноль будет обработана (при помощи if'f или аналога), либо в типе ф-и будет указано, что ф-я принимает ненулевой аргумент.

С зависимыми типами у тебя есть ДОКАЗАТЕЛЬСТВО, что аргумент ни в одном вызове не будет нулевым никогда.

Точно так же как с проверяемыми исключениями, лол.

В зависимых типах ты с ф-ей ассоциируешь ее тип, который сообщает информацию об аргументах, в чекаемых исключениях - список исключений, которые она бросает. И там и там можно пробрасывать совершенно одинаковую информацию.

А ты - просто кретин, который не понимает, что такое зависимые типы.

Хотя если ты покажешь, как на проверяемых исключениях повторить код ТС, то будет здорово.

Элементарно же. Есть ф-я с зависимыми типами:

pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys с типом:

pairAdd : Num a => Vect n a -> Vect n a -> Vect n a

пишешь эту функцию так же, но форсируешь проброс исключений в том случае, когда чекер не должен принимать твой код:

pairAdd (x :: xs) (y :: ys) = if ((length x) = (length y)) then (x + y :: pairAdd xs ys) else throw YobaError

и добавляешь инфу об исключении в декларации ф-и:

pairAdd : (Num a; throws YobaError) => Vect a -> Vect a -> Vect a

Теперь рассмотрим код с зависимыми типами. Допустим, нам даны два списка и мы хотим эту функцию применить в своей новой функции, как-то так:

fun x y = pairAdd x y

у нас есть два способа как сделать так, чтобы чекер это дело пропустил теперь - либо сделать общий тип и поменять код вот так:

fun : Num a => Vect a -> Vect a -> Vect a
fun x y = if ((length x) = (length y)) then (pairAdd x y) else []

либо код не менять но указать ограничение на типы в самом fun:

fun : Num a => Vect n a -> Vect n a -> Vect n a

в случае с чекаемыми исключениями все то же самое. Код вида:

fun : Num a => Vect a -> Vect a -> Vect a
fun x y = pairAdd x y

мы либо сохраняя общий тип меняем код аналогичным зависимым типам образом:

fun : Num a => Vect a -> Vect a -> Vect a
fun x y = try {pairAdd x y} catch {yobaError => []}

fun : (Num a; throws yobaError) a => Vect a -> Vect a -> Vect a
fun x y = try {pairAdd x y} catch {yobaError => throw YobaError}

и любой код с зависимыми типами так, очевидно, переписывается (на самом деле нам понадобится иметь по типу исключений на каждый функциональный вызов, но это для автоматической конвертации не проблема, на самом деле)

Ты уебанище без мозга. Проверяемое исключение не даст тебе доказательства принадлежности аргумента функции к множеству (0,maxint].

Проблядок ты тупорылый, в языке с зависимыми типами такой код совершенно легален.

Чекаемые исключения тоже не дадут, о чем и речь.

Дадут. Им вообще насрать на твой код, они ничего не проверяют. Тебя просто обяжут указать этот(или базовый) exception и ничего болен. А деление на ноль произойти может.

Да это, по-ходу, тот же уебанец, который тут когда-то с пеной на еблище доказывал всем, что для формального доказательства надо перебирать всё множество вариантов входных значений. По стилю похож. Вряд ли этому грязному выблядку ты что-то сможешь втолковать, он явно шизофреник.

Проверяемое исключение не даст тебе доказательства принадлежности аргумента функции к множеству (0,maxint].

Вообще-то даст:

try {
if (pred(x)) throw YobaError;
...
}
catch {
YobaError => ...;
}

Ещзе раз - ты не понимаешь, как работают зависимые типы. Почитай уже что-нибудь на эту тему, потом кукарекай.

Я понимаю, когда человек чего-то не знает, но при этом пытается узнать. Воинствующее же невежество вроде твоего мне всегда было непонятно. Зачем повторять раз за разом заведомую ересь, если есть интернеты? Нагуглил, прочитал, перестал быть тупым мудаком. Почему ты упорно не желаешь перестать быть тупым мудаком?

Проблядок ты тупорылый, в языке с зависимыми типами такой код совершенно легален.

Нет, не легален. Попробуй написать его в агде и увидишь.

Как я выше и говорил - ты просто не знаешь, как работают зависимые типы.

Дадут.

Нет, не дадут. В том же смысле, в каком не дадут зависимые типы.

Тебя просто обяжут указать этот(или базовый) exception и ничего болен.

Но точно то же самое делают зависимые типы - они обязывают тебя описать ветку, в которой ты должен указать control-flow для нуля. Когда ветка нуля обработана - код допускается, когда ветка не обработана - код не допускается. Одинаково что в случае зависимых типов, что в случае исключений. Еще раз - любая программа с зависимыми типами переписывается на чекаемые исключения, автоматически, с сохранением семантики, с сохранением допускаем чекером множеств программ. Это математический факт, который устанавливает эквивалентность соовтетствующих систем. Я не понимаю чего ты тут пытаешься показать, если математически верно, что 2*2=4, то 2*2=4, а не 5, как не изворачивайся.

А деление на ноль произойти может.

Нет, не может. Будет брошено исключение и вычисление перейдет на 0-ветку, просто в другой момент. Но с точки зрения семантики мы эту разницу не сможем заметить, это вообще произойдет исключительно в рантайме. Результат же ф-и будет один и тот же и результат чека компилятора будет тоже один и тот же. Иными словами, если у тебя две программы, одна из которых с исключениями, другая с зависимыми типами + компилятор и вычислитель этих программ, то ты не сможешь определить какая из этих программ - какая, если только не заглянешь в код. Поведение программ совпадает.

Вообще я жду, пока ты все-таки прочиташеь, что такое зависимые типы, и поймешь свою ошибку. Я могу намекнуть - ты связываешь зависимые типы с доказательствами, а это неверно. Почитай описание конкретных систем, узнаешь, почему именно неверно и в каком смысле. Тогда поймешь, почему зависимые типы = исключения.

Не, другой. Все варианты входных значений - это петушиный царь анскильных лалок, а этот анонимный дегенерат - anonimous, динамический фанат жабаскрипта и ИО, специалист по альтернативным методам вычисления и отрицатель математики.

Кунсткамера из неудачных экземпляров деятельности абортария - наше всё.

У тебя детектор сломан.

специалист по альтернативным методам вычисления и отрицатель математики.

Наоборот - я хочу чтобы дебилы занялись самообразованием и прежде чем кукарекать про зависимые типы разобрались, что это такое и как работает. А то последнее время развелось много долбоебов, которые слышали звон, но не знают где он. Так что я как раз за классические методы вычисления и самую что ни на есть математику.

Пиздец ты ебанутый шизофреник!

По сути есть что ответить?

По сути, сучка, докажи для начала Тьюринг-полноту чекаемых исключений. Потому как зависимые системы типов Тьюринг-полные, и это самый простой способ показать, насколько ты ебанулся.

ЗЫ: ну а про изоморфизм Карри-Говарда ты вообще не слышал, очевидно.

Потому как зависимые системы типов Тьюринг-полные

Ни одна из систем лямбда-куба не обладает тьюринг-полнотой, если ты не в курсе, это во-первых.

Во-вторых, ты перепутал ЗТ с CoC. В ЗТ нету операторов над типами, по-этому вообще понятие «вычислений на уровне типов» (а значит и понятие тьюринг-полноты) для ЗТ неприменимо.

Это общеизвестные факты, которые ты бы, конечно, знал, если бы хоть немного разбирался в предмете, который пытаешься обсуждать.

Вот опять ты приплел некий баззворд, смысла которого не понимаешь. ЗТ сами по себе не имеют отношения к изоморфизму Карри-Говарда. Единственное, зачем нужен изоморфизм Карри-Говарда в контексте ЗТ и теорем прувинга - это чтобы иметь возможность типизировать П-типы некоего специального вида.

В общем ведь П-тип не содержит в себе аргумента-доказательства, как это делается в той же агде. Однако, любой П-тип можно заменить на эквивалентный (в определенном смысле, содержательно) П-тип так, что все зависимости перейдут на зависимость последнего аргумента от предыдущих (этот последний аргумент и называют «доказательством»). При этом тогда сам факт того что этот аргумент передан и будет доказательством того, что ф-я чекается - именно в этот момент и применяется изоморфизм Карри-Говарда, т.о. вместо того чтобы как нормальные люди доказывать корректность типизации при помощи теорем прувера, мы пишем терм с типом-доказательством и суем в ф-ю., выполняя кучу лишних действий.

Если работать с П-типами общего вида, изоморфизм Карри-говарда не нужен вообще - мы просто берем утверждения из типов и скармливаем их пруверу.