Обеспечивается ли чистота в Haskell системой типов или реализацией IO?

Всегда говорят, что система типов Haskell предотвращает загрязнение чистого кода нечистым кодом, так как вы всегда должны указывать IO в подписи типа. Однако является ли это следствием самой системы типов, или это действительно так? IO(..) не экспортируется?

По сути, разве это не правда, что, если бы конструктор типов был доступен, что-то подобное могло бы быть сделано?

ioToPure :: IO a -> a
ioToPure (IO ioValue) = ioValue
Источник

2 ответа

Решение

Да, это в некотором смысле правда.

Система типов сама по себе ничего не знает о IO и не нужно. Это разные языковые возможности, которые скрывают реальное представление действия ввода-вывода от пользователей, поэтому невозможно "просто запустить" действие ввода-вывода.

Таким образом, правда в том, что безопасность ввода-вывода в Haskell и сопоставимых языках - это объединенный результат нескольких языковых функций и свойств, наиболее заметно:

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

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

Источник

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

Однако без ограничений по типу все, что связано с IO, было бы опасно. Так что мы бы полностью запретили IO. Не очень полезно.

Вместо этого с помощью системы типов мы можем экспортировать некоторые "опасные" IO-действия, зная, что они могут быть выполнены только в "контролируемых" местах, которые должны нести IO тег в их типе. Делать их больше не опасно.

Таким образом, чистота происходит от комбинации статических гарантий и тщательного экспорта.

Источник
Другие вопросы по тегам