Miking Collections

Notes by Viktor P from initial meeting on 2023-03-14

Typed notes:

• Lars: immutable container, static guarantees on dimensions (n-dimensional matrices), but not necessarily on all dimensions
• Sparsity of data (sparse matrices, graphs that aren't dense)
• Viktor: sequences are not optimal (they incur extra boxing, dynamic choice of implementation), and require more effort for implementing backends
• Oscar: mutable array that can be shared with ffi (C?), might not need polymorphism
• John: ndarrays, dimensions in the type system, probably doable without arithmetic on type-level, but not entirely certain
• Safe head on sequences and the like
• David: extensible (in operations) without extending the core language
• Try to have a small number of core types
• Needs to have a reasonable UX both for writing code in it, and generating code using it
  • Difficulty of producing potentially required annotations, good errors even in the face of inference

NColl (7, 8, 1) Int
NColl (7, Dyn, 1) Int

concat : NColl (a, b) x -> NColl (c, b) x -> NColl (a + c, b) x
concat : all r a b. NColl {r with 0 = a} x -> NColl {r with 0 = b} x -> NColl {r with 0 = a + b} x

(a, b, ....) -> (a, b, ..., 1)

concat : NColl (5) x -> NColl (c, b) x -> NColl (a + c, b) x
concat : NColl (Dyn) x -> NColl (c, b) x -> NColl (a + c, b) x

[[Int; 100]; 100]

[Int; 100, 100, 100, *]

foo : all a. [a] -> ...

let f : all a : Int. all b : Int. all c: Int. NColl (a, b) Int -> NColl (b, c) Int -> NColl (a, c) Int =
 lam a : NColl .... ...
 let x : NColl (a, b) Int = a +