These are chat archives for groupoid/exe

26th
Mar 2016
Zeit Raffer
@zraffer
Mar 26 2016 06:58
.{0,0,0} в таком случае были бы не три аргумента, а один аргумент типа Level, просто левелы звездочек у нас могут быть сложные (для контекстов). мы разрешаем подставить последовательность из нескольких уровней в любое место, где есть один аргумент .{u} и это все равно будет один аргумент.
по смыслу это означает, что у нас несколько физических файлов в подкаталоге, которые рассматриваются как одно логическое значение-рекорд
.{0}.{0}.{0} означает три аргумента простого уровня 0 (в данном случае - кодировку вида Prop->Prop->Prop)
Zeit Raffer
@zraffer
Mar 26 2016 07:08
(сначала я хотел отделить тему сложных кодировок, но увидел, что они используются постоянно с самого начала)
Zeit Raffer
@zraffer
Mar 26 2016 08:12
придумал альтернативу .{}.{}.{} - использовать для аргументов уровней одну карли, а сложные аргументы брать в круглые скобочки. тогда кодировка будет выглядеть как encoding.{0 0 0} зато тип типа сетоидов чуть сложнее Type.{(u,1,1,0,0,0)}. теоретически можно разрешить вложенные круглые скобочки, чтобы отражать вложенные подкаталоги (на уровне файловой системы), хотя на уровне теории типов вложенность скобок ничего особого значить не будет (то же самое каррирование).
при такой форме записи у нас цифре соответствует файл, а круглой скобочке - каталог, - всё достаточно просто.
ну что, так будет лучше?
Namdak Tonpa
@5HT
Mar 26 2016 09:12
пока если чесно нифига не понял (в частности "цифра — каталог") :-)
Zeit Raffer
@zraffer
Mar 26 2016 09:13
пример - ((1,2),(3,4)) - означает каталог с двумя подкаталогами, в каждом их которых по ДВУМ файлам
Namdak Tonpa
@5HT
Mar 26 2016 09:14
так а что это, иерархия контекстов?
Zeit Raffer
@zraffer
Mar 26 2016 09:14
ага
Namdak Tonpa
@5HT
Mar 26 2016 09:14
шото я такого никогда не видел
Zeit Raffer
@zraffer
Mar 26 2016 09:14
это кодировка, основанная на контекстах
Namdak Tonpa
@5HT
Mar 26 2016 09:14
тут бы самое место пейпер почитать ненаписаный :-)
давай с самого начала
Type.{u} — это конкретный типы в конкретной вселенной
Type.{u+1,1,1,0,0,0} — это составной тип (рекорд) разбросаный по 6 вселенным 5 из которых всегда одни и те же
Zeit Raffer
@zraffer
Mar 26 2016 09:16
уточнение
Namdak Tonpa
@5HT
Mar 26 2016 09:16
ты говоришь что он состоит из 6 файлов
Zeit Raffer
@zraffer
Mar 26 2016 09:16
вместо u можно подставлять контекст
Namdak Tonpa
@5HT
Mar 26 2016 09:16
я правильно тут понимаю?
Zeit Raffer
@zraffer
Mar 26 2016 09:17
правильно с поправкой на "вместо u можно подставлять контекст"
Namdak Tonpa
@5HT
Mar 26 2016 09:17
файлы 2-3 будут содержать *1, а файлы 3-6 будут содержать *0
Zeit Raffer
@zraffer
Mar 26 2016 09:17
да
Namdak Tonpa
@5HT
Mar 26 2016 09:17
а теперь покажи мне первый файл u+1 который
Zeit Raffer
@zraffer
Mar 26 2016 09:18
надо подставить что-то вместо u, например 1, тогда получится файл *2
Namdak Tonpa
@5HT
Mar 26 2016 09:19
т.е. файла не будет, только после приложения макроса к входному AST
Zeit Raffer
@zraffer
Mar 26 2016 09:20
ага
Namdak Tonpa
@5HT
Mar 26 2016 09:20
так а SetoidType.{u} тогда макрос чтоли?
это ж тип с полиморфной вселенной
Zeit Raffer
@zraffer
Mar 26 2016 09:21
это полиморфный терм
ну да
Namdak Tonpa
@5HT
Mar 26 2016 09:21
он же может инстанциироваться даже в рантайме
ты не сможешь создавать файлы в рантайме
Zeit Raffer
@zraffer
Mar 26 2016 09:21
похоже, что в рантайме не может
Namdak Tonpa
@5HT
Mar 26 2016 09:22
ну так а во что тогда этот макрос развернуть?
Zeit Raffer
@zraffer
Mar 26 2016 09:22
разрешаем инстанциироваться только при компиляции
Namdak Tonpa
@5HT
Mar 26 2016 09:22
я хочу пример вот язык (макро-0) и вот код на ОМ в который он будет разворачиваться
первое вроде есть
вот счас я хочу увидеть u+1 файл )
Zeit Raffer
@zraffer
Mar 26 2016 09:23
вот этот файл я перепишу на ОМ, только надо придумать, как мы маркируем полиморфные аргументы
Namdak Tonpa
@5HT
Mar 26 2016 09:23
в ОМ?
Zeit Raffer
@zraffer
Mar 26 2016 09:24
ну мы уже говорили, что надо сделать в ОМ полиморфные звездочки
Namdak Tonpa
@5HT
Mar 26 2016 09:24
ну т.е. чтобы заэкспандить этот макрос то так и будет типа
Zeit Raffer
@zraffer
Mar 26 2016 09:24
подстановка сложного u это трансформация АСТ
Namdak Tonpa
@5HT
Mar 26 2016 09:24
$ cat ST1
*{u+1}
?
Zeit Raffer
@zraffer
Mar 26 2016 09:24
ага
одно из двух ))
на самом деле не только звездочки - любой терм может принимать аргументы .{}
Namdak Tonpa
@5HT
Mar 26 2016 09:25
и это типа в общем случае надо будет генерировать уникальные имена типов для каждой ячейки каждого рекорда
Zeit Raffer
@zraffer
Mar 26 2016 09:25
именно
Namdak Tonpa
@5HT
Mar 26 2016 09:26
хорошо
Zeit Raffer
@zraffer
Mar 26 2016 09:26
я думаю через точку у имени аргумента
или есть другие предложения?
Namdak Tonpa
@5HT
Mar 26 2016 09:27
ага
т.е. тема такая что введя полиморфные вселенные без инферера мы теперь обязуемся их эксплисит везде указывать
Zeit Raffer
@zraffer
Mar 26 2016 09:27
надо продумать так, чтобы ОМ не знал ничего про контексты, но мог использовать переменные уровня
разворачивание оставить для макросов
Namdak Tonpa
@5HT
Mar 26 2016 09:28
ну так нельзя же выразить u+1 на ом
или создавать файлы только когда макросы используются
и тогда только в момент компиляции
а ну да так может быть
Zeit Raffer
@zraffer
Mar 26 2016 09:28
u+1 можно (должно быть можно), а (u,1) - нельзя (это трансформация)
u+1 это один файл
Namdak Tonpa
@5HT
Mar 26 2016 09:29
ну тут два файла будет
но все равно он создадутся в момент компиляции и все
и там будут константы
*6 и *1 например
Zeit Raffer
@zraffer
Mar 26 2016 09:29
(u,1) это два файла, их генерирует макрос
Namdak Tonpa
@5HT
Mar 26 2016 09:29
ну я ж и говорю
Zeit Raffer
@zraffer
Mar 26 2016 09:30
дело в том, что если у нас несколько разных переменных, то надо указывать их в ОМ, чтобы отличать
Namdak Tonpa
@5HT
Mar 26 2016 09:30
так у рекордов есть же поля
Zeit Raffer
@zraffer
Mar 26 2016 09:30
не поля, а просто разные переменные, разного типа
A->B
оба из разных переменных универсумов
Namdak Tonpa
@5HT
Mar 26 2016 09:31
... -> \ (A: *6) -> \ (B: *1) -> ...
ну вот так в рекорде будет после инлайна
в момент разворачивания макроса
Zeit Raffer
@zraffer
Mar 26 2016 09:32
не в одном рекорде
просто две переменные в терме
мы должны подставить что-то вместо первого уровня и что-то вместо второго - как нам их отличить?
Namdak Tonpa
@5HT
Mar 26 2016 09:33
параметры типа?
то что база, до := ?
так параметры мы тоже знаем на этапе компиляции и применения макроса
Zeit Raffer
@zraffer
Mar 26 2016 09:35
терм может иметь несколько переменных уровня, которые используются для типизации аргументов внутри терма. например, я могу захотеть вместо Prop в сетоиде использовать произвольный универсум *{v}, тогда нужно будет указывать в модифицированном сетоиде SetoidType.{u v}
Namdak Tonpa
@5HT
Mar 26 2016 09:35
т.е. реально абстракные переменные вселенных без привязки к полям рекорда или параметрам типа
Zeit Raffer
@zraffer
Mar 26 2016 09:35
да
Namdak Tonpa
@5HT
Mar 26 2016 09:36
ясно
Zeit Raffer
@zraffer
Mar 26 2016 09:36
да и просто один аргумент. нужно отличать произвольный {u} от фиксированного {1} на уровне тайпчекера.
Namdak Tonpa
@5HT
Mar 26 2016 09:36
ну все равно я думаю это все можно вынести в macro-0
а до тайпчека будут доходить уже развернуе константы
как и до синтаксиса ом
Zeit Raffer
@zraffer
Mar 26 2016 09:36
я не вижу как сделать это "отличать произвольный {u} от фиксированного {1} на уровне тайпчекера" без поддержки ОМ
Namdak Tonpa
@5HT
Mar 26 2016 09:37
так а не будет произвольного
будет либо * либо *N
или надо отличать u от v ?
Zeit Raffer
@zraffer
Mar 26 2016 09:37
тогда мы не сможем компилировать и тайпчекать библиотеку )) а только полную программу, полностью с подставленными 1 2 3 ))))
Namdak Tonpa
@5HT
Mar 26 2016 09:38
именно
Zeit Raffer
@zraffer
Mar 26 2016 09:38
так это фигня
Namdak Tonpa
@5HT
Mar 26 2016 09:38
для тайпчека библиотеки могут быть заглушки
Zeit Raffer
@zraffer
Mar 26 2016 09:38
например
Namdak Tonpa
@5HT
Mar 26 2016 09:38
которые подставляют параметры вселенных
Zeit Raffer
@zraffer
Mar 26 2016 09:38
u=1000, v=1000000 ?
Namdak Tonpa
@5HT
Mar 26 2016 09:38
а ну все равно надо в тайпчекер
раз теория
Zeit Raffer
@zraffer
Mar 26 2016 09:39
иначе у нас получатся юнит-тесты для уровней универсума ))
Namdak Tonpa
@5HT
Mar 26 2016 09:39
ну тогда макро язык сможет еще сократится если мы предикаты в звезды добавим в ом?
или уже нет?
Zeit Raffer
@zraffer
Mar 26 2016 09:39
предикаты?
что значит предикаты
Namdak Tonpa
@5HT
Mar 26 2016 09:40
.{u}
.{max u v}
.{u+1}
Zeit Raffer
@zraffer
Mar 26 2016 09:40
экспрешены ))
Namdak Tonpa
@5HT
Mar 26 2016 09:40
надо тогда в ОМ сначала это добавить
Zeit Raffer
@zraffer
Mar 26 2016 09:40
похоже, что придется добавить
Namdak Tonpa
@5HT
Mar 26 2016 09:40
чтобы потестить
Zeit Raffer
@zraffer
Mar 26 2016 09:40
ага
экспрешены в ОМ надо, контексты (1,2,3) не надо
Namdak Tonpa
@5HT
Mar 26 2016 09:41
ну понятно, контексты только в macro-0 же будут?
Zeit Raffer
@zraffer
Mar 26 2016 09:41
да
Namdak Tonpa
@5HT
Mar 26 2016 09:41
в EXE их не будет
Zeit Raffer
@zraffer
Mar 26 2016 09:41
да
Namdak Tonpa
@5HT
Mar 26 2016 09:41
ясно, ну мне все понятно
Zeit Raffer
@zraffer
Mar 26 2016 09:41
еще одно
на уровне макросов ты видишь, что аргументы уровня описываются в def напротив идентификатора
а куда их совать в ОМ?
Namdak Tonpa
@5HT
Mar 26 2016 09:43
ну я пока это не очень понимаю
let Setoid.HomType.{u} (A B : SetoidType.{u}) :
 Type.{u,0} := record.{onEl.1, (churchAnd onEl.2 onEqu)}
