Okay. Here is a very pretty idea that could serve as a foundational concept to mm-ADT.
There are only 2 types of mappings in mm-ADT:
<= obj "objects -- sets "
<- inst "morphisms -- functions "
Every object can have 0 or more of these guys dangling off them with the following semantics and syntax.
person[name:x] <=[=mongo][get,'users'][is,[get,'name'][eq,x]]
<-[-mongo] * [order] <- [id] |
[dedup,'name'] <- [id] |
[is,[get,id][eq,x]] <=[=mongo][eval,'idx-lookup',id,x]
<-[-group] * [zero] <= [map,person['alive':false]] |
([plus,0] | [mult,1]) <- [id] |
([minus,[neg]] | [div,[inv]]) <- [id]
[=mongo]: this is an object morphism that denotes a "person" encoded in JSON (the mongo model-AST).[-mongo]: this is an instruction morphism that serves as a rewriter to theorems in mongo's secondary structures (indices, sort orders, ..).[-group]: this would be in a 'standard library' of arrow morphisms based on group theorems. this constrains the object read/write rules to the group axioms and entailments.
That is all you can do in mm-ADT. Define object and arrow morphisms between models.
The <-[-group] notation says a [plus,0] instruction on a person is an identity. It also says that we are computing with instructions (--substructure of lst). That is, instructions are flowing through the stream.
mmadt> [start,2,3] <= [get,1]
==>2
mmadt> [start,2,3] <= [get,0]
==>'start'
Note that there is nothing weird about the syntax. Why?
[a] * [b] == [a][b]
[a] | [b] == [choose,[a],[b]]
[a] + [b] == [branch,[a],[b]]
[a] & [b] == [a][b]
[a] / [b] == [error] // ints is a ring w/ unity (with sub-rings within -- commutativity on filters, monoidic on reduction, ...)
Objects and arrows are all you need to reason on.
Think of it as being in a "world" (domain of discourse) and you realize that you are coupled in some functorial way to another world. Not necessarily an isomorphism ("pure merge")...But then you realize, its a freakin' multi-verse of coupled "algebraic environments" (various 'laws of physics' converging). And these coupled worlds (at all scopes of abstraction) exist ipso facto of being free energy machines because they just dereference pointers of their form within other structures...ad infinitum. never pinpointable --- deref, deref, deref. That is how the universe is powered (says Lord Rodström). mm-ADT's "funtorial" instructions [=xxx] [-yyy] capture this conceptualization.
I cost nothing because I'm represented everywhere. Information does not go to waste and, I reckon, pointer chasing is "free." (the 'ol carrot on a stick...we have all the time in the world)
Marko.
Aww yeah, there's those functors between algebraic varieties