Я только начинаю изучать Haskell, после того, как пришел из миров JavaScript / Ruby. Я наткнулся на https://github.com/HoTT и книгу по теории гомотопических типов , которую я очень хочу прочитать.
Тем не менее, я буду изучать понятия математики и теории типов по мере продвижения, поэтому, похоже, пройдет много времени, прежде чем я пойму, что теория гомотопического типа будет значить для практикующего программиста.
Не могли бы вы описать, какое влияние теория гомотопического типа окажет на программирование на практике для непрофессионала? Например, облегчит ли писать некоторые вещи? Если да, какие вещи? Или это позволит вам делать новые вещи в программировании, которые раньше были невозможны? Если да, какие вещи?
Спасибо, с нетерпением жду, чтобы обернуть мою голову на более базовом уровне.
источник
Ответы:
Одна из мощных вещей, которые компиляторы могут сделать на этапе оптимизации, - это заменить неэффективные представления эквивалентными. Например, в Haskell вы можете использовать ленивый список для вычисления суммы чисел, но компилятор GHC Haskell распознает, что это эквивалентно использованию итерации с временной переменной. Таким образом, вы получаете возможность программировать на основе простой абстракции, которую легко рассуждать, в то время как ваш исполняемый файл использует преимущества представления, лучше подходящего для аппаратной платформы (а это оказывается гораздо сложнее рассуждать в масштабе).
Однако эквивалентности, известные компилятору, в основном ограничиваются хорошо известными и исследованными структурами данных, такими как объединение потоков для списков. Вы можете определить свои собственные эквиваленты в исходном коде (используя пару функций преобразования, которые составляют идентичность в любом направлении), но вам придется применять их вручную, и может быть сложно выбрать правильный тип для использования во всех местах. во избежание чрезмерных конверсий.
Теперь давайте представим мир, в котором вы можете определить «высшие индуктивные типы», скажем, каноническую карту поиска. Этот тип имеет несколько конструкторов для различных типов карт: двоичный поиск, AVL, красно-черный, Trie, Patricia и т. Д. Наряду с типичными конструкторами данных вы также определяете тип эквивалентности, фиксирующий, возможно, множественные преобразования между этими представлениями, где разные преобразования предлагают различные измерения эффективности (т. е. время и память).
Что если бы компилятор мог использовать это понятие для прозрачного переписывания представлений карты, так же, как это можно сделать сегодня с объединением списков? Между тем, в вашем коде вы получаете работу с конструкцией, о которой проще всего рассуждать (и облегчающей работу по проверке, если вы находитесь в такой среде). Это может звучать так же, как абстрактные интерфейсы с несколькими реализациями, но оно включает в себя свободу выбора любой реализации и позволяет компилятору прозрачно заменять другую по мере необходимости, не влияя на смысл программы.
HoTT дает нам теоретическое обоснование типа, чтобы оправдать этот причудливый механизм переписывания и эти богато определенные типы, потому что он продвигает понятие эквивалентности эквивалентности равенству. Еще неизвестно, как это будет на самом деле реализовываться на практике, но это дает нам теоретическую основу, на которой можно основывать будущую работу.
источник