(* Idea 1 *)

There is no difference to the user whether a table has duplicate bindings 
for an entry. The most recent binding always shadows earlier bindings, and 
earlier bindings are not accessible. Therefore, using this argument, 
extendTable can be seen as not having multiple bindings and allows 
updating.

Alternatively, fooTable can be used to remove a specific binding from a 
table before adding an updated binding.

(* Idea 2 *)

Table = Nat -> Ref [OptionalNat]

emptyTable = lambda n:Nat. ref (<none = unit> as OptionalNat)

extendTable = lambda t:Table. lambda m:Nat. lambda v:Nat.
  case !t(m) of
    <none = _> => (lambda r:Ref [OptionalNat]. lambda n:Nat.
		     if (equal m n) then r else t(n))
                  (ref (<some = v> as OptionalNat))
  | <some = _> => (t(m) := <some = v> as OptionalNat; t)

(* Question: what happens if t(m) returns some reference to <none = unit> 
 * and you assign t(m) := <some = v> ?
 *)

(* Idea 3 *)

Table = List [Nat * Nat]

emptyTable = nil[Nat * Nat]

(* lookupTable: Table -> Nat -> OptionalNat *)

lookupTable = lambda t:Table. lambda m:Nat.
  case t of
    nil[Nat * Nat] => <none = unit> as OptionalNat
  | cons[Nat * Nat] (n, v) tail =>
    if (equal m n) then <some = v> as OptionalNat
    else lookupTable tail m

(* extendTable: Table -> Nat -> Nat -> Table *)

extendTable = lambda t:Table. lambda m:Nat. lambda v:Nat.
  case t of
    nil[Nat * Nat] => cons[Nat * Nat] (m, v) (nil[Nat * Nat])
  | cons[Nat * Nat] (n, _) tail =>
    if (equal m n) then cons[Nat * Nat] (n, v) tail
    else extendTable tail m v