These are chat archives for groupoid/exe

7th
Jul 2016
Zeit Raffer
@zraffer
Jul 07 2016 13:14
кстати, вопрос, - мы же хотим иметь extends для record в ЕХЕ? имею предложить такой вариант, когда выбранное поле объявляется "родительским". потому что хочется иметь имя, чтобы ссылаться на него. есть ли другие предложения? на уровне типов у нас реального сабтайпинга пока не планируется, сейчас это должно работать просто на уровне "сахара" во время поиска имен полей. пример: https://github.com/groupoid/exe/blob/d0ba720914e04580074d1bd96f6f197af7eb78cd/prelude/macro.new/Data.Bool.macro#L13
Zeit Raffer
@zraffer
Jul 07 2016 13:23
и еще самый писк моды! можем ли мы ввести что-то вроде сетоидов-рекордов? т.е. очевидная структура сетоида на типе-рекорде, но не описанная бойлерплейтом по полям, а удобном синтаксисе. как это описать на уровне макросов, чтобы не хардкодить? вопрос важный, потому что это как бы первый простейший шаг к кодировке индуктивных типов - с тривиальной пока кодировкой, но с полноценной обработкой исходного АСТ-описания типа. надо бы начать думать в этом направлении. тест-кейс: чтобы следующее заработало:
(ASet : Setoid := ...) (BSet : Setoid := ...)
( RecSet : Setoid := record (A : ASet) (B : BSet) )