OM: Lambda Assembler Сегодня откомпилировалась базовая библиотека Морте с помощью Om. Эсктраченый эрланг код на индуктивных списках вроде работает (то что я постил раньше, фолд миллиона элементов). Нужно больше тестов. Размер компилятора пока занимает 400 строк кода. Непрошло и три месяца как Групоид Инфинити, Инк. написала компилятор с зависимыми типами для Erlang инфраструктуры — как раз к проведению конференции Erlang Factory. Скоро вы сможете забыть про лямбда куб обычный и с наслаждением войти в неизведанный Космический Куб — полную чашу Инфиниту Групоидов и Инфинити Моноидов, и все это на старом добром говне мамонта Эрланге 86 года выпуска. А также js и других нетипизированных языков, которые нас интересуют в гораздо меньшей мере. Ом работает в MLTT сеттинге и реализует модель PTS, где основные параметры — сорта, аксиомы и правила вывода, задаются с помощью формул, а не с помощью перечислений, или как еще говорят предикативная модель: S = *{n}, n : nat A = *{i} : *{i+1} R = *{i} -> *{j} : *{max i j} Детальное описание этих параметров смотрите в Lambda Calculi with Types Хенка Барендрегта, а также статью Henk: Intermediate Language Саймона Пайтона и Эрика Мейера. Таким образом, можно говорить о том, что Ом в своей теоритической основе не хуже чем Agda, Lean, Coq и другие MLTT пруверы. Отличает его только то, как вы знаете уже по моим прошлым постам, что он внутри все элиминаторы и кодировщики индуткивных титпов реализует посредством своей макросистемы, а не как вшитые в ядро тайпчекера типы. Ближе всех из существующих пруверов — это божественный и самый быстрый в мире CiC прувер Lean. Если вы не пробовали еще плагин emacs для Lean, быстро пробуйте и сравните с коковским ProofGeneral. Небо и земля! Мы в Lean тестируем термы и строим метамодель кодировщика -- фибрационные диалгебры и взятие их лимитов. > 'List': '(<=<)'/0 '(<|>)'/0 '(=<<)'/0 '(>=>)'/0 '(>>=)'/0 'Cons'/0 'Nil'/0 all/0 any/0 concat/0 empty/0 length/0 map/0 module_info/0 module_info/1 null/0 pure/0 replicate/0 reverse/0 > 'Nat': '(*)'/0 '(+)'/0 '0'/0 'Succ'/0 'Zero'/0 module_info/0 module_info/1 odd/0 product/0 sum/0 > 'Bool': 'False'/0 'True'/0 'and'/0 'not'/0 'or'/0 module_info/0 module_info/1 > 'Maybe': '(<=<)'/0 '(<|>)'/0 '(=<<)'/0 '(>=>)'/0 '(>>=)'/0 '0'/0 'Just'/0 'Nothing'/0 empty/0 map/0 module_info/0 module_info/1 pure/0 Напоминаю как пользоваться OM: $ brew install erlang $ wget https://github.com/groupoid/om/releases/download/0.3/om $ chmod +x om $ ./om Ом мониторит директорию стандартную директорию для Erlang'а — "priv", в которой находятся каталоги с разными кодировками Church, Scott, а возможно и с разными прелюдиями и типами. В поставку Ом входят два закодированных парадокса: Жирара и Хуркенса, которые Ом должен будет схватить, как только мы пофиксаем все ошибки. $ om modes list ["girard","hurkens","hurkens-src","normal","setoids"] Ом обладает набором комбинаторов, которые вы можете выстраивать в пайп: $ om help me [{a,[expr],"to parse. Returns {_,_}=Term or {error,_}."}, {type,[term],"typechecks and returns Type term."}, {erase,[term],"to untyped term. Returns {Term,Type}."}, {file,[name],"load file as binary."}, {str,[binary],"lexical tokenizer."}, {parse,[tokens],"parse given tokens into {_,_} term."}, {fst,[{x,y}],"returns first element of a pair."}, {snd,[{x,y}],"returns second element of a pair."}, {debug,[bool],"enable/disable debug output."}, {mode,[name],"select metaverse folder."}, {modes,[],"list all metaverses."}] Покажем на примере: $ om fst erase a "#List/Cons" , mode normal ok {{"λ",{'Head',0}}, {any,{{"λ",{'Tail',0}}, {any,{{"λ",{'Cons',0}}, {any,{{"λ",{'Nil',0}}, {any,{app,{{app,{{var,{'Cons',0}},{var,{'Head',0}}}}, {app,{{app,{{var,{'Tail',0}},{var,{'Cons',0}}}}, {var,{'Nil',0}}}}}}}}}}}}}} Сам Ом, будучи консольной утилитой, имеет также встроенный шел (Эрланг шелл). Просто запустите его без параметров. $ om > [ {A,C} || {A,C,_} <- om:all() ]. [{"hurkens","PASSED"}, {"normal","PASSED"}, {"setoids","PASSED"}, {"src-hurkens","PASSED"}] > om:mode("setoids"). > om:snd(om:erase(om:a("#DEP.AND"))). {star,1} Надеюсь вам понравится! Все это стало возможным благодаря ZEIT_RAFFER и NPONECCOP, которые непокладая сил думают над устройством внутреннего языка пространства :-) __________________ [1]. http://groupoid.space/pts/pure [2]. https://github.com/groupoid/om