считается ли возвращение _|_ сайд эффектом?

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

Кстати, а что за кайнд (* -> *) -> * ?

Можно пример такого типа?

не совсем то

data Free f a = Pure a | Free (f (Free f a))

(ну просто оно запомнилось применением своего аргумента, наверное есть и проще примеры)

Fix f = f (Fix f)

видимо то что нужно

Fix f = f (Fix f)

а где тут конструктор типа?

newtype Fix f = Fix { unFix :: f (Fix f) } deriving (Generic, Typeable)

хм, интересно:)

про функцию fix я читал, а вот про тип нет

data Q f = forall a. Q (f a)

data Q f = forall a. Q (f a)

откуда это?

сам написал, меня попросили я написал

аа

после знака равно может быть что угодно главное что f кайнда *->*, т.е. принимает тип и возвращает тип, который может быть значением

именно этот вариант не очень осмысленный, но можно придумать и осмысленный

у фикс как написано выше будет (*->*)->*->*

просто применение таких штук сложновато представить

и.е. это не то

здесь forall это экзистенциальный тип?

вполне можно представить себе применение

ну да можно убрать и написать Q (f Int)

= Q (f Int)

ну если его до ко-йонеды довести но будут

data User f = User { userName :: f String }

у фикс как написано выше будет (*->*)->*->*

а откуда там второй аргумент?

или классов типов добавить

вот да про юзера лучше

User Identity - валидный, User (Either Err) - результат валидации

data Fix f a

не?

а блин туплю

норм

там Free f a а Fix от ненр

Вроде как тут говорили, что да, является Ну и действия от него вполне тянут на сайд-эффект - терминация программы

не все согласны 🤔

да определенно тут периодически всплывает что бесконечная рекурсия и андефайнед - сай эффекты

User Identity - валидный, User (Either Err) - результат валидации

норм

ну _|_ ломает referential transparency если я правильно понимаю

пример

(не ломает)

Кстати, как формализовать понятие "сайд-эффекта"? Как я не бьюсь, у меня получается, что сайд-эффектов нет, есть неправильная типизация

Кстати, как формализовать понятие "сайд-эффекта"? Как я не бьюсь, у меня получается, что сайд-эффектов нет, есть неправильная типизация

любое наблюдаемое изменение в мире, не отражённое в возвращаемом значении

E x. f x ≠ f x ?

любое наблюдаемое изменение в мире, не отражённое в возвращаемом значении

Это не формализация, во-первых, во-вторых такого просто не бывает, если мы мыслим через формализацию вычислений посредством lambda calculus

E x. f x ≠ f x ?

это недетерминированность, она перпендикулярна побочным эффектам

любое наблюдаемое изменение в мире, не отражённое в возвращаемом значении

Ты хотел сказать, что тип возвращаемого значения скрывает часть информации о нём :)

Т.е. это неправильная типизация

Если функция возвращает разные значения, значит она зависит от чего-то, что изменяется, значит есть сайдэффект

Что значит "вохвращаемые значения"? Процедурная чушь какая-то. Нет возвоащаемых значений, есть редукция терма (f x)

Только в строгих стратегиях редукции (f x) в не зависимости от контекста редуцируется одинаково

Это не формализация, во-первых, во-вторых такого просто не бывает, если мы мыслим через формализацию вычислений посредством lambda calculus

да, в лямбдах не бывает, и в этом суть лямбд

мне кажется, что можно формализовать для какой-нибудь «процедурной машины Тьюринга»

например, как любое изменение в ленте за пределами ячеек, предназначенных для возврата результата

да, в лямбдах не бывает, и в этом суть лямбд

Ну при этом сайд-эффект это понятие ФП

Так что формализация через тьюринг-машины это убегание от ответа

Ты хотел сказать, что тип возвращаемого значения скрывает часть информации о нём :)

нет

я хотел сказать, что побочных эффектов нет в типах

в типах может быть только "кодировка побочных эффектов", как в Хаскелле и других чистых языках

Что значит "нет в типах"?

в типах может быть только "кодировка побочных эффектов", как в Хаскелле и других чистых языках

В хаскеле нет никакой "кодировки побочных эффектов"

Что значит "вохвращаемые значения"? Процедурная чушь какая-то. Нет возвоащаемых значений, есть редукция терма (f x)

именно так. побочные эффекты существуют только в рамках процедурной модели

В хаскеле и клине есть кодировка строгих вычислений (в виде монад или линейных типов), а не побочных эффектов

Монады - ленивые :)

Монады - ленивые :)

А корутины -- энергичные :) Но тем не менее это способ эмуляции другой стратегии редукции

Ну при этом сайд-эффект это понятие ФП

нет, это понятие не внутри ФП, а для отличия ФП от ИП

Так что формализация через тьюринг-машины это убегание от ответа

ограничивать себя лямбдами — это убегание от ответа

Это не формализация, во-первых, во-вторых такого просто не бывает, если мы мыслим через формализацию вычислений посредством lambda calculus

ну так сайд-эффекты это же внешнее понятие к lambda calculus

там просто IO Int и всё, разве нет?

В хаскеле нет никакой "кодировки побочных эффектов"

есть, State

всегда "одинаковое"

а уж как это IO Int выведется на какой-то "экран" или запишется в какой-то "файл", это не имеет отношения к самому исчислению

Я не понимаю претензию к терминологии. Нормальная концепция возвращаемого значения, вполне применима, если рассматривать редукцию тёрмов.

я так представляю в общем

"Передать аргумент" — сделать function application, потом выполняем редукцию, оставшийся тёрм — "возвращаемое значение".

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

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

там просто IO Int и всё, разве нет?

Значения типа IO Int это не 10, 15, 1768, а функции f, g, h, где f, g, h имеют тип (Realworld -> Realworld, Int)

есть, State

См выше