Является ли `pure x :: IO a` чистым значением или побочным эффектом?

Question

С учетом

pure id <*> v = v

верно, может pure сделать что-нибудь заметное и не нарушить закон?

Если я определю тип, который инкапсулирует IO, и скажу, породить новый поток, свободен ли GHC для его оптимизации?

РЕДАКТИРОВАТЬ: я наконец понял, что вопрос на самом деле о последствиях незаконного экземпляра IO ...

Answer 1

Я должен разделить ваш вопрос на два вопроса:

Является ли pure x :: IO a чистым значением или побочным эффектом?

Практически чистая стоимость. В этом коде тип x равен a, что является чистым значением.
И тип pure равен a -> IO a, который заключает аргумент в IO, но фактически без каких-либо побочных эффектов.
Так что pure x :: IO a, кажется, имеет побочный эффект в своем типе, но на самом деле не имеет.

... может ли чистый сделать что-нибудь заметное и не нарушить закон?

Нет. pure только применяет id к результату побочного эффекта, вызванного v.
Пока дело соответствует Применимому закону, побочный эффект вызывает не pure, а v.

Я полагаю, вы берете x в pure x для v :: IO a в pure id <*> v.
Первое является полностью чистым значением, тип которого a, а второе не является чистым значением: действие, которое может вызвать побочный эффект, возвращая значение, тип которого a.

И последний вопрос:

Если я определю тип, который инкапсулирует IO, и скажу, породить новый поток, свободен ли GHC для его оптимизации?

Извините, я не уверен в оптимизации.

Answer 2

GHC ничего не знает о законах классов типов (в отличие, например, от Idris или Coq), они существуют только как документация и соглашение о программировании. Следовательно, экземпляр может быть законным или незаконным, и в любом случае оптимизация GHC не изменит поведения программы.

Если вы напишите конкретный законный экземпляр, то, возможно, вы можете добавить правило REWRITE, чтобы заставить GHC удалить pure id, и GHC также может в конечном итоге оптимизировать pure id в определенных Applicative функторах, где безопасность этой оптимизации очевидна.