maps

algebra of maps

Maps can be used as partial functions from key terms to value terms. Maps have their domain (i.e. a set of keys) and image (i.e. a set of values).

Maps are more complex than just partial functions, though: they can have linear/ownership semantics. Maps are objects + (linear?) lenses over their structure:

Maps are monoids: they have the neutral element {} and can be concatenated, producing a map (~ for concatenation? But, e.g. HOCON uses juxtaposition for monoidal concatenation):

Inspirations:

operations over values

Given an existing map, do something to its values without changing its set of keys ("structure").

// exactly one value cell:
m.a.b

// a prism to get zero or one cell:
m{.a.b}

// a prism to a reference to zero or one cell:
ref m{.a.b}

// a traversal to exactly two cells,
// (`val` uses an implicitly given allocator to make a copy):
#example
val {a=1, b=2, c=3}.(a, b) = {a=1, b=2}

#example
{a=1, c=3}.(a, b) = ERROR "b=?"  // static or dynamic error

// a prism to three values or less:
#example
{a=1, b=2, c=3}{.a, .b, .d} = {a=1, b=2}

// setting a value:
at m.a.b \set 42
// at <cell> <op> <args>...

// popping a value from a map:
//   a linear(?) lens that consumes and splits a map
v = at m \split k

operations over structure

  • projecting into a submap (also: by key)
  • replacing a submap (also: by key)
  • removing a submap (also: by key)

Constructing maps:

// an empty map
{}

// adding a pair to a map:
a' = a ~ {k: v}

// merging two maps:
m = m1 ~ m2

#example
{a=1, b=2} ~ {b=3, c=5} = {a=1, b=3, c=5}
// the last key wins

Monoidal concatenation of maps is abstract, it does not necessarily create a new flat map. It can be a kind of ECMAScript-like prototype chaining with a [[proto]] slot.

Additional operations:

#example
{a=1, b=2} \split .a = {b=2}

THINK: addressing keys vs addressing values, e.g.

// an iterator over all values < 2:
#example
{a=1, b=2, c=3}[v => v < 2] = ???

{1=a, b=2, c=3}.[k => ]

abstract value and self

(?) Every value v is equivalent to notation { v }, which is a shortcut for a pair of { self = v }. self is a special key which refers to the "default" value of the map. When a map is used as a value, it dereferences to its last self key.

TODO: it or self?

TODO: what is a map without self? something that cannot be constructed at runtime without a container?. If the maps does not have self, it cannot be used as a single value?

Properties:

  • ${\tt v} \equiv {\tt { v}} \equiv {\tt {{v}}} \equiv ...$
  • ${\tt v} \equiv {\tt v.self} \equiv {\tt v.self.self} \equiv ...$

self really looks like an identity lens.

TODO: think if this is in any way consistent.

THINK: can partiality be seen as {} instead of a value? {} becomes nil, it is smelly.

runtime reification

The notation {...} is an abstract comptime map. It can be used as a blueprint for a runtime value:

// given a runtime container type `HashMap`,
//   construct a HashMap from an abstract map:
m = HashMap { one = 1, two = 2, three = 3}

// Q: is this { self = HashMap, ... } ?

Q: empty runtime maps? HashMap {} is valid?

HOAS

Wiki: higher-order abstract syntax

When we have maps, we can have nested maps (where #<metainfo> <item>):

#outer {
  x = 1
  // #inner is not bound, it's the default value of #outer
  #inner {
    // Q: how this automatic chaining happens? Implicit `self = outer`?
    // here x is 1
    x = 2
    // here x is 2
    #last {
      x
      // currently bound x becomes the default value
      //   of both inner and outer map
    }
  }
  // here x is 1, but no one is able to see this
}

Nesting maps can be seen a sequencing mechanism. The inner map without a key can be seen as a temporary scope inside of it, chained to / inheriting the outer map. Lookups of symbol can use the current chain.

TODO: non-shadowable definitions, #const ?

scopes

The vanilla map notation is very awkward for this, though. Scopes are notations for sequences of nested pairs, each inheriting scope of its parent pair.

This scope corresponds to the example map above:

do
  x = 1       // the body of #outer
  // the value of #outer:
  x = 2       // the body of #inner
  // the value of #inner:
  x           // #last
