Rulexec
@Rulexec
Метатеоретик теории типов

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

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


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


В общем, объясните пожалуйста, что такое зависимые типы, как они работают и причём тут доказательства. Спасибо.
  • Вопрос задан
  • 4557 просмотров
Решения вопроса 1
ymn
@ymn
Объясняю: математики заметили связь между программами и математическими доказательствами (тут читаем про изоморфизм Карри-Говарда). Так вот исчисление предикатов соответствует лямбда-исчислению с зависимыми типами.

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

Подробнее читаем в учебнике Пирса «Типы в языках программирования».
Ответ написан
Комментировать
Пригласить эксперта
Ваш ответ на вопрос

Войдите, чтобы написать ответ

Войти через центр авторизации
Похожие вопросы