okram

On the Encoding of Type Equivalences within the mm-ADT Type Graph

In category theory, if C and D are both categories, then a functor from C to D maps every morphism in C to some morphism in D. You can think of a functor as a set of "morphism-to-morphism"-morphisms. Furthermore, if the functor maps from category C to category C (i.e., D=C), this is called an endofunctor.

In mm-ADT, in the type subgraph of the obj graph, the vertices denote types and a path (of edges) back to the root of the graph (a ctype root) denotes a type definition. These edges are labeled with instructions from inst, where a path is a sequence of operations that morph one type into another type (see The Type). In abstract algebra, the type subgraph is called a (generalized) Cayley graph as the obj graph captures the structure of the underlying inst monoid. N

okram

/*** 
An mm-ADT type has a signature and a definition.
  range<=domain[inst]
   \_________/  \__/
    signature  definition   
***/


// An mm-ADT type definition is always with respects to the type of objects that can be mapped.
// In the definition below, an int can be mapped to a nat by way of a predicate membership function.

okram

~/software/mmadt/vm/jvm$ bin/mmadt.sh
                                _____ _______
                           /\  |  __ |__   __|
 _ __ ___  _ __ ___ _____ /  \ | |  | | | |
| '_ ` _ \| '_ ` _ |_____/ /\ \| |  | | | |
| | | | | | | | | | |   / ____ \ |__| | | |
|_| |_| |_|_| |_| |_|  /_/    \_\____/  |_|
                                 mm-adt.org

//////////////////

okram

Welcome to mm-ADT™.

All mm-ADT contributors must sign the Contributor License Agreement. A signed agreement applies to all mm-ADT repositories indexed at the mm-ADT GitHub Organization. A review of the license is provided below and can be e-signed here.

---

Thank you for your interest in mm-ADT by RReduX, Inc. (the “Company”). In order to clarify the intellectual property license granted with Contributions from any person or entity, the Company must have a Contributor License Agreement (“CLA”) on file that has been signed by each Contributor, indicating agreement to the license terms below. This license is for your protection as a Contributor as well as the protection of the Company and its users; it does not change your rights to use your own Contributions

okram

~/software/mmadt/vm/jvm$ bin/mmadt.sh
                                _____ _______
                           /\  |  __ |__   __|
 _ __ ___  _ __ ___ _____ /  \ | |  | | | |
| '_ ` _ \| '_ ` _ |_____/ /\ \| |  | | | |
| | | | | | | | | | |   / ____ \ |__| | | |
|_| |_| |_|_| |_| |_|  /_/    \_\____/  |_|
                                 mm-adt.org
mmlang> 1+4
==>5

okram

           mm-ADT [http://mm-adt.org]

This is a demo of the [trace] instruction which exposes
the core data structure of the mm-ADT VM (obj trace graph).
Unfortunately, it will be difficult to understand without knowing how polys and types work in mm-ADT.
However, for those competent with Gremlin/TinkerPop (TP3), 
             the examples below are like path().by(), but for both types and values.
///////////////////////////////////////////////////////////////////////////////////////////////////////

mmlang> int[plus,2][mult,3]                                                         // standard type

okram

mmlang> int{3}~<[+2|[is>4]-<[_|_]>-+4]>-[gt,[plus,2]][id][explain]
==>
bool{3,9}<=int{3}~<[int{3}[plus,2]|int{0,6}<=int{3}[is,bool{3}<=int{3}[gt,4]]-<[int{0,3}|int{0,3}]>-[plus,4]]>-[gt,int{3,9}[plus,2]][id]

instruction                                    domain                                              range                                         state
-------------------------------------------------------------------------------------------------------------------------------------------------------
~<[int{3}[plus,2]|int{0,6}<=int{3}[is,bo...    int{3}                                         =>   [int{3}[plus,2]|int{0,6}<=int{3}[is,bool...
 [plus,2]                                       int{3}                                        =>    int{3}
 [is,bool{3}<=int{3}[gt,4]]                     int{3}                                        =>    int{0,3}
  [gt,4]                                         int{3}                                       =>     bool{3}

okram

/*******************************************
   A stream of polys or a poly of streams.
        mm-ADT's match/case story
*********************************************/

// There is one fundamental composite structure in mm-ADT: poly.
// Polys are used to create data structures (e.g. lists, maps, trees, graphs, etc.)
// Polys are used for branch-based data flow.

// -< (split)

okram

mmlang> 1
==>1
mmlang> 1-<[+2|+3|+4]
==>[3|4|5]
mmlang> 1-<[+2|+3|+4]=[_|>6|10]
==>[3|false|10]
mmlang> 1-<[+2|+3|+4]=[_|>6|10]=[_|_]
==>[3|false]
mmlang> 1-<[+2|+3|+4]=[_|>6|10]=[_|_]=[-<[+1|+2]|_]
==>[[4|5]|false]

okram

trait MultOp[O <: Obj] {
  this: O =>
  def mult(anon: __): this.type = MultOp(anon).exec(this)
  def mult(arg: O): this.type = MultOp(arg).exec(this)
  final def *(anon: __): this.type = this.mult(anon)
  final def *(arg: O): this.type = this.mult(arg)
}

object MultOp {
  def apply[O <: Obj](obj: Obj): MultInst[O] = new MultInst[O](obj)