Слава
На японских двачах распространены картинки из ascii
Anonymous
Кстати, идея. Надо было из столь любимых хаскеллистами пейперов стикеров нарезать. Только пейперов самых придурошных, где автор пишет пейпер ради пейпера
Слава
Именно поэтому
Слава
Alexander
из столь любимых или из придурошных? contradiction
Anonymous
Я просто, эээ, замечаю, что у многих господ от слова "пейпер" происходит переход в предоргазмическое состояние вне зависимости от контента
Alexander
это ж у хаскель хейтеров?
Кабачок
Alexander
им слово пейпер скажешь и их в космосе ловить надо
Антон
Антон
𝙱𝚎𝚒𝚉𝚎𝚛𝚘
Можно, если множество термов каждого типа конечно. Но это непрактично
Смотря что понимать под тестами. В общем-то ничто особо не мешает(кроме конечного числа времени и здравого смысла) написать тест, который будет доказывать эквивалентность какого-то блока кода(хоть по инструкциям) уже каким-то доказанным/верифицированным вещам, а они в свою очередь могут работать и с какими-то бесконечными типами данных. Т.е. в общем-то самый отвратительный вариант это написать рядом такую же программу на языке с нормальной мощной системой типов, а тест будет доказывать их изоморфность как набора инструкций с точностью до каких-то не значительных деталей.
Слава
Есть подход из ada spark (а также dafny, ats, frama c и т.п.). Рядом с обычной императивной программой с байтогрызением записывается декларация того, что программа должна делать. В декларативной форме. А верификатор сверяет - соответствует ли декларируемое реальному.
Евгений
Alexander
да, мне понравилось, можно жуткую дискриминацию устраивать
Евгений
Я думаю сделать бота, который всем запрещает
Евгений
Заходишь в чат -- он тебя разувае
кана
так очень старая фича же
Alexander
я не видел
Alexander
тут выложили видосы с curry on
https://www.youtube.com/watch?v=t0mhvd3-60Y
Anonymous
А презентации тут постить можно?
Dmitry
Кстати, в чатике по Генту есть же простой бот: он предлагает входящему выбор из двух вариантов, надо выбрать один. Если за 5 сек не справился - в бан. Давайте такой тут поставим?
Dmitry
Dmitry
и что тут надо отвечать?
Dmitry
но вообще - да, надо бы
Dmitry
"Идём"
Dmitry
Ну, а ответы-то можно подобрать
Dmitry
"Го рулит", "Снойман бох"
Dmitry
Во, в чатике по Генту ещё и бот для ограничения по количеству символов предлагают
Dmitry
https://t.me/AutoBanSpamBotsBot
Dmitry
https://t.me/Cyberdyne_Systems_bot
Sr
Я бы с таким ботом не разобрался и попытался бы послать нахер эту железяку (хотя единственный кого послали бы был кожанный мешок)
Dmitry
Так ты уже всё равно в чате.
Dmitry
Всех перерегистрировать не будут
Алексей ayaye :)
Alexander
в каких алгоритмах есть большой бонус от unboxed sums? ну кроме того, что с векторами попроще теперь может быть?
Alexander
ну и то, что теперь руками и страданием можно делать алгоритмы без bottom, хотя практическое применение для этого под вопросом, поидее этим оптимизатор бы мог заняться
Dmitry
Ну что?
Dmitry
Добавляем ботов?
Dmitry
Админы, ау?
Dmitry
Или пусть китайцы хаскель осваивают?
Alexander
если кому не лень посмотрите список ников, и я автобан бота поставлю
Alexander
чтобы никого из своих не пришибло, а то я помню тут были с длинными никами
Nikita
Prelude> length "Зигохистоморфный препроморфизм"
30
Alexander
с другой стороны у меня не хватит прав выдать права боту
Alexander
нужно @weonn пинать
Nat
Крылатый
У Алекса Фейлза есть бот, который научился автоматом банить и подчищать таких китайцеботов.
Alexander
алгоритмы значения в которых гарантировано не являются bottom
A64m
анбоксед суммы это же просто средство вернуть более одного значения из функции на стеке, как и анбоксед туплы, только погибче. не знаю, для чего их еще можно использовать
A64m
сейчас их даже в массиве не сохранишь
Alexander
а почему?
Alexander
надо бы покопаться с ними
Alexander
и.е. если я понимаю правильно, то мы можем возвращать на стеке распакованный Either', но толку все равно будет не много и.к. поля будут забокшены, если они не распакованы и лениво матчиться?
A64m
ну просто нету примитивных массивов для элементов с таким представлением, но их нету почти ни для каких представлений, вообще говоря, даже для анлифтед только планируются
Alexander
и.е. у нас будет -1 indirection всего-лишь?
A64m
A64m
Alexander
а все полностью распаковать только backpack может
Alexander
а Array# не позволит хранить там сумму?
Alexander
хм.. а произведение хотя бы позволяет?
A64m
ну, бакпаком можно написать "полиморфный" код в котором представление возвращаемого может быть анбоксед суммой анбоксед типов
A64m
нет
Alexander
чтож за жизнь то
Alexander
а ещё они наверное не обновили проверку unsafeCoerce# для сумм распакованных
Alexander
сколько вещей на проверку
Dmitry
Китаец как бы намекает: "включайте ботов!"
Alexander
у меня нету прав дать права боту
Dmitry
А самый Главный может передать права кому-нибудь из активных юзеров? Вроде он чатиком не очень пользуется, как я понял.
Alexander
как бесят линзы когда я уже выучу как ими пользоваться
Alexander
вот есть foo :: Lens A (Maybe B) и bar :: Lens B (Maybe C)
Alexander
как сделать Getting A (Maybe C)
Leonid 🦇
_Just
Alexander
ну или Lens если сходу можно, мне именно получить
Alexander
foo . _Just . bar ?
Leonid 🦇
вроде да
Alexander
и запускать , через ^. ?
A64m
линзу-то никак
Alexander
ну мне getting надо
A64m
вообще, если в типе линзы Maybe есть - значит что-то идет не так