These are chat archives for groupoid/exe

19th
Jul 2016
Zeit Raffer
@zraffer
Jul 19 2016 11:02
одновременно пишу трансляцию с верхнего ЕХЕ на промежуточный, чтобы типы*1 преобразовывались в сетоиды, например, и читаю монографию Джекобса, чтобы сравнить мою писанину с лучшими образцами. будет такая же категорная модель, как у него, вместо зав.типов - "расслоения", т.е. объекты слайс-категории. разница в том, что мы четко различаем размерность категорий, Prop, Setoid, Groupoid - это, соответственно, 0-, 1-, 2-категории, что позволяет компактно и единообразно описыавать происходящее на разных уровнях универсума (у Джекобса с этим мутно и неоднородно, его про верхние размерности никто не просветил, поэтому он мучительно рассматривает отдельно зав-типы, отдельно полиморфизм, отдельно логику).
Zeit Raffer
@zraffer
Jul 19 2016 14:44
надо подумать над сокращенным синтаксисом для data, как в Хаскелле/Идрисе. а то полные типы конструкторов, которые нужны для GADT, віглядят в большинстве простых случаев бойлерплейтом...
Zeit Raffer
@zraffer
Jul 19 2016 14:54
предыдущее пожелание - по мотивам того, что я рисовал абстрактный синтаксис в виде простых data. в принципе, туда можно прикрутить еще GADT, который будет учитывать типы выражений, это будет уже не АСТ на выходе парсера, а типизированный АСТ на выходе из тайпчекера.
вообще как похолодало, сразу стало веселее. а то на выходных многие города у нас побили рекорды июльской температуры, у нас было полдня по 38.
по мотивам Джекобса - он рассматривает зав типы над типами из универсумом 1, параметрический полиморфизм над кайндами из унивесума 2, а дополнитеьную логику как универсум 0. итого получается ситуация, похожая на СоС с ограниченным числом универсумов. вобщем, я тоже пока зыписываю трансляцию для *0,*1,*2 как Prop, Setoid, Groupoid - а остальные универсумы добавим впоследствии.
Zeit Raffer
@zraffer
Jul 19 2016 15:27
вообще для типов АСТ можно использовать не записи с именованными полями, как сейчас, а Erlang-style tuples вида {{a,b},{c,d}}, я не знаю, что нагляднее.