Extensible Tables

[tiansivive]

Combine Lua's concept of tables with row polymorphism.

Tables allows for any type to be used as the indexing key. We can generalise this idea by extending the simple key-val pair to any n sized tuple. Any element of such a tuple can act as an index.
This is mimic Prolog's facts/relations

We can leverage row polymorphism for extensibility. Rather than having a Row Type kind, we can instead have a Row Relation, where Relation is of kind Type -> Type -> Type.
This would allow multi-key records, hashmaps, lists and arrays to all be specializations of a Extensible Table.

String indexed record:

type Record 
 : Row (Relation String Type) -> Type
 = \r => { | r }

Array:

type Array 
 : Row (Relation Nat Type) -> Type
 = \r => { | r }

Multi-key, 2d Matrix

type Matrix 
 : Row (Relation (Int, Int) Type) -> Type
 = \r => { | r }

Question:

• What about non indexed types like Relation Unit Type? Is that just a Tuple?
• What about only keyed types like Relation Nat Unit? Is that an error? Or do we default to integer index, as in, a sequential array?

---

Syntactic sugar

Based off Typescript:

String indexed table:

type Foo = { [String]: Bar }

desugar to

type Foo 
  : Row (Relation String Bar) -> Type
  = \r => { | r }

Note

The following would not work:

let table
  : { [String]: Int }
  = { foo: 1, bar: 2 }

Because the desugared type var r is rigid, and cannot be unified by any specific term.
This might cause confusion, so perhaps we need another syntax or some mechanism to allow such "generic" types.
For example, would it be possible to allow:

type Foo = \r => { [String]: Int | r}

???

[tiansivive]

Interestingly,

type Foo = { [0,0]: String, [0,1]: Int }

Would mean a term can only ever have [0,0] and [0,1] as indexes. Whereas:

type Foo = { [Int, Int]: String, [0,1]: Int }

would mean any indexes of the form [Int, Int], albeit [0,1] would be "overriden" to Int.

Perhaps a better way of defining such types is allowing:

type Foo = { [0,1]: Int | [Int, Int]: String }

Here we get rid of the rigid type variable r, therefore n-sized [Int, Int] indexed tables.
We can always add a r by

type Foo = \r => { [0,1]: Int | ([Int, Int]: String |  r)}

which we could allow as:

type Foo = \r => { [0,1]: Int | [Int, Int]: String | r}