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

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

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

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

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

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

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

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

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

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

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

   для всех. (a -> Bool) -> [a] -> Bool
  

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

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

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