> Проект мой касался генерации примитивных sql-запросов из dsl. На вход подавалась структура данных (разобранная из json over http, и разбор на окамле сделать было чуть разумнее из-за причин, выходящих за рамки этого поста), и на её основании нужно было сгенерить запрос, учитывающий описанную в coq схему базы данных (ту её часть, которая необходима для генерации запроса). В том числе, там были поля с автоматической группировкой и необходимость создавать вложенные sql-запросы, со всякими там алиасами столбцов и их использованием во внешнем запросе.
А в результате: Венедикт Ерофеев Монатки-петушки.
В любом случае крутой опыт. Только по тексту я не сумел сопоставить, что из изложенного каким частям задачи соответствует. То есть какие части получились чистыми с доказательствами, какие императивными. Тем более, если речь идет о создании маленкого компилятора, откуда там столько грязного кода, что монадами не выравнивается, какая-то динамика с типом-свидетелем. Столько всего.
да так и было! Впечатление абсолютно правильное. Ещё coq, что само по себе переводится как "петух".
Однако, расскажу подробнее про части. Чистые с доказательствами -- типы, кое-какие мелкие инварианты над ними, eq_dec над этими типами, "ассоциативный список с уникальными ключами", ещё какие-то мелочи. Чистые без доказательств -- в основном, функции, не требующие ни состояния, ни ошибок при обработке запросов. Их где-то половина среди всех функций, но они мелкие. Остальное -- грязно. Впрочем, х-исты такое "грязное" оправдывают (и отмывают штоле), у них это "чистое, но монадное". Ну, бывает.
Монадами -- выравнивается. "Мировую манатку" сделал -- и ЗБС.
Тип-свидетель -- это то, что меня отчасти сподвигло на модные типы, он упомянут скорее в качестве вступления, чтобы не было _совсем уж_ впечатления, что я _ебанутый_, и от нехуй делать полез работать работу на coq. Предпосылки были, давно уже. Это хоть как-то меня оправдывает.
да, кто-то говорил такое. Я даже скорее всего не имел тебя ввиду тут, хотя как-то давно мы что-то такое обсуждали, и ты был не в восторге от тактик. Но это было слишком давно. А про "тактики -- не модно" я слышал вполне таки недавно, в пределах полугода.
Comments 16
> Проект мой касался генерации примитивных sql-запросов из dsl. На вход подавалась структура данных (разобранная из json over http, и разбор на окамле сделать было чуть разумнее из-за причин, выходящих за рамки этого поста), и на её основании нужно было сгенерить запрос, учитывающий описанную в coq схему базы данных (ту её часть, которая необходима для генерации запроса). В том числе, там были поля с автоматической группировкой и необходимость создавать вложенные sql-запросы, со всякими там алиасами столбцов и их использованием во внешнем запросе.
А в результате: Венедикт Ерофеев Монатки-петушки.
В любом случае крутой опыт. Только по тексту я не сумел сопоставить, что из изложенного каким частям задачи соответствует. То есть какие части получились чистыми с доказательствами, какие императивными. Тем более, если речь идет о создании маленкого компилятора, откуда там столько грязного кода, что монадами не выравнивается, какая-то динамика с типом-свидетелем. Столько всего.
Reply
да так и было! Впечатление абсолютно правильное. Ещё coq, что само по себе переводится как "петух".
Однако, расскажу подробнее про части.
Чистые с доказательствами -- типы, кое-какие мелкие инварианты над ними, eq_dec над этими типами, "ассоциативный список с уникальными ключами", ещё какие-то мелочи.
Чистые без доказательств -- в основном, функции, не требующие ни состояния, ни ошибок при обработке запросов. Их где-то половина среди всех функций, но они мелкие.
Остальное -- грязно.
Впрочем, х-исты такое "грязное" оправдывают (и отмывают штоле), у них это "чистое, но монадное". Ну, бывает.
Монадами -- выравнивается. "Мировую манатку" сделал -- и ЗБС.
Тип-свидетель -- это то, что меня отчасти сподвигло на модные типы, он упомянут скорее в качестве вступления, чтобы не было _совсем уж_ впечатления, что я _ебанутый_, и от нехуй делать полез работать работу на coq. Предпосылки были, давно уже. Это хоть как-то меня оправдывает.
Reply
Reply
Reply
CPDT давно в 2read списке, но все боялся за нее взяться. И еще побоюсь какое-то время.
Reply
> породив вместо неё ещё несколько
Агдовое так и работает.
Только вот, откуда ты взял про "пацанов" и "тактики-немодно"?
Лично я этого не говорил и не думал. Кто-то таки говорил?
Reply
Reply
Reply
Reply
Leave a comment