Cubical

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/anders.