Зависимые типы?

Question

[Александр Рулёв]

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


Однако может кто-нибудь пояснить, в чём профит? Ну и вообще объяснить, что происходит. Какие-то доказательства, верификации, что это даёт? По ссылке той статьи, как я понял, мы имеем две штуки — алгоритм сортировки (неизвестно какой) и доказательство, что он (точно он?) верный.


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

Comments

[leventov]

Я сам не разбирался с ними, но есть подозрение, что на пальцах все равно не понять, надо прочувствовать. Например есть статья на вики «Зависимые типы», которую вы наверное уже читали, но ясности не прибавилось. Поэтому вряд ли на ваш вопрос можно так ответить. Читайте beust.com/weblog/2011/08/18/a-gentle-introduction-to-dependent-types/ www.slideshare.net/fprogru/haskell-15961414 и т. д.

Answer 1

[ymn]

Объясняю: математики заметили связь между программами и математическими доказательствами (тут читаем про изоморфизм Карри-Говарда). Так вот исчисление предикатов соответствует лямбда-исчислению с зависимыми типами.

Это объяснение на пальцах.

Подробнее читаем в учебнике Пирса «Типы в языках программирования».