MP
хотя нет кстати, видел такое в api какой-то библиотеки для LMDB
Size: a a a
2020 November 19
MP
там довольно изящно было сделано, только транзакция может утечь
YR
это что за сигнатура -
withSocketsDo :: () => IO a -> IO a ?V0
возможно этот кейс можно решить просто в компайлтайме темплейт-хаскелем, ну вдруг
нет, разумеется если бы все можно было заинлайнить и зашить, то вопросов нет. тут я подвожу к более общему вопросу - IO и чистоты.
в этом сеттинге очевидно есть write в какой-то сокет по сети, однако с точки зрения всей системы мы знаем что функция детерминированная, не меняет глобального состояния, для одних аргументов вернет одно и то же - можно же назвать чистой? с оговоркой на хардварь и условие "ненаход ipfs файла = ошибка хардвари = можно падать в корку"
короче говоря, получается что система типов замкнута в рамках одной ноды и нет способа объяснить что архитектурно это чисто.
тем более, что если 1990 почти все программы были десктопными/локальными, сейчас все наоборот и для серверов и для (тонких, зачастую вебовских) клиентов
короче, почему есть только одно IO-с-т.з.-локалхоста, когда я точно знаю что в проде все связано по сети, оно везде есть, мне интересно IO-с-т.з.-системы, т.е. либо запись-изменение-ее-состояния, либо поход во внешние апи.
еще короче, запись в сокет семантически означает _разное_, но тип для этого один 😕
в этом сеттинге очевидно есть write в какой-то сокет по сети, однако с точки зрения всей системы мы знаем что функция детерминированная, не меняет глобального состояния, для одних аргументов вернет одно и то же - можно же назвать чистой? с оговоркой на хардварь и условие "ненаход ipfs файла = ошибка хардвари = можно падать в корку"
короче говоря, получается что система типов замкнута в рамках одной ноды и нет способа объяснить что архитектурно это чисто.
тем более, что если 1990 почти все программы были десктопными/локальными, сейчас все наоборот и для серверов и для (тонких, зачастую вебовских) клиентов
короче, почему есть только одно IO-с-т.з.-локалхоста, когда я точно знаю что в проде все связано по сети, оно везде есть, мне интересно IO-с-т.з.-системы, т.е. либо запись-изменение-ее-состояния, либо поход во внешние апи.
еще короче, запись в сокет семантически означает _разное_, но тип для этого один 😕
AV
Есть ли способ избавиться от IO в сигнатуре, если мы read-only из чего-то ipfs-подобного?
Я понимаю, что сеть ненадежна, но нельзя ли в случаях ошибки хардвари просто упасть, или erlang-style тут не в почете?
Короче, хочется воспринимать ф-ю с таким чтением как чистую, обращающуюся к константе в типа-ооооочень-медленной-памяти?
Я понимаю, что сеть ненадежна, но нельзя ли в случаях ошибки хардвари просто упасть, или erlang-style тут не в почете?
Короче, хочется воспринимать ф-ю с таким чтением как чистую, обращающуюся к константе в типа-ооооочень-медленной-памяти?
{-# NOINLINE #-} + unsafePerformIO
AV
Yuki Rito
это что за сигнатура -
withSocketsDo :: () => IO a -> IO a ?Древний костыль для винды но забудь
AV
А вообще сигнатура - это сделать что-то с IO действием
AV
Например что-то перед действием как в withSocketsDo или обернуть в bracket или после
AV
нет, разумеется если бы все можно было заинлайнить и зашить, то вопросов нет. тут я подвожу к более общему вопросу - IO и чистоты.
в этом сеттинге очевидно есть write в какой-то сокет по сети, однако с точки зрения всей системы мы знаем что функция детерминированная, не меняет глобального состояния, для одних аргументов вернет одно и то же - можно же назвать чистой? с оговоркой на хардварь и условие "ненаход ipfs файла = ошибка хардвари = можно падать в корку"
короче говоря, получается что система типов замкнута в рамках одной ноды и нет способа объяснить что архитектурно это чисто.
тем более, что если 1990 почти все программы были десктопными/локальными, сейчас все наоборот и для серверов и для (тонких, зачастую вебовских) клиентов
короче, почему есть только одно IO-с-т.з.-локалхоста, когда я точно знаю что в проде все связано по сети, оно везде есть, мне интересно IO-с-т.з.-системы, т.е. либо запись-изменение-ее-состояния, либо поход во внешние апи.
еще короче, запись в сокет семантически означает _разное_, но тип для этого один 😕
в этом сеттинге очевидно есть write в какой-то сокет по сети, однако с точки зрения всей системы мы знаем что функция детерминированная, не меняет глобального состояния, для одних аргументов вернет одно и то же - можно же назвать чистой? с оговоркой на хардварь и условие "ненаход ipfs файла = ошибка хардвари = можно падать в корку"
короче говоря, получается что система типов замкнута в рамках одной ноды и нет способа объяснить что архитектурно это чисто.
тем более, что если 1990 почти все программы были десктопными/локальными, сейчас все наоборот и для серверов и для (тонких, зачастую вебовских) клиентов
короче, почему есть только одно IO-с-т.з.-локалхоста, когда я точно знаю что в проде все связано по сети, оно везде есть, мне интересно IO-с-т.з.-системы, т.е. либо запись-изменение-ее-состояния, либо поход во внешние апи.
еще короче, запись в сокет семантически означает _разное_, но тип для этого один 😕
IO это какой-то любой эффект, в этом случае операции как с точки зрения локалхоста, так и сети вообще не отличаются по свойствам
AV
Всё может быть недеретимнировано по результату и по занимаемому времени
V0
Всё может быть недеретимнировано по результату и по занимаемому времени
А я правильно помню, что если в языке нет тотальности (типа dhall) то локальная чистая fn не имеет других гарантий относительно времени выполнения, и получается разницы с надежной, но очень медленной сетью нет, так?
V0
В общем, если оставить в сторону абстрактные темы, то могу переформулировать так - есть ли языки/экосистемы/whatever которые имея несколько частей задеплоеными на разные ноды, связанные по сети - могли бы мне гарантировать, что условный HTTP GET ничего никуда не пишет (чистый в системном смысле)?
YR
Древний костыль для винды но забудь
аа, вроде можно опустить пишут.... ОК
AV
А я правильно помню, что если в языке нет тотальности (типа dhall) то локальная чистая fn не имеет других гарантий относительно времени выполнения, и получается разницы с надежной, но очень медленной сетью нет, так?
если в языке есть тотальность, то в нём тоже нет никаких гарантий относительно времени выполнения, кроме того, что оно не бесконечное
AV
Гарантии о времени выполнения могут быть только если язык поддерживает систему доказательств и нам выражено доказательство про время выполнения. В человеческих системах так не делает никто, кажется
AV
Возможно во всяких инженерных такое и есть, но там свои правила языки и утилиты, я но я тут не специалист. Ещё есть в академических
AV
А про сеть вообще мало разумного доказать можно будет, разве, что если время выполнения больше X то код выйдет с такой-то ошибкой)
А
Гарантии о времени выполнения могут быть только если язык поддерживает систему доказательств и нам выражено доказательство про время выполнения. В человеческих системах так не делает никто, кажется
для встроенного софта это важно, за этим следят и, вроде бы, кое-где строго доказывают