These are chat archives for groupoid/exe

29th
Jul 2016
Zeit Raffer
@zraffer
Jul 29 2016 08:43
с грамматикой нужно решить: либо мы преобразуем ее в вид, подходящий для имеющегося LALR(1) парсера, либо ищем другой парсер.
тайпчекер можно писать параллельно, если мы считаем АСТ фиксированным
и еще вопрос по грядущему митапу. мы его отложили до выполнения неких задач, чтобы было что показать. можем мы сейчас четко конкретизировать эти задачи, по минимуму, чтобы на них сейчас сосредоточиться, как на приоритетных?
Namdak Tonpa
@5HT
Jul 29 2016 13:11
а с чего ты взял что твою грамматику нельзя в LALR(1) записать?
митап можно уже проводить — индукция же есть
слайды надо рисовать
Zeit Raffer
@zraffer
Jul 29 2016 13:11
я читал, что любую грамматику можно туда запихать, но секрет древних мастеров ныне утерян ))
Namdak Tonpa
@5HT
Jul 29 2016 13:12
и какой ты предлагаешь взамен LALR(1) чтобы немастера могли выразить грамматику? :-)
(просто интересно)
Zeit Raffer
@zraffer
Jul 29 2016 13:13
ну вот люди пользуются наполовину вручную парсер-комбинаторами
я не знаю, есть ли что-то такое под эрланг
Namdak Tonpa
@5HT
Jul 29 2016 13:13
ну как я в ОМ
после чего мы все вроде договрились что ручные парсеры больше не пишем )
этот чат почитают и скажут что к группоид инфинити не смогли левую грамматику записать )
задача для 3-го курса
есть кто читает этот чат и хочет переписать грамматику? :-)
Zeit Raffer
@zraffer
Jul 29 2016 13:15
ок. а кто у нас больший спец по грамматикам? я давно не преобразовывал в ЛАЛР(1), хотя могу, конечно, попытаться
и про митап. а мы не хотели показать хотя бы тайпчекер ОМ? а лучше трансляцию ЕХЕ->OM? в идеале, гарантию работоспособности дает либо статья, где все выписано с подробным доказательством, либо работающий транслятор.
Namdak Tonpa
@5HT
Jul 29 2016 13:18
ну так лучше конечно
поэтому я и оттягивал это
ну я уже начал смотреть на грамматику
надо просто переписать ее немного
так то понятно что ты хочешь
есть правда несколько вопросов
Zeit Raffer
@zraffer
Jul 29 2016 13:19
давай вопросы
Namdak Tonpa
@5HT
Jul 29 2016 13:19
счас попытаюсь их вербализировать
Zeit Raffer
@zraffer
Jul 29 2016 13:19
может лучше написать больше удобоваримых примеров
а то файл "тест" просто проверяет продукции
Namdak Tonpa
@5HT
Jul 29 2016 13:19
ну примеров жизненных — там же есть у тебя папки macros.new
Zeit Raffer
@zraffer
Jul 29 2016 13:19
ага
Namdak Tonpa
@5HT
Jul 29 2016 13:20
вот они должны парсаться а не test
Zeit Raffer
@zraffer
Jul 29 2016 13:21
надо их "причесать" (синтаксис немного гулял)
основное - операторы или нотации
они пока не парсятся
надо что-то решать
Namdak Tonpa
@5HT
Jul 29 2016 13:22
(f  p
    {{x,y},{}}
    [a,{b}|c.d.e]
    :=
    \ q -> z)
вот эта конструкция мне непонятна
Zeit Raffer
@zraffer
Jul 29 2016 13:22
это ужас
Namdak Tonpa
@5HT
Jul 29 2016 13:22
LValue вроде тут неверен
нельзя присвоить что-то выражению аппликации
Zeit Raffer
@zraffer
Jul 29 2016 13:22
паттерн-метчинг
как в хаскелле
Namdak Tonpa
@5HT
Jul 29 2016 13:23
паттерн мачинг же это ->
а тут в LValue стоит :=
Zeit Raffer
@zraffer
Jul 29 2016 13:23
ну давай поменяем на стрелочку
мне все равно
парситься лучше не станет ))
Namdak Tonpa
@5HT
Jul 29 2016 13:23
ну просто ниже
(z := case f x y of
    (A, B x, C x y -> foo)
    ({
        [],
        [A],
        [B {x,y}, C x y | Q]
    } -> bar))
