Transactional memory with data invariants.

Страница 7 AThrow, и Catch 1,2,3

Да, т.е. как я и сказал при throw лог хранится, эффекты нет. При catch если не было throw просто действие, если было то вызывается handler, если retry то retry всей транзакции (в этом отношении это не вложенные транзакции).

А пока не унывайте. Всего хорошего, здоровья!

Держитесь тут.

А вот люди говорят, State Transactional Memory можно ещё сделать??

Можно. Вопрос в том, будет ли такая реализация более выразительной, чем без монад: а) в Хаскеле, б) вообще, т.е. в языке где монады не нужны для оформления императивщины.

Но я не могу найти, чтобы там были safe points при вызове catchSTM. То есть, если мы прочитали или записали переменную внутри catchSTM, а потом внутри же него сделали throwSTM, то эти чтения и записи сохранят эффект в рамках текущей попытки завершить транзакцию. Разве нет?

Тем более, что в throwSTM может быть передана информация, добытая внутри catchSTM. Значит, safe points не может быть, я так полагаю. К тому же, как я прочитал, throwSTM может передать информацию во вне atomatically, если не будет перехвачено через catchSTM.

Я ж дал ссылку на операционную семантику. catchSTM action handler

При исключении в action все эффекты теряются, все логи сохраняются.

Про вне - правило ARET2. Если исключение не ловится catch то мы получаем IO исключение вне atomically.

Но если в handler передается информация из action, как те эффекты тогда могут потеряться?

В общем или под safe point ты понимаешь что-то не то, что я или я не знаю.

По мне safe-point - точка до которой можно откатиться, при это то, что было выполнено между точкой и местом где отказывались должно быть отменено.

Это реализуется через catchSTM где ловится Rollback (или специальное исключение) и throwSTM.

Я в этой записи не очень)

Ок, может я и не прав, дома проверю.

Может быть, говорим о разных вещах)

Но все же, если твой Rollback зависит от action внутри catchSTM, то как же тогда можно отменить то, что будет использоваться дальше в handler?

Ну, ладно. За статью спасибо!

{-# LANGUAGE ScopedTypeVariables #-}
import Control.Concurrent.STM
import Control.Exception

main = print =<< (atomically $ do
    x <- newTVar 10
    catchSTM (inner x) (\(e::SomeException) -> handle x))
  where
    handle x = fmap (+1) $ readTVar x
    inner x = do
      writeTVar x 15
      throwSTM (userError "Q")

qnikst@qwork ~ $ runhaskell 22.hs
11

похоже, я таки прав.

Да, скорее всего. STM и IO идут рядом. Очень часто из вычисления STM возвращается вычисление IO, которое затем применяется. В рамках транзакции мы не можем применить IO, но мы можем его вернуть и применить после транзакции (функция join).

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

мне казалось, что не вошло.

Про IO, если «нельзя, но очень хочется», то конечно можно:

qnikst@qwork ~ $ cat 23.hs
import Control.Concurrent.STM
import GHC.Conc
import Acme.Missiles

main = do
  atomically $
    unsafeIOToSTM launchMissiles

qnikst@qwork ~ $ runhaskell 23.hs
Nuclear launch detected.

мне казалось, что не вошло.

https://ghc.haskell.org/trac/ghc/ticket/11713

Действительно не вошло.

Про IO, если «нельзя, но очень хочется», то конечно можно:

И получить потенциально 100500 запусков, что не круто :)

это плохо, т.к. мне как жабаrодеру из этого всего только монады не понятны - и то потому что гдето это какято НЁХ, а гдето множество something и операция над ними обладающая something

а читать про них что-то кроме лора лень - т.к. в практических ЯП это не попадается

это плохо, т.к. мне как жабаrодеру из этого всего только монады не понятны - и то потому что гдето это какято НЁХ, а гдето множество something и операция над ними обладающая something

я не знаком с ООП и с многими вещами, которые знают разрабы, учившиеся в ВУЗ-ах на тех. специальностях. Да что там, даже плюсы не пытался осилить.

т.ч. не думаю что ЭТО настолько плохо... :)

вся эта херня (и ооп и функци-анальщина) нужна и для того чтобы применять ее кодя на баше или сях

исключение - когда ты ограничен ресурсами - микроконтроллеры и т.п. и у тебя не простота поддержки всех этой херни на первом месте а «как это впихнуть»

вся эта херня (и ооп и функци-анальщина) нужна и для того чтобы применять ее кодя на баше или сях

ух как завернул... даже не знаю что сказать.

исключение - когда ты ограничен ресурсами - микроконтроллеры и т.п. и у тебя не простота поддержки всех этой херни на первом месте а «как это впихнуть»

а также перформанс... да, знаком уже, благо, немало.

а также перформанс...

да, точно

ЯННП. Лор, это нормально?

нормально.

 Проходящие мимо и мы, идущие следом
  В полете лет глядящие в зеркала
  Мы хотели б жить долго, но я знаю
  Что скоро Ангел сна поднимет нас в небеса
  А нам нравится здесь и мы хотели бы
  Остаться здесь, но, увы нам уже пора
  Лететь

шманс-перфоманс

он самый

