Значения типа 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" }

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

поле parameters зависит от поля action

как это лучше через тип выразить?

через гадты и дата кайндс

"Поле A зависит от поля B" порождает два варианта: 1. симулировать зависимые типы через синглтоны (не советую, это хардкор) 2. сделать sum-тип и написать коммент про инвариант (классный и тупой Haskell98)

через гадты и дата кайндс

вот этот вариант нравится, сам о нем думал

ну сигнлтоны не факт что нужны

но если будешь далеко заходить, то до них дойдет

Твое предложение (gadt-ы и datakinds) равносильно синглтонами

но пока не понимаю как это стоит сделать