Alexey Veselovsky писал(а):
Geniepro писал(а):
В языках с зависимыми типами неправильная программа не скомпилируется, даже если в ней нет синтаксических ошибок. Вот неправильный алгоритм, и всё тут, так чего его запускать на выполнение...
Гм. А пример можно? Например для каких-нибудь простых алгоритмов типа сортировки.
И вообще, откуда оно будет знать какой алгоритм правильный а какой нет?
Why Dependent Types Matter -- эта статья, наверное, лучше меня ответит на эти вопросы.
К сожалению, она не только на английском, но ещё и использованный в ней язык программирования (Epigram) черезчур непривычен большинству программистов, многие из которых простой двухмерный синтаксис таких языков, как Occam, Haskell, Python или F# не переваривают, а в этом Epigram использована какая-то экстремальная форма двухмерного синтаксиса...
В пятом параграфе статьи описывается, как с помощью зависимых типов можно специфицировать функцию сортировки списка, точнее указать, что результат сортировки -- упорядоченный список, что даёт компилятору возможность проверить или отвергнуть реализацию функции на соответствие спецификации.
ЗЫ. Я сам пока не имею опыта в теме зависимых типов, только начинаю потихоньку изучать это дело. Приведу, как я сам сейчас понимаю процесс разработки программ с зависимыми типами...
Вот из-за чего были недовольны бейсик программисты паскалем, или более общий случай -- что не нравится "динамическим" программистам в языках со статической типизацией?
"Динамисты" привыкли к тому, что могут сразу же "броситься в бой", начать разработку программы, по ходу дела уточняя или переделывая её. А в языках со статической типизацией программист должен сначала перечислить переменные, указать их типы, то есть провести какой-то анализ задачи, и только потом начать делать программу. (Языки с выводом типов и особенно хаскельного семейства немного облегчают это бремя.)
Зависимые типы ещё более ужесточают начальный этап -- нужно не просто указать тип функции, но и специфицировать какие-нибудь свойства алгоритма. Т.е. фактически нужно выдвинуть некоторую теорему о свойствах функции, и компилятор, являющийся по совместительству системой доказательства теорем, попытается верифицировать реализацию функции.
Естественно, такой подход не поможет в случаях, когда спецификация алгоритма неправильная или неполная -- у компилятора просто не будет информации о том, что должен делать этот алгоритм...
Вот в этом недостаток такого подхода -- от заказчика не добиться вменяемого ТЗ, а если и добьёшься -- оно постоянно меняется. Как тут какие-то формальные спецификации определить, теоремы о свойствах программы выдвинуть?..