Что делает систему типов Haskell более "мощной", чем системы типов других языков?

Question

Чтение недостатков системы типов Scala по сравнению с Haskell? Я должен спросить: что именно делает систему типов Haskell более мощной, чем системы типов других языков (C, C++, Java). Очевидно, даже Scala не может выполнять некоторые из тех же полномочий, что и система типов Haskell. Что именно делает систему типов Хаскелла (вывод типа Хиндли-Милнера) настолько мощной? Можете привести пример?

Answer 1

Что именно делает систему типов Хаскелла

За прошедшее десятилетие он был спроектирован как гибкий - как логика проверки собственности - и мощный.

Система типов в Haskell разрабатывалась годами для поощрения относительно гибкой, выразительной дисциплины статической проверки, когда несколько групп исследователей определили методы системы типов, которые позволяют создавать новые мощные классы проверки во время компиляции. Скала относительно не развита в этой области.

Таким образом, Haskell/GHC предоставляет мощную логику, предназначенную для поощрения программирования на уровне типов. Нечто довольно уникальное в мире функционального программирования.

Некоторые статьи, которые дают представление о направлении, которое предприняли инженерные усилия в системе типов Хаскелла:

• Веселье с функциями типа
• Связанные типы с классом
• Веселье с функциональными зависимостями

Answer 2

Хиндли-Милнер - это не система типов, а алгоритм вывода типов. Раньше система типов Haskell могла быть полностью выведена с помощью HM, но этот корабль уже давно проплыл на современном Haskell с расширениями. (ML остается способным быть полностью выведенным).

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

Но это в основном не то, о чем я думаю, вопрос на самом деле.

Документы, на которые ссылаются, указывают на другой аспект - на то, что расширения системы типов Haskell делают ее полной по Тьюрингу (и что современные семейства типов делают этот полный по языку язык намного более похожим на программирование на уровне значений). Еще одна приятная статья на эту тему - " Faking It: моделирование зависимых типов" в Haskell.

В другой статье о Scala: "Классы типов как объекты и следствия" объясняется, почему вы можете сделать большую часть этого в Scala, хотя и с большей ясностью. Я склонен чувствовать, но это более интуитивное чувство, чем из реального опыта Scala, что его более специализированный и явный подход (то, что в C++ называется "номинальным") в конечном счете немного сложнее.

Answer 3

Давайте рассмотрим очень простой пример: Haskell's Maybe,

data Maybe a = Nothing | Just a

В C++:

template <T>
struct Maybe {
    bool isJust;
    T value;  // IMPORTANT: must ignore when !isJust
};

Давайте рассмотрим эти две сигнатуры функций в Haskell:

sumJusts :: Num a => [Maybe a] -> a

и C++:

template <T> T sumJusts(vector<maybe<T> >);

Отличия:

• В C++ есть больше возможных ошибок. Компилятор не проверяет правило использования Maybe,
• Тип C++ sumJusts не указывает, что требуется + и снимали с 0, Сообщения об ошибках, которые появляются, когда что-то не работает, являются загадочными и странными. В Haskell компилятор просто будет жаловаться, что тип не является экземпляром Num, очень просто..

Короче говоря, Haskell имеет:

• ADTS
• Type-классы
• Очень дружелюбный синтаксис и хорошая поддержка дженериков (которых в C++ люди стараются избегать из-за всей своей криптикиштишизмы)

Answer 4

Язык Haskell позволяет писать более безопасный код, не отказываясь от функциональности. Большинство языков в настоящее время обмениваются функциями безопасности: язык Haskell показывает, что возможно иметь и то, и другое.

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

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

Просто мои два цента.

Answer 5

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

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

fibs :: Num a => [a]
fibs@(_:xs) = 0:1:zipWith (+) fibs xs

Например:

map (`div` 2) fibs        -- integral context
(fibs !! 10) + 1.234      -- rational context
map (:+ 1.0) fibs         -- Complex  context

Вы можете даже определить свой собственный числовой тип для этого.

Answer 6

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

1. Чистота.
   Purity позволяет Haskell различать чистый код и код с возможностью ввода-вывода
2. Параметричность.
   Haskell обеспечивает параметричность параметрически полиморфных функций, поэтому они должны подчиняться некоторым законам. (Некоторые языки позволяют выражать полиморфные типы функций, но они не обеспечивают параметричность, например, Scala позволяет сопоставить шаблон для определенного типа, даже если аргумент полиморфен)
3. ADT
4. Расширения
   Система базовых типов Haskell - это более слабая версия λ2, которая сама по себе не особо впечатляет. Но с этими расширениями он становится действительно мощным (даже может выражать зависимые типы с помощью singleton):
   1. экзистенциальные типы
   2. типы ранга n (полное λ2)
   3. типовые семьи
   4. виды данных (позволяет "типизированное" программирование на уровне типов)
   5. GADT...