types-seem-vectorish.groovy

// Types in Tensors             
// Types as "inclusion-predicates" or subspaces in {}-quantifier tensors                       // SIDENOTE: We need to be more strict on the quantifier ring -- ordered,ring,unity. max and min make life easier).


// mm-ADT instruction (mmlang 'assembly')
int{0,5} <= [start,int{5}][plus,5][mult,5][is,bool{5} <= [start,bool{5}][gt,5]][plus,100][is,bool{0,5} <= [start,int{0,5}][mult,45][minus,10][gt,0]]

// the above in "block form"-syntax
if(((int{5} + 5) * 5) > 5) {
  bool{5} + 100
  if(((int{0,5} * 45) - 10) > 0) {
	  // this is a stream in int{0,5}   (type inference as a consequence of the +/*-operators in the function and quantifier rings)		
  }
}

int{0,5} <= [start,int{5}][plus,5][mult,5]
            [is,bool{5} <= [start,bool{5}][gt,5]][plus,100]
            [is,bool{0,5} <= [start,int{0,5}][mult,45][minus,10][gt,0]]

// BELOW IS HAND CRAFTED NOTATION THAT ISOLATES A STRUCTURE IN THE INSTRUCTION ABOVE FOR THE DISCUSSION TO FOLLOW.
           // initial           
	      obj{0} * int{5} -> int{5}    
			         int{5} * bool{5} -> int{0,5}
			                             int{0,5} * bool{0,5} -> int{0,5}                      /// wild hit me thought: <= and -> are duals in some way

// Everything right of <= is operational semantics in "morphism space."          /// function ring of SRT     (instructions in mm-ADT)     
// Everything left of  <= is type semantics in "object space"                    /// coefficient ring of SRT   (quantifiers in mm-ADT)
//    Above is the instruction 'type' signature of the instruction sequence. X -> Y.                           
//    In mm-ADT instruction domain/range objs constructed at moment of 'compose'.  



/* Space Notes         */
/* Stardate 11.13.2019 */
/*

Quantifiers define a tensor-space. 
mm-ADT currently only supports 0D, 1D and 2D ("quantified" by the carrier set of the ring).
  0D being possible because of degenerate/trivial 1-ring.
  1D being {x}     // not a type system (there is no index from a higher-dimension 'anchor point' (1-to-*))
  2D being {x,y}   // this is the emergence of the type system. 
  
  The token "{,y}" denotes the union of the {1,y},{2,y},{3,y}...{inft,y} tokens.
  x are the instances/elements.
  y is the type/set.
  
  ---- modern type systems are N^2-systems (defined by a 2D int-ring).
  
  [the ring algebra of the {,y}-"column" carrier set has one extra token "{,y}", thus |{,y}| + 1 = size of type+instances.]
  [int + 4 has a meaning with ring operators the same as 2 + 4.]
  [...what about...]
  [int + bool ...that requires a functor. the functor's instruction definition is the path equation to the right of <=]
  	--- [branch,[a,int],[a,bool]]
  
  ////////////////////////////////////////////////////////////////////////
  [I believe that I may be able to "*" across types algebraically without looking at their "instruction mappings."]
  ... The Magical |  (or)
               (I hypothesize there is a ring algebra closed over 2D containing 1D closed subrings.)       /// that is "*" yields mm-ADT's intra-type algebra (cross column algebras)
  ////////////////////////////////////////////////////////////////////////
  .....................................................................................................................
  
  ...this concept goes off the rails when you realize that (physical) quantum computing
  ...       (single qubit as far as I have shown.)                                       /// I don't understand entanglement and the wave function as a 2 "partcle system.")
  ...is in {complex,complex}. C^{2} for 1D-line quantum traversals/streaming.
  ...is in {complex,complex,complex,complex} for C^{4} for 2D-planar quantum traverals/streaming.
  ...
  ...When you go into C^{8} 4D-tensor, you get a "quamtum type system." with an algebra that works "downward" across all lower dimensional tokens.
  
Types as N-1 vectors in N tensor spaces.

*/

mmadt> obj{0} <= [start,int{5}][plus,5][mult,5][is,[gt,5]][plus,100][is,[mult,45][minus,10][gt,0]]
==>int{0,5} <= [start,int{5}][plus,5][mult,5][is,bool{5} <= [start,int{5}][gt,5]][plus,100][is,bool{0,5} <= [start,int{0,5}][mult,45][minus,10][gt,0]]