These are chat archives for groupoid/exe

8th
Aug 2016
Namdak Tonpa
@5HT
Aug 08 2016 05:40
Namdak Tonpa
@5HT
Aug 08 2016 06:54
пол эрланга надо переписать, чтобы вставить свой шелл :-)
думаю сделаю переключение между Erlang и EXE командами шелла
я не хочу делать как в хаскеле свой язык :t, :i и других шеллах
я хочу чтобы можно было в шелл направить обычную EXE программу и она выполнилась
т.е. чтобы шелл не было отличим от обычного потока файла
что скажите @nponeccop @proger ?
типа вводишь терм нажимаешь ввод и получаешь ераснутый терм и его тип
нажимаешь CTRL+G попадаешь в меню шелла
там клацаешь настройки, переключаешь вывод с OM на EXE и обратно допустим
возвращаешься и опять
вводишь терм нажимаешь ввод и получаешь терм и его тип
Namdak Tonpa
@5HT
Aug 08 2016 06:59
хочешь только типы видеть например, идешь в меню шелла, выключаешь вывод термов оставляешь вывод только типов
и т.д.
Zeit Raffer
@zraffer
Aug 08 2016 07:58
Иногда хочется ераснутый, но иногда - нормализация, а иногда только тип. Хм.
Namdak Tonpa
@5HT
Aug 08 2016 07:58
ну вот это все можно будет переключать в меню похожему на то которое ты счас видишь нажимая CTRL+G
так ок или ты хочешь как в GHCi перед термом ставить :t ?
Zeit Raffer
@zraffer
Aug 08 2016 07:59
А, меню. Надо попробовать.
Namdak Tonpa
@5HT
Aug 08 2016 08:00
1>
User switch command
 --> ?
  c [nn]            - connect to job
  i [nn]            - interrupt job
  k [nn]            - kill job
  j                 - list all jobs
  s [shell]         - start local shell
  r [node [shell]]  - start remote shell
  q                 - quit erlang
  ? | h             - this message
Zeit Raffer
@zraffer
Aug 08 2016 08:00
Надо в сам язык вставить type of. Так консистентнее.
Namdak Tonpa
@5HT
Aug 08 2016 08:00
я про это меню
Zeit Raffer
@zraffer
Aug 08 2016 08:01
Ага.
Namdak Tonpa
@5HT
Aug 08 2016 08:01
я счас пишу его реплейсмент для EXE
ну без type of все должно рабтать тоже
Zeit Raffer
@zraffer
Aug 08 2016 08:02
Требуется эксперт по юзабилити ) специализирующийся на командной строке.
Namdak Tonpa
@5HT
Aug 08 2016 08:02
просто вводишь терм и REPL должен гвоорить "ОК, схвал", или "ГОВНО, не тайпчекается"
ну я ж Процессора и Прогера пинганул
Zeit Raffer
@zraffer
Aug 08 2016 08:03
Ок
Они спят
Namdak Tonpa
@5HT
Aug 08 2016 10:24
на гитхабе ОМ лайкают из EPFL
Zeit Raffer
@zraffer
Aug 08 2016 10:24
уря!
nponeccop
@nponeccop
Aug 08 2016 14:51
Ну я проснулся, но не имею особого мнения по реплу. По мне так лучшим реплом будет интеграция с эдитором в части навигации по ошибкам, т.е. добавление номеров строк в вывод ошибок
Namdak Tonpa
@5HT
Aug 08 2016 14:52
Интеграция с эдитором — это сложнее чем репл написать.
nponeccop
@nponeccop
Aug 08 2016 14:54

да ну нах, я не говорю о полной интеграции. Просто выводишь строки в формате совместимом с GCC, и 99% едиторов это подхватывают.

@zraffer в чём пускает?

