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

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

36 голосов
/ 24 сентября 2010

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

Ответы [ 5 ]

22 голосов
/ 24 сентября 2010

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

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

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

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

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

13 голосов
/ 24 сентября 2010

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

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

Но, по-моему, вопрос не в этом.

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

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

10 голосов
/ 27 сентября 2010

Давайте рассмотрим очень простой пример: Haskell 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
  • Тип-классы
  • Очень дружелюбный синтаксис и хорошая поддержка дженериков (которых в C ++ люди стараются избегать из-за всей своей криптичности)
7 голосов
/ 24 сентября 2010

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

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

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

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

5 голосов
/ 24 сентября 2010

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

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

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

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

...