тут паттерн мачинг на ->
Zeit Raffer
@zraffer
Jul 29 2016 13:23
так то кейс
да надо определиться
в принципе есть разница
первый ПМ через := он тривиальный, просто переменные или таплы
Namdak Tonpa
@5HT
Jul 29 2016 13:24
(f  p
    {{x,y},{}}
    [a,{b}|c.d.e]
    :=
    \ q -> z)
вот это прокоментруй
что тут мачится на что
лямбда матчится на 4-кратную апликацию?
Zeit Raffer
@zraffer
Jul 29 2016 13:25
f берет три аргумента
и четвертый через лямбду
Namdak Tonpa
@5HT
Jul 29 2016 13:25
ну вроде по приоритету операций это
Zeit Raffer
@zraffer
Jul 29 2016 13:26
да
Namdak Tonpa
@5HT
Jul 29 2016 13:26
(((f  p)
    {{x,y},{}})
    [a,{b}|c.d.e]) :=
Zeit Raffer
@zraffer
Jul 29 2016 13:26
ну да
фигурные скобочки как в эрланге
квадратные тоже
Namdak Tonpa
@5HT
Jul 29 2016 13:26
и типа результат это должна быть конкретная лямбда с телом ?
с точностью до имен переменных?
Zeit Raffer
@zraffer
Jul 29 2016 13:27
ну да
Namdak Tonpa
@5HT
Jul 29 2016 13:27
и как это чекнется?
Zeit Raffer
@zraffer
Jul 29 2016 13:27
нормально чекнется
Namdak Tonpa
@5HT
Jul 29 2016 13:27
а в агде можно так делать?
Zeit Raffer
@zraffer
Jul 29 2016 13:27
а в чем проблема?
в агде нету списков
Namdak Tonpa
@5HT
Jul 29 2016 13:27
ну неважно я про LValue
Zeit Raffer
@zraffer
Jul 29 2016 13:28
ну да, в агде как в хаскелле
Namdak Tonpa
@5HT
Jul 29 2016 13:28
ну перепиши это в case
любой паттерн мачинг переписывается в case
Zeit Raffer
@zraffer
Jul 29 2016 13:28
case берет один аргумент
Namdak Tonpa
@5HT
Jul 29 2016 13:28
паттерн мачинг вроде в агде и хаскеле только по конструкторам
чтобы по лямбде делать ПМ я вообще не понимаю этого :-)
Zeit Raffer
@zraffer
Jul 29 2016 13:28
так тут тоже конструкторы - таплов и списков
Namdak Tonpa
@5HT
Jul 29 2016 13:29
не
ты не понял
Zeit Raffer
@zraffer
Jul 29 2016 13:29
это не ПМ по лямбде
мы чего-то недопоняли
Namdak Tonpa
@5HT
Jul 29 2016 13:29
(case (((f  p)
    {{x,y},{}})
    [a,{b}|c.d.e]) of
  (\ q -> z) -> ok
  _ -> raise)