Zeit Raffer
@zraffer
Aug 08 2016 14:55
убунта, если речь про ОС
nponeccop
@nponeccop
Aug 08 2016 14:55
а едитор?
Zeit Raffer
@zraffer
Aug 08 2016 14:55
атом.ио
Namdak Tonpa
@5HT
Aug 08 2016 14:56
а ну это да, консольный вывод конечно должен быть в стиле mad хотябы или gcc
это с repl не связано, это просто вывод тайпчекера
nponeccop
@nponeccop
Aug 08 2016 15:01
Так я и не говорю что связано. Я говорю что удобства навигации по ошибкам перекроют удобства репла имхо и это надо прикручивать первее. Но пусть Павел решает что ему хочется первее. У нас он сейчас узкое место поэтому надо ему помогать.
Zeit Raffer
@zraffer
Aug 08 2016 15:02
страшный вопрос - кто пишет тайпчекер?
Namdak Tonpa
@5HT
Aug 08 2016 15:03
Андрей, ты пишешь тайпчекер ? :-)
Zeit Raffer
@zraffer
Aug 08 2016 15:03
подозреваю, что я
nponeccop
@nponeccop
Aug 08 2016 15:04
Я нет. Я по пиздежу специалист же
короче нужная командная строка встраивается тривиально
(как и в другие едиторы впрочем)
Namdak Tonpa
@5HT
Aug 08 2016 15:04
Пацаны, я смог бы написать тайпчекер? )
Zeit Raffer
@zraffer
Aug 08 2016 15:04
мы в тебя верим ))
ну смотрите, просто сейчас возможны два параллельных шага - писать трансляцию ЦиЦ/ЦоЦ и одновременно писать тайпчекер языка с рекордами
Namdak Tonpa
@5HT
Aug 08 2016 15:08
ну сначала тайпчекер думаю
скопировать просто ОМ код
добавить кляузу для record
я так это вижу
nponeccop
@nponeccop
Aug 08 2016 15:08
Ага
Namdak Tonpa
@5HT
Aug 08 2016 15:08
потом когда видно что чекается начинать экспанд
я хочу чтобы тайпчекер не отличался от ОМ-ного и было видно приемственность
пушо я ОМ-ный понимаю )
Zeit Raffer
@zraffer
Aug 08 2016 15:09
нужно описать структуру для хранения информации о рекорде, и посик в ней имен полей. это не сложно.
Namdak Tonpa
@5HT
Aug 08 2016 15:10
ну это ж вот эти арити
Zeit Raffer
@zraffer
Aug 08 2016 15:10
шоза арити
контексты
Namdak Tonpa
@5HT
Aug 08 2016 15:10
ну вот эти нули и единицы (тип и значения)
контексты да
Zeit Raffer
@zraffer
Aug 08 2016 15:10
ну и это
Namdak Tonpa
@5HT
Aug 08 2016 15:10
ну это тайпчекером будет заполнятся
Zeit Raffer
@zraffer
Aug 08 2016 15:10
ну вот
Namdak Tonpa
@5HT
Aug 08 2016 15:12
{record,Name,Base,Args,Type,{fields,[{field,Name,Pos,TypeTerm,FieldValue},{...},...]}
Zeit Raffer
@zraffer
Aug 08 2016 15:13
так ты хочешь писать? если нет, то я напишу, конечно. просто время...
nponeccop
@nponeccop
Aug 08 2016 15:14
Важно понимать, что нам тайпчекер интересен только своими сообщениями об ошибках. Никаких других функций он не выполняет. Т.е. если сообщения будут неотличимы от генерируемых омом после рассахаривания, цель не достигнута.
Zeit Raffer
@zraffer
Aug 08 2016 15:14
ага
хочется быть уверенным в том коде библиотек, который я пишу
ну и плюс, хочется непредикативности, а в АГде или Леан ее в полной мере нету
nponeccop
@nponeccop
Aug 08 2016 15:15
Ну это тебе обеспечит и чекер ома
Zeit Raffer
@zraffer
Aug 08 2016 15:15
а кто рассахарит?
nponeccop
@nponeccop
Aug 08 2016 15:15
компилятор
Namdak Tonpa
@5HT
Aug 08 2016 15:15
так речь же идет что экспандер без чекера EXE будет позволять течь абстракциям
nponeccop
@nponeccop
Aug 08 2016 15:16
просто потому что сообщения будут дебильными
не будет видно где ошибка
т.е. задача - улучшить сообщения.
Zeit Raffer
@zraffer
Aug 08 2016 15:16
ну когда он будет, то да. только тут надежность состоит в том, что мы можем сделать ЕХЕ предикативным (и скорее всего консистентным) при том что ОМ будет непредикативным (и скорее всего неконсистентным)
т.е. тайпчек уровня ЕХЕ дает больше, чем тайпчек уровня ОМ
Namdak Tonpa
@5HT
Aug 08 2016 15:17
он имеет ввиду что после рассахаривания теряется информация
nponeccop
@nponeccop
Aug 08 2016 15:17
ну это как бы задел на будущее, у нас сейчас нет предикативной кодировки
Namdak Tonpa
@5HT
Aug 08 2016 15:17
которую не восстановить в ОМ коде
и даже если ОМ прочекается, может быть неконсистентность
nponeccop
@nponeccop
Aug 08 2016 15:17
сейчас этой разницы нет
Zeit Raffer
@zraffer
Aug 08 2016 15:17
речь про существующую кодировку как раз. на будущее у нас могут быть оба языка предикативными. а сейчас придется выкручиваться.
nponeccop
@nponeccop
Aug 08 2016 15:18
Ага, т.е. в Exe предикативная система типов уже сейчас?
Zeit Raffer
@zraffer
Aug 08 2016 15:18
ага
nponeccop
@nponeccop
Aug 08 2016 15:18
Теперь понятно
Namdak Tonpa
@5HT
Aug 08 2016 15:19
в тех макросах что он рисует на коленке
Zeit Raffer
@zraffer
Aug 08 2016 15:19
подразумевается, что ЕХЕ предикативен, а макросы его транслируют в непредикативный код
effectfully
@effectfully
Aug 08 2016 15:19
собственно, оригинальная CoC импредикативна и [считается что] консистентна
Zeit Raffer
@zraffer
Aug 08 2016 15:19
доказано вроде, да
Namdak Tonpa
@5HT
Aug 08 2016 15:19
она консистента для огранниченого набора сортов
Zeit Raffer
@zraffer
Aug 08 2016 15:19
но там один универсум полноценный
Namdak Tonpa
@5HT
Aug 08 2016 15:19
а если у тебя инфинити, то любые функуторы существуют )
Zeit Raffer
@zraffer
Aug 08 2016 15:19
это уже обсуждали ))
Namdak Tonpa
@5HT
Aug 08 2016 15:20
обсуждали но @effectfully поздно пришел
Zeit Raffer
@zraffer
Aug 08 2016 15:20
да с ним же и обсуждали
effectfully
@effectfully
Aug 08 2016 15:20
а зачем их много?
Namdak Tonpa
@5HT
Aug 08 2016 15:20
начинается )
чтобы HoTT делать
Инфинити Групоиды
effectfully
@effectfully
Aug 08 2016 15:20
((A : Prop) -> A) ∈Prop
Zeit Raffer
@zraffer
Aug 08 2016 15:20
потом поробуем сделать ограниченный вариант. но там нужно изворачиваться ужом.
вот как мы начинаем вводить всякие непредикативные Пропы, как в АУТОМАТ
это пусть просто к многим универсумам
ладно я домой бегу. потом продолжим.
Namdak Tonpa
@5HT
Aug 08 2016 15:22
котаны я начал колекционировать факапы http://maxim.livejournal.com/482046.html
для презентации Групоид Инфинити инвесторам
кидайте если что-то такое найдете
не надо никаких ограниченых вариантов!
работаем в полном и открытом пространстве!
Zeit Raffer
@zraffer
Aug 08 2016 15:23
падающие спутники! марсоходы! зонды на сатурне!
Namdak Tonpa
@5HT
Aug 08 2016 15:23
да да да
Zeit Raffer
@zraffer
Aug 08 2016 15:23
люди, поджаренные рентгеновским аппаратом
effectfully
@effectfully
Aug 08 2016 15:24
аппаратом лучевой терапии
nponeccop
@nponeccop
Aug 08 2016 15:28
взломанные автопилоты, прыгающие с моста!
Namdak Tonpa
@5HT
Aug 08 2016 15:30
пилоты кстати часто совершают креши из-за того что их психолог плохо работал
не прочекал кванторами :-)
типа там в скалу самолет часто бывает
самоубийства
когда кокаин дорогой )