These are chat archives for groupoid/exe

29th
Jun 2016
Zeit Raffer
@zraffer
Jun 29 2016 11:00
начал писать более разнообразные индуктивные типы, и сразу выясняется, что надо дописывать к сетоидам те куски определения категории, которые я выкинул. предварительные ощущения такие, что для полноценного макроса, который будет обрабатывать произвольное определение индуктивного типа (через профункторы и орнаменты, или еще как), нам все равно понадобятся все категорные определения из библиотечки на Леан. отака фигня, малята. сократить рабочий прототип для Empty+Unit удалось только за счет того, что конструкторы были очень простые. с другой стороны, Bool можно сделать на той же сложности, что и сейчас.
Zeit Raffer
@zraffer
Jun 29 2016 13:05
пока пишу некоторые размышления о языке макросов и как он будет отображаться в ОМ в это файл https://github.com/groupoid/exe/blob/da0fa230864af07d822251a3b392afd995c86e52/prelude/macross-0/guidelines
на данный момент назрел вопрос об унификации записей-рекордов-модулей-неймспейсов
предлагается использовать два ключевых слова record для типа записи и new для ее конструктора, а то, что раньше было def считать полями объемлющей записи. такой подход вполне согласуется с трансляцией полей в отдельные файлы директории.
Zeit Raffer
@zraffer
Jun 29 2016 13:10
или вместо сочетания new record можно ввести ключевое слово module? но я не знаю, какой вариант минимальнее...
Zeit Raffer
@zraffer
Jun 29 2016 13:20
и еще я не писал еще в чат про такой удобный подход - (1) значения аргументов конструктора можно делать именованными new ... ( fN := fV )... - так гораздо нагляднее; (2) если тип данного поля - это функция ∀(a:T)->..., то вместо задания значения поля как лямбды ( fN := λ (a:T)->...), можно использовать сахарный синтаксис (fN a := ...) - так короче и нагляднее (как бы тривиальный паттерн-метчинг).