end   // "evaluates" to 2

Scopes can branch: they can inherit the outer scope, but end up as a separate, non-default value:

do
  one = 1
  three = do two = 1; one + two; end
  three
end

<=>

_ ~  // outer context
{ one = 1 } ~
{ three = self ~ { two = 2 } ~ { one + two } } ~
{ three }

Multiple sequential default values:

do 1; 2; end

<=>

_ ~   // outer scope
{ /* self = */ 1 } ~
{
  // the last `self` binding wins due to monoidal concatenation:
  /* self = */ { /* self = */ 2 }
}

encapsulation

E.g. you have a helper or a value you don't want to expose:

(range: Nat) => (Rand) do
  num = randInt range  // unexported
  #export {
    guess = (n) => n == num
    range = range
  }
end

Importing multiple other things from other scope:

// sometimes you want to bring another scope in:
math = @include("math.iota")
at self ~ math.{
  ln, log2, sqrt
}

// or just import everything from another scope:
at self ~ @include("math.iota")

do-notation

aka "programmable scope".

Examples to think of:

// Implicit Identity monad:
do
  one = 1
  three = do two = 2; one + two; end
  three
end

// <=> [by monad expansion]
(ctx: Id _) =>
  Id.lift 1 \Id.bind one =>
    Id.lift (
        Id.lift 2 \Id.bind two =>
          Id.pure (one + two)
    ) \Id.bind three => Id.pure
      three

//   Id.pure : a -> Id a
//   Id.bind : Id a -> (a -> Id b) -> Id b
//   Id.lift : {Has Id m} -> Id a -> m a
// <=> (by definitons of Id.lift)

// (self : Id _) => { ...
(_: Id _) =>
  1 \Id.bind one =>
    (self \Id.bind
      (_: Id _) => {two = 2} ~ Id.pure { one + two }
    ) \Id.bind three =>
      Id.pure three

// <=> [ by def. of `Id.bind` ]
(_: Id _) =>
  { one = 1 } ~
  { three = self ~ {two = 2} ~ {self = one + two} } ~
  { three }

// <=> [no values from `Id` anymore]
{ one = 1 } ~
{ three = {two = 2} ~ { one + two }} ~
{ three }

// <=> [scope reduction]
{ {two = 2} ~ { 1 + two } }

// <=> [scope reduction]
{ 1 + 2 }

// State monad:
St = State
(St) do
  x = get ()
  x = x + 1
  put x
  x
end

// <=> [monad expansion]
(st : St _) =>
  // lift is closed over the runtime `st`:
  // St.bind does not, it goes straight to the type
  // TODO: think about comptime/runtime binding more.
  st.lift get () \St.bind x =>
    st.lift add x 1 \St.bind x =>
      st.lift put x \St.bind _ =>
        st.lift x \St.bind id

// <=> [expand `st.lift` to `St.lift st`]
(st : St _) =>
  St.lift st get () \St.bind x =>
    St.lift st (add x 1) \St.bind x =>
      St.lift st put x \St.bind _ =>
        St.lift st x \St.bind id

// <=> [State.mk, State.get, State.put]
State.mk (st: _ : Add) =>
  (st, st) \St.bind (x, st) =>
    (add x 1, st) \St.bind (x, st) =>
      ((), x) \St.bind (_, st) =>
        (x, st)

// <=> [State.bind]
State.mk st =>
  {(x, st) = (st, st)} ~
  {(x, st) = (add x 1, st)} ~
  {(_, st) = ((), x)} ~
  (x, st)

// <=>
State.mk st => {x = st} ~ {x = add x 1} ~ {st = x} ~ (x, st)
// <=>
State.mk st => { x = add st 1 } ~ (x, x)

// IO:
(IO) do
  x = read \ getLine ()
  putStr "the number is "
  print x
end

// <=> [monad expansion]
(io: IO) =>
  IO.lift io.getLine () \IO.bind $0 =>
    IO.lift read $0 \IO.bind x =>
      IO.lift io.putStr "the number is " \bind _ =>
        IO.lift (io.print x)

// <=>
// TODO

// An effect bag, (State, IO):
(State | IO) do
  x = get ()
  x = x + 1
  put x
  print x
end

// TODO

misc

  • interplay with XML attributes/children distinction?