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

Ответ 1

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

Система типов выполняет две роли:

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

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

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

Ответ 2

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

Для Simon Marlow отличный ответ, я бы добавил, что система типов, особенно такая, которая включает в себя алгебраические типы данных, облегчает запись программ:

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

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

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

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

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

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

Ответ 3

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

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

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

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

Ответ 4

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

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