These are chat archives for groupoid/exe

16th
Apr 2016
Zeit Raffer
@zraffer
Apr 16 2016 06:00
пока я ковыряю предикативность и окончательного результата дать не могу, но мы можем обсудить такой реалистичный вариант стека: ЕХЕ использует предикативные универсумы, ОМ - непредикативные. консистентность всей системы обеспечивает тайпчекинг ЕХЕ, а непредикативность ОМ нужна для простоты кодировки.
nponeccop
@nponeccop
Apr 16 2016 06:05
мировое сообщество устроит и непредикативная кодировка
Zeit Raffer
@zraffer
Apr 16 2016 06:07
да здравствует мировое сообщество!
Namdak Tonpa
@5HT
Apr 16 2016 09:17
ну не забываем что морте либа не компилится предикативным чекером
webus
@webus
Apr 16 2016 10:11
привет всем. пока я совершенно ничего не понимаю что вы тут пишите. но читать интересно ) пока я понял что эти решения базируются на erlang/otp
Zeit Raffer
@zraffer
Apr 16 2016 11:01
@5HT морте-либа и не сможет компилиться! вот я сейчас внимательно смотрю, помогут ли нам 2-монады, чтобы плющить дважды пополненную категорию (в которой естественно строится объект натуральных чисел и прочие инициальные алгебры) в просто пополненную. нужно проверять, попадает ли конструкция в нужный универсум или, если нет, то работает ли универсальное свойство для того универсума, куда это объект попадает. там всё... довольно громоздко. результат нужен самый простой - работает ли рекурсор нашего объекта на самом этом объекте, чтобы в результате оказалось, что единственный его эндоморфизм - тождественный, отсюда можно будет вытащить индукцию аналогично непредикативному случаю. таков план. вобщем, тигр схвачен за хвост, и контекст в котором мы работаем идентифицирован - это слабо идемпотентные 2-монады. осталось пахать и рисовать стрелочки.
@webus Эрланг у нас основной бекэнд, правильно.
Namdak Tonpa
@5HT
Apr 16 2016 16:01
Конкатенативный APL-like язык со статической типизацией:
http://lambda-the-ultimate.org/node/5329
nponeccop
@nponeccop
Apr 16 2016 16:44
ага, я уже своему @inv2004 отправил ссылку, он хотел сделать подобие APL на Х-М, и я юзал его чекер пока имплементил кодогенерацию.
Он вроде как J в продакшене юзает