💾 Archived View for oortcloud.flounder.online › junk › 1finmaps.gmi captured on 2024-02-05 at 09:22:58. Gemini links have been rewritten to link to archived content
-=-=-=-=-=-=-
finite maps are sets of rows and hence have a partial order
m <= n := m.x ~ n.x
finite map (as data) lookup is the same as finite map (as fun) application
m x := m.x NB. (m`) == (m.)
{Nuts} <= (m && n) <= m <= (m || n) <= {Null}
application is not only continuous, but determined by atoms; in particular this implies that keys should be elements (and that the elemental maps are the functions)
(m|n) x == m x | n x m (x|y) == m x | m y x ~ y ==> m x ~ m y NB. fun by def m ~ n ==> m x ~ n x (m&n) x == m x & n x m (x&y) ~ m x & m y
use (%*) to give sequences of keys a map action, chaining lookup
m %* (k, l) := (m %* k) %* l
m %* k := m.k
m %* Nil := m
(&&) and (||) behave as one would expect
m && m == m
m && n == n && m
m && (n && o) == (m && n) && o
{Null} && m == m
m && {Nuts} == {Nuts}
m || m == m
m || n == n || m
m || (n || o) == (m || n) || o
{Nuts} || m == m
m || {Null} == {Null}
(!!) is like (&&), but also operates on bare rows, packing them as singletons.
m !! k:v := m && {k:v}
{d} !! {k:v | j:w} <=> {d} !! (k:v) !! (j:w) NB. Action
{Nuts} !! {d} <=> {d}
{d} !! {Null} <=> {Null}
(::) combines symmetrically, with priority by specificity
a::a <=> a
a::b <=> b::a
a::(b::c) <=> (a::b)::c
{Null}::a <=> a
NB. no zero
{k: v} :: {k: w | j: u} <=> {k: v | j: u} <=> {k: w | j: u} :: {k: v}
{k: v} :: {Nuts} <=> {k: v} NB. ({k: v} :: {Null}) == bare {k:v}
(//) combines asymmetrically, with priority to the left
{k: v} // {k: w | j: u}Â <=> {k: v | j: u}
{k: w | j: u} // {k: v} <=> {k: w | j: u}
a//a <=> a
a//{Null} == bare a NB. a//Nuts == Nuts
{Null}//a == {Null}
{Nuts}//a == a
a//{Nuts} == a
a//(b//c) == (a//b)//c
these operations are also available at (*) == (&&), (%) == (||), and (/) == (//)
OPEN: at least (//) needs to distribute over sequencing (for (<-) to behave properly in def'ns); are there reasons for or against the other synthetic ops doing so?
Yet another (commutative) action with map intersection
m && {k: v | j: w} == (m && {k: v}) && {j: w}
xor: {(True,True): False | (False,False): False
|(True,False): True | (False,True): True}