Это не формализация, во-первых, во-вторых такого просто не бывает, если мы мыслим через формализацию вычислений посредством 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

См выше

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

да. и в рамках этой модели эта функция одна и та же

> (Realworld -> Realworld, Int) Какой-то неправильный тип

она не зависит от каких-то состояний

unsafePerformIO

?

unsafePerformIO

ну так нечестно

И вообще модель IO a как функции RealWorld -> (a, RealWorld) я никогда не понимал, ведь мне в такой модели ничто не помешает к одному RealWorld применить разные функции, что нонсенс.

Нормально это моделируется только с линейными типами, в Merucry красиво сделали

См выше

не понял, уточни направление, пожалуйста

Я как-то задавал вопрос про РилВорлд, мне никто не ответил про него ничего. Я так понимаю, это какой-то кусок памяти, изменение которого сразу отражается на реальном мире (файловая система например). То есть именно РилВорлд является хаком, а не IO

начнём с того, что ST является хаком?

RealWorld не память, это вообще ничего. все действия с ним сводятся к вызову процедур, определённых вне Хаскелла

RealWorld это фантомный тег для создания data dependency

А на самом деле при редукции термов в Haskell могут быть сайд-эффекты, выполняемые RTS

И этот RealWorld позволяет порядок там навести небольшой

unsafePerformIO просто забивает на RealWorld

Я к тому, что можно ли делать сайд-эффекты без IO? То есть можно ли на хаскеле написать свою систему для сайд-эффектов без IO-монады

Можно

Есть набор примитивов, у которых во внутренностях GHC проставлено, что они могут вызывать прерывания процессора и делать сайд-эффекты. Их перечень захардкожен. Оптимизатор аккуратно не перемещает их никуда (там два принципа перемещения, float in и float out), чтобы гарантировать, что ничто два раза не вызывается. RealWorld применяется, чтобы в правильном порядке вызывались (создавая искуственно data dependency).

Можно взять эти примитивы и свою систему эффектов сделать.

Все-таки IO это библиотечный тип, а не примитив

А ST примитив?

Нет

ST это тот же тип, что IO, только вместо RealWorld там forall s. s, и имеем от этого runST

понять бы ещё, как эта runST работает

Никак, это no-op чтобы гарантировать, что ты не пытаешься ST-переменные за пределами ST использовать

ST гарантирует referential transparency за счет того, что переменные локальны

но всё-таки интересно, откуда она это начальное состояние берёт

или на самом деле она ничего не берёт

и это большой обман

Он его не берет, переменная s никогда не инстанцируется

когда я писал «примитив», имел в виду процедуры readIORef и writeSTRef, а не типы ST или IO

s не обман, она честно не используется

то есть её значение

У нее нет значения

интересно. то есть получается, что не все допустимые функции могут быть написаны на haskell, однако это не мешает нам их использовать, потому что из самой сигнатуры (forall s. ST s a) -> a следует, что такая функция единственна, а значит и "знать" нам её не обязательно

а ещё такие функции есть?

тело которых нельзя записать на языке редукции выражений

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

вечером статью с определением найду

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

тело которых нельзя записать на языке редукции выражений

Я не понимаю, runST редуцируется как положено

ну как бы выглядео тело такой функции?

Возьми и посмотри исходник

ок

начнём с того, что ST является хаком?

почему?

почему?

наверное я не прав. просто так читал в какой-то книжке, типа нач. значение берётся из ниоткуда

Я к тому, что можно ли делать сайд-эффекты без IO? То есть можно ли на хаскеле написать свою систему для сайд-эффектов без IO-монады

эм?

Кстати, надо бы и мне смотреть повнимательнее. Судя по runRW#, все-таки s инстанцируется внутри, как RealWorld.

оно размера 0

Так что ST еще больше похож на IO, чем я думал.

дальше оптимизации

В смысле что похож на ио, если ио это и есть ст

Я думал что IO это ST, где s принимается за RealWorld

а оказывается и в самом ST тоже RealWorld

Соответственно разница еще меньше

как это в ст Real world?

Ну вон там runRW# в определении runST

так, теперь надо в GHC.Magic лезть

# это просто название идентифаера?

Да

действительно

@anarchostatist обычно добавляют к функциям работающим с данными кайнда #

unboxed

Этого кайнда больше нет, но традиция осталась

лол ?

у меня практический вопрос, пишу обвязку вокруг api.ai

{ "id": "702fcc70-aa52-4ea0-8e78-3d040e56d221", "timestamp": "2017-09-16T12:38:33.477Z", "lang": "ru", "result": { "source": "agent", "resolvedQuery": "давай завтра", "action": "create_task", "actionIncomplete": false, "parameters": { "date": "2017-09-17", "time": "" }, "contexts": [], "metadata": { "intentId": "3dc678bb-900f-4323-9eb0-5e8342207647", "webhookUsed": "false", "webhookForSlotFillingUsed": "false", "intentName": "create_task" }, "fulfillment": { "speech": "Сделал задачу", "messages": [ { "type": 0, "speech": "Сделал задачу" } ] }, "score": 1 }, "status": { "code": 200, "errorType": "success" }, "sessionId": "fe8a36c0-6780-435a-84bd-59d9a052e3cd" }

заранее я не знаю какой мне ответ придет, потому что он зависит от запроса