gds
24.03.2012 18:06 umodniD58387E2
I heard Coq like types, so we put type in your type so you can type your types while you are typing your types.
и больше ничего не могу сказать про текущие дела :)
7 comments
recommend
bookmark
subscribe
having fun, i see ..
да там такие задачки пошли, что либо metaocaml и кодогенерилку (в чятике ещё чесал репу на эту тему), либо coq (и упрощённую кодогенерилку, по крайней мере в случае окамла), либо прочие "зависимые типы" (агдочька, например).
Но кодогенерю только в окамл! Расово, православно, верно!
реквестирую больше постов про прелести coq'a — а то пока все это попахивает какими то нездоровыми извращениями :)
прелести для реальных задач ofc
эх, сам хочу :) Пока да, извращения. Так же, как ньюб, изучающий камло с его типами и прочим, считает это извращением относительно сишечьки.
Много чего ковырял, но многое ниасилил. Сейчас ковыряю ermine'овские комбинаторы. Там получится, думаю.
так ты пиши чего ковыряешь, чего не осилил — чтобы пасаны были в курсе :)
в камлочятик не хочу, а так — сходу, ниасилил мутабельность (массивы из примера ygrek'а), мутабельные строки (для своих грязных делишек), и там либо манатки, либо линейные/уникальные типы, что в принципе однохуйственно. Либо ещё один трюк, гораздо более легковесный, но я пока не проверил его, буду ещё думать-пробовать.
Из текущих вопросов — не понимаю, как заматчить тип (т.е. то, что в окамле принципиально нельзя, потому "готовых решений" в голове нет).
А так — спортировал ermine'овские комбинаторы на coq, экстрактится ровно в тот же код, который был написан на окамле руками, и это хорошо.
кроме того, вот я напишу — "ниасилил императивщину" — и у людей будет впечатление о том, что императивщину в coq нельзя никак реализовать? Это же неправда будет.