Zeit Raffer
@zraffer
Jul 29 2016 13:29
лямбда RValue
ненене
Namdak Tonpa
@5HT
Jul 29 2016 13:29
ну как ненене
перепиши это в case чтобы я понял
что тут записано )
Zeit Raffer
@zraffer
Jul 29 2016 13:30
ты хаскелем пользовался? щас запищу
Namdak Tonpa
@5HT
Jul 29 2016 13:31
если я правильно тебя понял, то у тебя записано то что позволяет сравнивать тела функций
впринципе у нас это ок
но сомневаюсь что в Хаскеле ты это запишешь )
Zeit Raffer
@zraffer
Jul 29 2016 13:32
f := \p -> \t -> \ l -> \q -> case t of ({{x,y},{}} -> case l of ([a,{b}|cde] -> z))
вот
Namdak Tonpa
@5HT
Jul 29 2016 13:33
непонятно стало еще больше
как это равно предыдущему коду )
тут просто биндин на переменную f
а там матчинг трех аппликаций после f
совершенно разные конструкции
Zeit Raffer
@zraffer
Jul 29 2016 13:34
еще раз - ты хаскеллем пользовался?
Namdak Tonpa
@5HT
Jul 29 2016 13:34
напиши на хаскле
чтоб можно было скомпилировать
Zeit Raffer
@zraffer
Jul 29 2016 13:35
ну вот это типа на хаскелле, только там списки и наче и таплы
Namdak Tonpa
@5HT
Jul 29 2016 13:35
ну без таплов
просто f a p = \ p -> q
Zeit Raffer
@zraffer
Jul 29 2016 13:36
f p ((x,y),()) (a:tail) = \ q -> z
вот на хаскелле
Namdak Tonpa
@5HT
Jul 29 2016 13:37
ну это тоже что я написал
Zeit Raffer
@zraffer
Jul 29 2016 13:37
ну да, у меня подробней
так что здесь не так / непонятно?
:)
Namdak Tonpa
@5HT
Jul 29 2016 13:38
и если в case переписывать то \ p -> q ставится слева?
Zeit Raffer
@zraffer
Jul 29 2016 13:39
да пофиг
Namdak Tonpa
@5HT
Jul 29 2016 13:39

типа

case \p -> q of
   f a p -> ok
   _ -> rise

?

Zeit Raffer
@zraffer
Jul 29 2016 13:39
неее
это ты пробуешь метчить по лямбде
или я ты хочешь оба варианта свести к одному?..
Namdak Tonpa
@5HT
Jul 29 2016 13:41
я хочу свести твое выражение к case как универсальному PM оператору
Zeit Raffer
@zraffer
Jul 29 2016 13:41
ну я же выше свел
case берет один аргумент
тут метчатся два аргумента, значит два кейса
Namdak Tonpa
@5HT
Jul 29 2016 13:42
а почему 2?
(((f  p)
    {{x,y},{}})
    [a,{b}|c.d.e])
