okram

mmlang> :[model,mm][define,tree<=[?0|(int;tree;int)]]
==>_[define,tree<=_[_{?}<=_[is,bool<=_[a,0]]|(int;tree;int)]]
mmlang> 0 => tree
==>tree:0
mmlang> 1 => tree
language error: 1 is not a tree
mmlang> (1;0;1) => tree
==>tree:(1;tree:0;1)
mmlang> (1;(2;0;2);1) => tree
==>tree:(1;tree:(2;tree:0;2);1)

okram

mmlang> 1
==>1
mmlang> 1-<(_;_)
==>(1;1)
mmlang> 1-<(_;_)=(vertex;vertex)
==>(vertex:('id'->nat:1);vertex:('id'->nat:1))
mmlang> 1-<(_;_)=(vertex;vertex)=>edge
==>edge:('outV'->vertex:('id'->nat:1),'inV'->vertex:('id'->nat:1))
mmlang>
mmlang>

okram

List(edge<=(vertex;vertex)[split,('outV'->vertex<=(vertex;vertex)[get,0,_],'inV'->vertex<=(vertex;vertex)[get,1,_])])
List(cmplx:(real;real), <x>, cmplx<=cmplx:(real;real)<x>, [plus,cmplx<y>]{2}, [combine,(real;real){2}], cmplx:(real;real){2})
List(attr:('key'->_,'value'->_))
List(digraph#1105759305:('type'->([inst]->([inst]),attr->(attr:('key'->_,'value'->_),attr<=(str;_[id])[split,('key'->str<=(str;_[id])[get,0,_],'value'->_<=(str;_[id])[get,1,_])]),nat->(nat<=int[is,bool<=int[gt,0]]),cmplx:(real;real){2}->(cmplx{2}<=cmplx:(real;real)<x>[plus,cmplx<y>]{2}),bool->(bool),real->(real),str->(str),cmplx:(real;real)->(cmplx:(real;real)),rec->(rec),int->(int<=vertex[get,'id',_],int<=nat,int),edge->(edge:('outV'->vertex,'inV'->vertex),edge<=(vertex;vertex)[split,('outV'->vertex<=(vertex;vertex)[get,0,_],'inV'->vertex<=(vertex;vertex)[get,1,_])]),(_)->((_)<=(_[id]),(_)),(int)->((int)<=(int[neg][neg]),(int)<=(int[plus,0]),(int)<=(int[mult,1]),(int)),(_[1])->((_[1])<=(int[one]),(_[1])),(_[0])->((_[0])<=(int[zero]),(_[

okram

{"id":{"@type":"g:Int64","@value":0},"label":"type","properties":{"iso":[{"id":{"@type":"g:Int64","@value":3},"value":{"empty":true,"serial":false,"choice":false,"plus":false,"parallel":false}}],"obj":[{"id":{"@type":"g:Int64","@value":1},"value":{"empty":true,"serial":false,"choice":false,"plus":false,"parallel":false}}],"root":[{"id":{"@type":"g:Int64","@value":2},"value":true}]}}
{"id":{"@type":"g:Int64","@value":64},"label":"type","inE":{"noop":[{"id":{"@type":"g:Int64","@value":68},"outV":{"@type":"g:Int64","@value":17},"properties":{"iso":{"empty":true,"serial":false,"choice":false,"plus":false,"parallel":false},"obj":{"empty":true,"serial":false,"choice":false,"plus":false,"parallel":false}}}]},"properties":{"iso":[{"id":{"@type":"g:Int64","@value":67},"value":{}}],"obj":[{"id":{"@type":"g:Int64","@value":65},"value":{}}],"root":[{"id":{"@type":"g:Int64","@value":66},"value":false}]}}
{"id":{"@type":"g:Int64","@value":4},"label":"type","inE":{"split":[{"id":{"@type":"g:Int64","@value":16},"outV":{"@typ

okram

mmlang> :[model,mm]                                              // the base model (int,bool,real,str,lst,rec)
......>  [define,
......>    vertex<=rec,                                          // a vertex is a sort of record
......>    vertex<=int-<('id'->_),                               // a vertex can be constructed from an int
......>    edge<=rec,                                            // an edge is a sort of record
......>    edge<=(vertex;vertex)-<('source'->.0,'target'->.1)]   // an edge can be constructed from a vertex x vertex pair
==>_[define,vertex<=rec,vertex<=int[split,('id'->int)],edge<=rec,edge<=(vertex;vertex)[split,('source'->vertex<=(vertex;vertex)[get,0,_],'target'->vertex<=(vertex;vertex)[get,1,_])]]

mmlang> 5 => vertex                                              // morph 5 into a vertex
==>vertex:('id'->5)

okram

okram

  lazy val cType:Parser[Obj] = (anonType | boolType | realType | intType | strType | instType | (not(inst) ~> (lstType | recType)) | tokenType) ~ opt(quantifier) ^^ (x => x._2.map(q => x._1.q(q)).getOrElse(x._1))

  lazy val dtype:Parser[Obj] = cType ~ rep[Inst[Obj, Obj]](inst) ^^ (x => x._2.foldLeft(x._1.asInstanceOf[Obj])((x, y) => y.exec(x))) | anonTypeSugar
 

 // the top definition of a type
 lazy val aType:Parser[Obj] = opt(cType <~ Tokens.:<=) ~ dtype ^^ {
    case Some(range) ~ domain => range <= domain
    case None ~ domain => domain
  }

okram

pg_2:('type' -> (                                                       
  graph  -> (graph<=edge{*}),                                           
  vertex -> (vertex<=('id'->int),                                       
             vertex<=int-<('id'->_)),                                   
  edge   -> (edge<=('outV'->vertex,'inV'->vertex),                      
             edge<=(vertex;vertex)-<('outV'->.0,'inV'->.1)))) <= mm    

okram

HoTT and Sweaty with mm-ADT
---------------------------
   http://mm-adt.org/vm

In homotopy type theory,

there is a space U,  (universal set)
a is a point in U,          (object)
b is a point in U.          (object)

okram

/* MODEL: digraph (extends numbers and mm)
digraph:(
'type' -> (
  vertex -> (vertex:('id'->nat,'attrs'->attr{*}),
             vertex<=nat-<('id'->nat),
             vertex<=(nat;attr)=(_)-<('id'->.0,'attrs'->.1),
             vertex<=int[is<0]-<([neg];('no';'data'))),
  attr   -> (attr:('key'->_,'value'->_),
             attr<=(str;_)-<('key'->.0,'value'->.1)),
  edge   -> (edge:(outV->vertex,inV->vertex))