:-)
Zeit Raffer
@zraffer
Mar 26 2016 09:44
первый u это декларация аргумента
Namdak Tonpa
@5HT
Mar 26 2016 09:44
я думаю вопрос состоит в том что тут дофига { }
Zeit Raffer
@zraffer
Mar 26 2016 09:44
второй для тайпчекинга типа-результата
третий, чтобы показать, как отображаются поля
у третьего свой синтаксис, на макросах
придумай проще )))
Namdak Tonpa
@5HT
Mar 26 2016 09:46
надо листочек взять порисовать )
ну я понял что начинать надо все равно с парсера { }
чтобы передать тебе их в тайпчекер
а там ты разберешься и скажешь чего нехватает
Zeit Raffer
@zraffer
Mar 26 2016 09:46
тут я исходил из того, что сложной типовыводилки на макросах не будет, ее мы сделаем только для ЕХЕ, возможно через макросы, поэтому в любом полиморфном месте надо явно указывать уровни универсума
кстати в Агде тоже везде указывают
там нет выводилки универсумов
Namdak Tonpa
@5HT
Mar 26 2016 09:47
ну и отлично
Zeit Raffer
@zraffer
Mar 26 2016 09:47
это объясняет, почему тут столько карли бракетс
Zeit Raffer
@zraffer
Mar 26 2016 11:42
ты скажи лучше по конкретному синтаксису - есть еще вопросы или предложения? и @nponeccop желательно тоже чтобы высказался. чтобы увидеть возможные подводные камни и исправить сразу.
nponeccop
@nponeccop
Mar 26 2016 15:06
я не могу высказаться, поскольку не владею материалом
мне на конкретный синтаксис плевать, равно как и на выведение вселенных. А по поводу высокоуровневого дизайна ("что делать в каком компоненте") - всё равно потом рефакторить, я бы сделал как попало, а потом поперемещал между уровнями индирекшона
Zeit Raffer
@zraffer
Mar 26 2016 15:38
"всё равно потом рефакторить" это радикальный подход, конечно :) спасибо
nponeccop
@nponeccop
Mar 26 2016 15:40
а если вотерфолл дизайн хотите - то надо требования как-то сформулировать документально, и можно будет задизайнить.. без четких требований только хуяк-хуяк
Zeit Raffer
@zraffer
Mar 26 2016 16:21
и где тут вотерфолл? )) просто спросили твое мнение об этих набросках синтаксиса, может свежим взглядом видно какую тупую дыру, которую я пропустил. без всякого вотерфолла это надо превращать в грамматику.
Zeit Raffer
@zraffer
Mar 26 2016 17:11
993879_1711775445729066_6806647880230757033_n.jpg