тут разве 2 ?
Zeit Raffer
@zraffer
Jul 29 2016 13:43
три, но первый тривиальный
для него кейс не нужен
хотя можно, конечно и ему кейс сделась ))
{{x,y},{}}
[a,{b}|c.d.e]
вот два конструктора
Namdak Tonpa
@5HT
Jul 29 2016 13:44
теперь вроде понятнее
но это шугаринг над case все равно
Zeit Raffer
@zraffer
Jul 29 2016 13:44
ну так с хаскелле и агде и идрисе это стандартный синтаксис
я сначала писал лямбды везде
но потом переехал на это
так короче и меньше лишних экзотических букв
я для простоты чтения предлагаю разрешить такой (хаскеллевский) синтаксис только для рекордов-таплов-списков, а для именованный конструкторов использовать всегда case
собственно текущая грамматика это и отражает
хотя это можно обсуждать ))
Namdak Tonpa
@5HT
Jul 29 2016 13:49
разрешить тут не то слово :-) тут надо говорить дописать дешугаринг до case для таких конструкций
там автоматически бесплатно ничего нет
т.е.
Zeit Raffer
@zraffer
Jul 29 2016 13:50
так это я как раз и собираюсь сделать
сначала дешугаринг
потом тайпчекнигг
Namdak Tonpa
@5HT
Jul 29 2016 13:50
не сначала дешугаринг - потом макросистема case - потом уже тайпчекинг
или это базовый примитим макросов?
базовые примитивы только ж по ключевым словам
Zeit Raffer
@zraffer
Jul 29 2016 13:51
макросы должны быть типизиированные
Namdak Tonpa
@5HT
Jul 29 2016 13:51
ну вот case такой макрос
только он есть
все остальное — это макросы над макросами
Zeit Raffer
@zraffer
Jul 29 2016 13:51
я хочу разобраться, как макросы сейчас выглядят в Скале и этой Андромеде
case да, должен вызывать элиминатор
т.е. макрос
Namdak Tonpa
@5HT
Jul 29 2016 13:52
а все остальное это еще один уровень дешугаринга
это хорошо что мы про это поговорили это значит что ты думаешь про паттерн мачинг и свободно в голове переводишь ) я так не умею
счас я пытаюсь избавится от ворнингов в парсере
shift/reduce
Zeit Raffer
@zraffer
Jul 29 2016 13:53
смотри, ПМ для рекордов должен быть реализован до реализации макросов, потому что макросы будут его использовать
Namdak Tonpa
@5HT
Jul 29 2016 13:53
я так и думал
что case будет на эрланге писатся
Zeit Raffer
@zraffer
Jul 29 2016 13:54
поэтому я и говорю про ограничение: хаскель-синтаксис будет вшитый, а case - макрос, хотя в принципе, первое сводится ко второму
Namdak Tonpa
@5HT
Jul 29 2016 13:54
у меня не было иллюзий увидеть case на макроязыке
Zeit Raffer
@zraffer
Jul 29 2016 13:55
case вызывает элиминатор, а элиминатор генерится вместе с типом анных уже макросами
как то так
и я напишу два варианта новой кодировки, без категорий. пока они существуют только на бумажке )
там больше думать надо не про индукцию, а про конструкторы, потому что в категорном варианте они были "автоматические", а тут я до полной общности еще не добрался
Namdak Tonpa
@5HT
Jul 29 2016 13:58
это типа на poset ?
у нас как бы есть две версии — категорная на сетоидах
и на посетах ?
или это еще компактнее?
Zeit Raffer
@zraffer
Jul 29 2016 13:58
ненене. новой упрощение.
Namdak Tonpa
@5HT
Jul 29 2016 13:58
на индукции OK ?
Zeit Raffer
@zraffer
Jul 29 2016 13:58
да
я пост напишу, а потому начну реализовывать
на бумажке уже что-то получилось ))
Namdak Tonpa
@5HT
Jul 29 2016 13:59
ясно ну я так и думал что рано или позно придется сказать Паше чтобы он все эти теоремы удалили из core )
Zeit Raffer
@zraffer
Jul 29 2016 13:59
))))
типа просветление
Namdak Tonpa
@5HT
Jul 29 2016 13:59
ага
Zeit Raffer
@zraffer
Jul 29 2016 14:00
интересная штука этот ресерч
пишешь пишешь
потом удаляеь
Namdak Tonpa
@5HT
Jul 29 2016 14:00
это не удаление, а оптимизация
Zeit Raffer
@zraffer
Jul 29 2016 14:01
именно
Namdak Tonpa
@5HT
Jul 29 2016 14:01
категорные сетоиды бишопа, потом посеты, потом на абстрактной индукции
хорошо что видны все эти каталоги
Zeit Raffer
@zraffer
Jul 29 2016 14:02
ну посеты это полумера для упрощения
Namdak Tonpa
@5HT
Jul 29 2016 14:02
можно будет еще Very Long Tale написать
Zeit Raffer
@zraffer
Jul 29 2016 14:02
вот да
Namdak Tonpa
@5HT
Jul 29 2016 14:02
хотя этот чат это оно и есть
Zeit Raffer
@zraffer
Jul 29 2016 14:02
tale надо дописать
в идеале хочется увидеть работающий компилятор, апотом дописівать, но єто еще долго
Namdak Tonpa
@5HT
Jul 29 2016 14:03
ну да пушо уже в tale.pdf там последний написаные параграф уже стал неактуальным )
Zeit Raffer
@zraffer
Jul 29 2016 14:04
вот поєтому
не, надо написать и с категориями и так, и объяснить, что они изоморфны
Namdak Tonpa
@5HT
Jul 29 2016 14:05
ну да Long Tale же
Zeit Raffer
@zraffer
Jul 29 2016 14:05
и какой-то Short
доклад
слайдами
Namdak Tonpa
@5HT
Jul 29 2016 14:05
Short — надо статья с публикацией sec2all
и все
просто распечатка терма
Zeit Raffer
@zraffer
Jul 29 2016 14:05
полмегабайта? )))
Namdak Tonpa
@5HT
Jul 29 2016 14:06
там не пол мегабайта
Zeit Raffer
@zraffer
Jul 29 2016 14:06
это же Unit
Namdak Tonpa
@5HT
Jul 29 2016 14:06
sec2all маленький
Zeit Raffer
@zraffer
Jul 29 2016 14:06
ааа
ясно
Namdak Tonpa
@5HT
Jul 29 2016 14:06
ну все классы расписать да
Zeit Raffer
@zraffer
Jul 29 2016 14:06
если нормализовать, то полмегабайта
Namdak Tonpa
@5HT
Jul 29 2016 14:06
и внимательно прочитать ту статью про "Induction Principle is not derivable"
Zeit Raffer
@zraffer
Jul 29 2016 14:07
и объяснить в чем отличие
Namdak Tonpa
@5HT
Jul 29 2016 14:07
если чувак грамотный и обложился сносками
а если действиетельно опровержение то было бы круто
Zeit Raffer
@zraffer
Jul 29 2016 14:07
ПенгФу новее
Namdak Tonpa
@5HT
Jul 29 2016 14:08
а Пенг Фу что сказал?
что derivable?
Zeit Raffer
@zraffer
Jul 29 2016 14:08
ну он там в поиске
Namdak Tonpa
@5HT
Jul 29 2016 14:08
или он тоже на эту статью ссылался?
Zeit Raffer
@zraffer
Jul 29 2016 14:08
он расширяет новыми аксиомами, чтобы получить инд.
Namdak Tonpa
@5HT
Jul 29 2016 14:08
так у нас нет новых аксиом
Zeit Raffer
@zraffer
Jul 29 2016 14:08
вот!
Namdak Tonpa
@5HT
Jul 29 2016 14:09
вообщем надо заказлить их в Short версии с опубликованым термом
Zeit Raffer
@zraffer
Jul 29 2016 14:09
ну это надо посидеть тупо недельку и разобрать все их рассуждения
т.е. применить к нашей моели
Namdak Tonpa
@5HT
Jul 29 2016 14:09
Short версию можно уже подготовить, но да главная работа будет в прочтении детальном их статей
нехочется тоже этой херней заниматься
можно вообще от них абстрагироваться и не ссылаться на них
просто сказать вот ребята держите sec2all и всем привет
Zeit Raffer
@zraffer
Jul 29 2016 14:10
все-таки работающий компилятор самое наглядное (кстати, Бауер так примерно и говорит, про "сертификаты", в этих слайдай про андромеду)
Namdak Tonpa
@5HT
Jul 29 2016 14:10
ну Бауер счас находится на стадии нас в январе
на стадии категорных сетоидов
Zeit Raffer
@zraffer
Jul 29 2016 14:11
так сейчас будет вариант без sec2all, там тупо индукция в ОК, там сложнее не вытащить ее, а показать, что мы можем таким образом оттранслировать все типы
Namdak Tonpa
@5HT
Jul 29 2016 14:17
впринципе можно взлетать на твоей гармматике
просто на ней можно булшит записать который схавается
Zeit Raffer
@zraffer
Jul 29 2016 14:19
например
Namdak Tonpa
@5HT
Jul 29 2016 14:19
в работе
Zeit Raffer
@zraffer
Jul 29 2016 14:20
я как раз думал - в качестве прототипа использовать эту грамматику, главное АСТ, для рассахаривания и тайпчекинга. а параллельно "древние мастера" доведут ее до уровня ЛАЛР(!)-пригодности :)
Namdak Tonpa
@5HT
Jul 29 2016 14:21
нет выход этой грамматики ты можешь замораживать
если я перепишу оно будет совместимым
Zeit Raffer
@zraffer
Jul 29 2016 14:21
ну вот
прекрасно! )
Namdak Tonpa
@5HT
Jul 29 2016 14:22
заодно и тесты будут
Zeit Raffer
@zraffer
Jul 29 2016 14:22
но если ты видишь "булшит" то я тоже хочу его увидеть )
Namdak Tonpa
@5HT
Jul 29 2016 14:22
если ее уже в производство запускать и генерировать что-то из нее
ну там вся простыня в ambiguous
Zeit Raffer
@zraffer
Jul 29 2016 14:23
я так понял конфликты приводят наоборот к лишним синтаксическим ошибкам
???
Namdak Tonpa
@5HT
Jul 29 2016 14:23
да ворнинги на то и ворнинги
что ничего страшного )
один удалил
ворнинг
осталось 26
:-)
Zeit Raffer
@zraffer
Jul 29 2016 14:25
ооо
прогресс
ты будешь приоритеры вводить или как-то иначе?
Namdak Tonpa
@5HT
Jul 29 2016 14:26
нет простая копипаста
я не меняю ничего
просто переставляю правила
Zeit Raffer
@zraffer
Jul 29 2016 14:26
без приоритетов там все равно неоднозначная грамматика получается
Namdak Tonpa
@5HT
Jul 29 2016 14:26
приоритеты в твоем понимании это связанное с notation ?
или обычные приоритеты умножения и сложения?
Zeit Raffer
@zraffer
Jul 29 2016 14:26
ну вот VagVagoff тут писал
Namdak Tonpa
@5HT
Jul 29 2016 14:27
так он про bottom down парсеры писал
технология примененная в OM
Zeit Raffer
@zraffer
Jul 29 2016 14:28
ок
Namdak Tonpa
@5HT
Jul 29 2016 14:28
я кстати спрашивал как это класифицировать, вот он и ответил что это Пратта
Namdak Tonpa
@5HT
Jul 29 2016 14:54
проблема твоего парсера
что у него не используется нигде служебный символ $empty
а без этого разворачивать бесконечные аппликации невозможно
странно что оно работает
Zeit Raffer
@zraffer
Jul 29 2016 14:55
если можешь, поменяй
Namdak Tonpa
@5HT
Jul 29 2016 14:55
пока не могу )
написано дохуя
Zeit Raffer
@zraffer
Jul 29 2016 14:56
$empty дает пустую строку, у меня просто все _seq подразумеваются непустыми
Namdak Tonpa
@5HT
Jul 29 2016 14:56
ну в аппликациях тоже
names        -> '$empty'                 : [].
names        -> var names                   : ['$1'|'$2'].
вот как у меня аппликация
или вот
forms        -> '$empty'                                       : [].
forms        -> form forms                                     : ['$1'|'$2'].
Zeit Raffer
@zraffer
Jul 29 2016 14:57
это последовательность "вар"ов, возможно пустая
я не думал, что тут проблема
Namdak Tonpa
@5HT
Jul 29 2016 14:57
не без $empty маловерятно что что-то будет
нет базы у рекурсии
мне непонятно как оно работает )
Zeit Raffer
@zraffer
Jul 29 2016 14:58
зачем емпти для рекурсии? рекурсия это когда я использую нетерминал в его собственной продукции
(ладно, я домой поеду, временно недоступен)...
Namdak Tonpa
@5HT
Jul 29 2016 15:01
давай
Namdak Tonpa
@5HT
Jul 29 2016 20:03
ну я избавился от ворнингов
Namdak Tonpa
@5HT
Jul 29 2016 20:30
просто прописал приоритеты