INTRO

Мова кубічного тайпчекера cubicaltt, синтаксис якого базується на попередній мові cubical, про яку йшлося на сторінках журналу МАКСИМ в 2017 році. Сам cubical у свою чергу базується на японському тайпчекері Mini-TT, розмір якого на мові Haskell займає 400 рядків. Синтаксис мови у БНФ нотації є максимально компактним та не передбачає ускладнених конструкції як то тайпкласи, тактики чи навіть позиційні макроси, усього цього в кубічному тайпчекері немає. Так у нього є індуктивні типи, та вищі індуктивні типи які є моделями-вбудовуваннями (моделями часу виконання) CW-комплексів, але на цьому все. Здавалося б чому так бідно, але цього виявляється цілком достатньо аби формалізувати усю математику, інші мовні можливості з легкістю реалізуються при наявності мінімальної макросистеми. Такі теорем прувери як Coq, Lean мають більш потужні можливості до препроцесінгу програм, хоча мінімальна Notation як у Coq звісно не завадила би для цієї прекрасної мінімалістичної мови.

GRAMMAR

Формальна граматика цієї мови, окрім оригінальної статті CCHM описана також в статі про мінімальну конструктивну мову MLTT, яку можна вбудувати саму в себе. Але тут представлена актуальна версія грамматики в LALR(1) флейворі, для платформи Erlang, та її бібліотек leex та yeec, токен та парсер генераторів.

LEEX

A = [a-zA-Z_0-9\-\x{2074}-\x{208E}\x{2010}-\x{2191}\x{2193}-\x{2199}\x{2201}-\x{25FF}\x{3B1}-\x{3BA}\x{3BC}-\x{3FF}] S = ([\t\s\r\n]|--.*) B = [\r\n] Star = \* Unit = \(\) Slash = \\ Dot = \. Comma = \, Arrow = (\-\>|\→) Forall = (\\/|\∀) Meet = (/\\) Lambda = (\\|\λ) Curly = [\{\}] Angle = [\<\>] Parens = [\(\)] Square = [\[\]] Colon = \: Et = \@ Eq = \= Pipe = \|

YEEC

% package system mod -> 'module' id 'where' imp dec : {module,'$2','$4','$5'}. imp -> skip imp : '$2'. imp -> '$empty' : []. imp -> 'import' id imp : [{import,'$2'}|'$3']. % ids ids -> '$empty' : []. ids -> id ids : ['$1'|'$2']. % telescopes tele -> '$empty' : []. tele -> cotele : '$1'. cotele -> '(' exp ':' exp ')' tele : {tele,uncons('$2'),'$4','$6'}. % cubical homogeneous composition systems sys -> '[' sides ']' : {sys,'$2'}. sides -> '$empty' : []. sides -> side : '$1'. sides -> side ',' sides : ['$1'|'$3']. side -> '(' id '=' id ')' arrow exp : {side,'$2','$4','$7'}. formula -> formula forall f1 : {join,'$1','$3'}. formula -> f1 : '$1'. formula -> f2 : '$1'. f1 -> f1 meet f2 : {meet,'$1','$3'}. f1 -> f2 : '$1'. f2 -> '-' f2 : {neg,'$2'}. f2 -> id : '$1'. % core expression exp -> 'split' cobrs : {split,'$2'}. exp -> id : '$1'. exp -> id '{' exp '}': {inst,'$1','$h3'}. exp -> '<' ids '>' exp : {plam,uncons('$2'),'$4'}. exp -> exp '.1' : {fst,'$1'}. exp -> exp '.2' : {snd,'$1'}. exp -> lam cotele arrow exp : {lam,'$2','$4'}. exp -> cotele arrow exp : {pi,'$1','$3'}. exp -> exp arrow exp : {pi,'$1','$3'}. exp -> cotele '*' exp : {sigma,'$1','$3'}. exp -> 'comp' exp exp sys : {comp,'$2','$3','$4'}. exp -> 'fill' exp exp sys : {fill,'$2','$3','$4'}. exp -> 'glue' exp sys : {glue,'$2','$3'}. exp -> 'unglue' exp sys : {unglue,'$2','$3'}. exp -> exp ',' exp : uncons_p('$1','$3'). exp -> papp : '$1'. exp -> '(' exp ')' : '$2'. exp -> app : '$1'. % lambda and path applications app -> exp exp : {app,'$1','$2'}. papp -> exp '@' formula : {papp,'$1','$3'}. % top level inductive data and function declarations dec -> '$empty' : []. dec -> codec : '$1'. codec -> def skip dec : ['$1'|'$3']. codec -> def dec : ['$1'|'$2']. def -> 'data' id tele '=' sum : {data,'$2','$3','$5'}. def -> id tele ':' exp '=' exp : {def,'$1','$2','$4','$6'}. def -> id tele ':' exp '=' exp 'where' def : {def,'$1','$2','$4','$6','$8'}. % inductive and HIT introductions sum -> '$empty' : []. sum -> rsum : '$1'. rsum -> id tele : {ctor,'$1','$2'}. rsum -> id tele '|' rsum : [{ctor,'$1','$2'}|'$4']. rsum -> id tele '<' ids '>' sys : {htor,'$1','$2','$4','$6'}. rsum -> id tele '<' ids '>' sys '|' rsum : [{htor,'$1','$2','$4','$6'}|'$8']. % inductive and HIT eliminators cobrs -> '|' br brs : ['$2'|'$3']. br -> ids arrow exp : {br,'$1','$3'}. br -> ids '@' ids arrow exp : {br,'$1','$3','$5'}. brs -> '$empty' : []. brs -> cobrs : '$1'. Nonterminals mod imp tele exp app dec def ids sum cotele rsum br brs cobrs codec formula f1 f2 side sides sys papp. Terminals id digits atom oper skip lam meet arrow forall '(' ')' '[' ']' '<' '>' '{' '}' '.' ',' ':' '=' '#' '|' '-' '*' '/' '@' '0' '1' 'module' 'where' 'import' 'record' 'data' 'split' 'let' 'in' '.1' '.2' 'comp' 'fill' 'glue' 'unglue'.

RUN

Для запуску кубічного синтаксичного фронтенду скористайтеся MAD.

$ git clone git://github.com/groupoid/homotopy && cd homotopy $ mad compile release homotopy $ ./homotopy parse file core/mltt.ctt

Адреса репозиторію — groupoid/homotopy.