вот на удивление я не смог заставить launchMissiles в примере выше выстрелить 100500 раз, так и не понял в чем прикол :(. Я добавил readTVar, в другом треде этот TVar менял + добавил долгое вычисление, чтобы другой тред точно имел шанс поменять значение.

Похоже, что он тупо гонит. Выливает стеной всё, что родит (под)сознание.

call/cc мне нужен для того, чтобы реализовать в моей IDE инкрементную раскраску файла.

Любая монада выражается через cont-монаду, так что если есть call/cc - монады в принципе ни за чем не могут быть нужны. Даже с теоретико-формальной точки зрения, которую так любят хаскиводы.

по сути: монада это некоторая обобщённая, универсальная модель.

Проблема в том, что универсальная = бесполезная.

Ну например .? в цшарпе — по сути монада maybe.
Список, по которому можно замапить функцию — тоже монада.

Штука в том, что это конкретные монады, а не монады в общем. Ну это как если бы на вопрос «зачем нужны числа?» ты бы начал отвечать в стиле «ну вот у тебя яблоко, чтобы указать что оно у тебя, нужно число 1. А чтобы указать что их два - нужно число 2» вместо того, чтобы рассказать про возможность выполнения арифметических операций. Вот для монад арифметики нет, потому монады в общем, как концепция - не нужны. Нужны конкретные монады, но при этом совершенно незачем знать, что они являются монадами (это даже вредно, на практике).

Изоляция достигается за счет строгой системы типов языка Haskell.

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

Любая монада выражается через cont-монаду

Тот результат, который ты вспомнил, говорит про do-синтаксис монад. Более корректно сформулировать следующим образом: если есть do-синтаксис для cont-монады, то через него можно реализовать do-синтаксис для остальных монад. Не так пафосно звучит, правда?

> по сути: монада это некоторая обобщённая, универсальная модель.

Проблема в том, что универсальная = бесполезная.

Когда термин употребляется в контексте методологии естественных наук, тогда да. А когда контекст — это CS, тогда нет.

В качестве примера можешь вспомнить машину Тьюринга и лямбда-счисление. Обе абстракции — универсальные модели вычислений.

Довольно любопытный пример. Может быть, они так специально уменьшают размер журнала откатов? Тем не менее, полученный внутри inner временный результат может быть-таки передан в handle, что несколько запутывает дело.

Это в Haskell она так достигается за счет инкапсуляции?!

Да, при выбрасывания исключения можно прочитать неконсистентное значение, если честно, то я в этом больших проблем не вижу, на то они и исключения. Про мотивацию наверное в статье можно посмотреть.

Не так пафосно звучит, правда?

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

В качестве примера можешь вспомнить машину Тьюринга и лямбда-счисление. Обе абстракции — универсальные модели вычислений.

Какие же они универсальные? Они как раз концептуально весьма ограниченные и описывают очень узкий класс теорий. Потому и полезны. А вот «просто какая-то теория» (без ограничений) - штука бесполезная, как и «просто какая-то монада».

Это в Haskell она так достигается за счет инкапсуляции?!

Да. Опасные ф-и, применение которых может привести к факапу (вроде unsafePerformIO) засовываются внутрь, а в публичном интерфейсе остаются только безопасные ф-и (вроде bind), которые реализованы через безопасные, но заведомо корректным путем. Вот если бы хаскель мог гарантировать, что реализация бинда безопасна - тогда другой разговор, но мы просто в это верим. Точно так же можно сделать на какой-нибудь условной jave.

которые реализованы через безопасные

через опасные, селффикс

сажи негодному треду, потому что все объяснения в оп-посте неправильные и не отражают настоящих плюсов от фич

Это эквивалентыне утверждения

А, так ты просто тролль, так бы сразу и сказал.

Если ты можешь получить любую монаду из cont-монады внутри do, то ты можешь получить любую монаду враппингом бинда cont-монады в определенную функцию. Просто потому, что если рассахарить do-нотацию, то это будет _то же самое_. Странно, что кому-то это не очевидно.

Если посмотришь внимательно на код, который «реализует через cont любую монаду», то найдёшь в нём два места, в которые от этой любой монады средствами тайпклассов передаются уже реализованные bind и return. Соответственно возникает вопрос, что же именно реализует этот код тогда?

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

бинд любой другой монады выражался через композицию ее бинда с фиксированным естественным преобразованием

bind монады А выражается через bind монады А? Вау. Сформулируй утверждение поконкретнее.

этот тред прекрасен всем

Сформулируй утверждение поконкретнее.

Весь код в любом языке с call/cc является монадическим автоматом (в identity монаде). Без переписывания в do-нотацию, замены аппликаций на бинды и прочую чушь.

Именно по-этому получается в do-нотации записать любую другую монаду - do-нотация внутри cont является таким языком.

Точно так же, как ты в хаскеле превращаешь код внутри do в код любой монады - в языках с call/cc ты можешь делать _с произвольным_ кодом. В любом месте.

Весь код в любом языке с call/cc является монадическим автоматом (в identity монаде).

Точнее, он в cont-монаде, параметризованной биндом identity монады (как выше параметризуется биндом list-монады).

Весь код в любом языке с call/cc является монадическим автоматом (в identity монаде). Без переписывания в do-нотацию, замены аппликаций на бинды и прочую чушь.

Ты мог бы просто сказать «я этих ваших хаскелей не понимаю, схема всё равно круче». Но зачем-то выбрал путь длиннее.