особенно учитывая что Reader это тупо ->, а параметры в функции это вроде не плохо

Почему StateT а не ReaderT?

Потому что obscuring the intent is not the correct way.

Мутабельная ссылка на мутабельный референс, что может пойти не так?

Ну, может между запусками нужно хранить. Это же микросервисы, некогда не знаешь в какой момент кубернетесы всякие решат его убить и запустить на другой ноде

N мутабельных ссылок на разные подкомпоненты стейта, ты имел ввиду?

StateT (IORef [IORef a]) :)

Вариант.

Даже веселее, это закончится тем, что ты будешь делать встроенную СУБД своими руками, с индексами и журналами Вместо того, чтобы прикрутить редис

но ведь даже своя криво написанная СУБД лучше чем реддис?

Чем редиска плоха?

тем что для встраиваемой есть средства и лучше, так же как внешней и распределенной тоже

Для начала нужно понять, узкое ли это будет место

Может и sqlite хватить много для чего

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

ну sqlite вообще классика и прекрасно

для простых кейсов во всяком случае

sqlite это 100%'ные локи

Он хорош только если на одну запись приходится > 500 чтений

для начала нужно понять, что в итоге хочется, чтобы выбирать из правильного класса решений хотя бы

а то может начальное утверждение что быть стейтлес плохо - неверно

а мы тут базу ищем

https://gist.github.com/CMCDragonkai/b203769c588caddf8cb051529339635c

даешь все кванторы в хаскелл)

pi добавили бы

А экзистенциальная и так энкодится

А экзистенциальная и так энкодится

как?

exists x. t = forall r. (forall x. t -> r) -> r

форол на фороле

Обычный continuation passing

Обычный continuation passing

Cont?

Вместо 'a' всегда можно написать '(a -> r) -> r'

Это определение Cont

Если быть параметричным по 'r', то будет изоморфно

И forall второго ранга превращается в exists

а в чем тогда профит от pi?

Синглтоны можно будет выкинуть.

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

https://github.com/ghc-proposals/ghc-proposals/pull/52

А если все на свете промотиться будет, то pi через Sing выражается

инетерсно в идрис есть pi?

есть конечно

Конечно, там только он и есть

в этом же и поинт идриса, что он там изначально по построению есть

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

Не связано

pi as Π?

Да

вообще связано, бреди писал что при тотальности мол неважно ленивый язык или строгий :)

но основная причина мол проще за ресурсами следить

Так не важно, поэтому не связано

Эм? А как может быть "ленивый" тотальный язык?

Агда напр.

Ленивость это нормальная стратегия для вычисления тотальных функций

Надо только гарантировать отсутствие боттомов статически

Так для тотального подмножества лямбды стратегия одна, нет?

Она скорее не важна и повлияет только на асимптотику, а не на результат.

Множество стратегий появляется, если есть терм, у которого нету нормальной формы

А так их конечно много

Она скорее не важна и повлияет только на асимптотику, а не на результат.

Чо-т я не подумал об этом, да

Ну и всякую корекурсию проще всего реализовать как ленивость

Я, кстати, до сих пор не понимаю как коиндукция тотальность гарантирует. Как нормальная форма для коиндукции выглядит?

Ну и всякую корекурсию проще всего реализовать как ленивость

ну как бы да) интересно как сделать корекурсии в энергичном языке

Я, кстати, до сих пор не понимаю как коиндукция тотальность гарантирует. Как нормальная форма для коиндукции выглядит?

простейший пример - стримы?

Я, кстати, до сих пор не понимаю как коиндукция тотальность гарантирует. Как нормальная форма для коиндукции выглядит?

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

Я как-то так и думал, но ты заговорил о коиндукции в контексте тотальности...

интересно если хистоморфизм позволяет обращаться по истории на любой шаг, то выходит Cofree хранит всю историю вычислений свертки?

Я как-то так и думал, но ты заговорил о коиндукции в контексте тотальности...

Это считается тотальным

Ну такое, обычно под тотальным понимают имеющее нормальную форму

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

кто-то понял досконально рекурсивные схемы?)

я смотрю вам ваш ник покоя не дает :)

xgrommx слегка упоролся рекурсивными схемами :)

Кметт понял

Кметт понял, что есть ещё пара слоёв понимания

Для них тоже будут(есть?) пакеты

xgrommx слегка упоролся рекурсивными схемами :)

ну вот почему так)) тема классная а норм доков или туториалов нет)

так внеси вклад, начни писать :)

как же это нет

http://blog.sumtypeofway.com/ http://duplode.github.io/posts/whats-in-a-fold.html https://monad.cat/posts/2016-05-10-barbed-wire.html

кстати да, есть же колючая проволока! А ещё конверты и бананы с линзами :)