Функциональное программирование и системы типов

Question

Я уже некоторое время изучаю различные функциональные языки, включая Haskell, Scala и Clojure. У Haskell очень строгая и четко определенная система статических типов. Скала также имеет статическую типизацию. Clojure, с другой стороны, динамически набирается.

Так что мои вопросы

1. Какую роль играет система типов в функциональном языке?
2. Нужно ли для языка иметь систему типов, чтобы он был функциональным?
3. Как «функциональный» уровень языка связан с типом системы типов языка?

Answer 1

Язык не должен быть типизированным, чтобы быть функциональным - в основе функционального программирования лежит лямбда-исчисление , которое поставляется в нетипизированном и типизированном вариантах.

Система типов играет две роли:

• она обеспечивает гарантию во время компиляции, что класс ошибок не может возникнуть во время выполнения.Класс ошибок обычно включает в себя такие вещи, как попытка сложить две строки вместе или попытка применить целое число как функцию.
• имеет некоторые преимущества в плане эффективности, поскольку объекты во время выполнения не должны переносить свои типы вокругпотому что типы уже были установлены во время компиляции.Это известно как стирание типа .

В современных системах типов, таких как Haskell, система типов может предоставить больше преимуществ:

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

Answer 2

Какую роль играет система типов в функциональном языке?

К превосходному ответу Саймона Марлоу я бы добавил, что система типов, особенно та, которая включает алгебраические типы данных , упрощает написание программ:

• Проекты программного обеспечения, которые на объектно-ориентированных языках иногда выражаются с помощью диаграмм UML, очень четко выражаются с помощью типов. Эта ясность особенно проявляется, когда не только значения имеют типы, но и модули имеют типы, как в Objective Caml или Standard ML.

• Когда человек пишет код, пара простых эвристик позволяет очень и очень легко писать чистые функции на основе типов:

  • Значение типа функции всегда можно создать с помощью лямбды.
  • Значение типа функции всегда можно использовать, применяя его.
  • Значение алгебраического типа данных можно создать, применив любой из конструкторов типа.
  • Значение алгебраического типа данных можно получить, изучив его с помощью выражения case.

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

  forall a . (a -> Bool) -> [a] -> Bool
  

  Искусство использования типов для создания кода называется программированием на основе типов. Когда оно работает хорошо, вы слышите, как функциональные программисты говорят что-то вроде ", как только мы получили правильные типы, код практически написал сам. " Так как типы обычно намного меньше, чем код, это большая победа.

Answer 3

1. То же, что и на любом другом языке программирования: он помогает избежать / найти ошибки в вашем коде. В случае статической типизации хорошая система типов предотвращает компиляцию программ с определенными типами ошибок.
2. Нет. нетипизированное лямбда-исчисление - это то, что вы можете назвать прототипом функциональных языков программирования, и, как следует из названия, оно полностью нетипизировано.

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

   В чисто функциональном языке вам необходимо абстрагировать побочные эффекты, поэтому вы хотите, чтобы система типов как-то могла это поддерживать. Например, если вы хотите, чтобы тип мира был таким же, как в Clean, вы бы хотели, чтобы система типов поддерживала типы уникальности, чтобы обеспечить правильное использование.

   Если вы хотите иметь монаду ввода-вывода, как в haskell, вам понадобится тип ввода-вывода (хотя класс типов монад, как в haskell, не обязательно должен иметь монаду ввода-вывода, поэтому вам не нужна система типов, поддерживает это).

Answer 4

1: Как и любой другой, он останавливает вас от выполнения операций, которые либо плохо определены, либо чей результат будет «бессмысленным» для людей.Как и сложение с плавающей запятой для целых чисел.
2: Нет, самый старый язык программирования в мире, (нетипизированное) лямбда-исчисление, является функциональным и нетипизированным.
3: Вряд ли, функциональный просто означает отсутствие побочных эффектов, никаких мутаций, ссылочная прозрачность и так далее.

Просто помните, что самый старый функциональный язык, нетипизированное лямбда-исчисление, не имеет системы типов.