но я сразу разбаню

только по человеку, всему каналу как - не нашел

Пройдитесь по списку юзеров. Там полно спамеров

@jey_lee все ещё тут?

Все еще тут

Это проблема?

О, доброй ночи

нет, все хорошо

О, доброй ночи

❤️

а стикеры теперь не работают?

У меня еще не ночь же

не, тут только на 1 человека

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

я на первом сделавшем проверил

Гм, вот теперь не работают

Тьфу, ужас, скукота

спасибо за помощь в проведении эксперимента

На японских двачах распространены картинки из ascii

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

Именно поэтому

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

Не поймёт никто, и ты тоже. Картинка маленькая

из столь любимых или из придурошных? contradiction

Я просто, эээ, замечаю, что у многих господ от слова "пейпер" происходит переход в предоргазмическое состояние вне зависимости от контента

это ж у хаскель хейтеров?

Сосед-француз по имени Jérôme смотрит на такую политику в недоумении

Француз-я тоже

им слово пейпер скажешь и их в космосе ловить надо

Через неделю предлагаю пригласить гошника, ну или там растера.

Так тут уже есть растоманы

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

Можно, если множество термов каждого типа конечно. Но это непрактично

Можно, если множество термов каждого типа конечно. Но это непрактично

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

Есть подход из ada spark (а также dafny, ats, frama c и т.п.). Рядом с обычной императивной программой с байтогрызением записывается декларация того, что программа должна делать. В декларативной форме. А верификатор сверяет - соответствует ли декларируемое реальному.

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

Удобно, надо поэкспериментировать в блах

да, мне понравилось, можно жуткую дискриминацию устраивать

Я думаю сделать бота, который всем запрещает

Заходишь в чат -- он тебя разувае

так очень старая фича же

я не видел

тут выложили видосы с curry on https://www.youtube.com/watch?v=t0mhvd3-60Y

А презентации тут постить можно?

Кстати, в чатике по Генту есть же простой бот: он предлагает входящему выбор из двух вариантов, надо выбрать один. Если за 5 сек не справился - в бан. Давайте такой тут поставим?

и что тут надо отвечать?

но вообще - да, надо бы

"Идём"

Ну, а ответы-то можно подобрать

"Го рулит", "Снойман бох"

Во, в чатике по Генту ещё и бот для ограничения по количеству символов предлагают

https://t.me/AutoBanSpamBotsBot

https://t.me/Cyberdyne_Systems_bot

Я бы с таким ботом не разобрался и попытался бы послать нахер эту железяку (хотя единственный кого послали бы был кожанный мешок)

Так ты уже всё равно в чате.

Всех перерегистрировать не будут

Есть подход из ada spark (а также dafny, ats, frama c и т.п.). Рядом с обычной императивной программой с байтогрызением записывается декларация того, что программа должна делать. В декларативной форме. А верификатор сверяет - соответствует ли декларируемое реальному.

контрактное программирование - эйфель

в каких алгоритмах есть большой бонус от unboxed sums? ну кроме того, что с векторами попроще теперь может быть?

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

Ну что?

ERROR: S client not available

Добавляем ботов?

Админы, ау?

Или пусть китайцы хаскель осваивают?

если кому не лень посмотрите список ников, и я автобан бота поставлю

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

Prelude> length "Зигохистоморфный препроморфизм" 30

с другой стороны у меня не хватит прав выдать права боту

нужно @weonn пинать

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

а что такое "алгоритмы без bottom"?

У Алекса Фейлза есть бот, который научился автоматом банить и подчищать таких китайцеботов.

алгоритмы значения в которых гарантировано не являются bottom

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

сейчас их даже в массиве не сохранишь

а почему?

надо бы покопаться с ними

и.е. если я понимаю правильно, то мы можем возвращать на стеке распакованный Either', но толку все равно будет не много и.к. поля будут забокшены, если они не распакованы и лениво матчиться?

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

и.е. у нас будет -1 indirection всего-лишь?

и.е. если я понимаю правильно, то мы можем возвращать на стеке распакованный Either', но толку все равно будет не много и.к. поля будут забокшены, если они не распакованы и лениво матчиться?

да

и.е. у нас будет -1 indirection всего-лишь?

да

а все полностью распаковать только backpack может

а Array# не позволит хранить там сумму?

хм.. а произведение хотя бы позволяет?

ну, бакпаком можно написать "полиморфный" код в котором представление возвращаемого может быть анбоксед суммой анбоксед типов

нет

чтож за жизнь то