Thoughts about algebraic datastructures, as found in ML style languages (SML, Ocaml, F#, Elm, Haskell, Scala, …).

Atomic types

• They are atomic and thus not interesting.
• Important later are
  • the type Nat of natural numbers (starting at 0).
  • the type Fin n, for n : Nat, which describes the values [1, ..., n]
    • Fin 0 has no values, i.e. describes the values in [].

Core composite types

Arrays

• Abstract: Array a is dollection of n : Nat elements of the same type a.
  • Indices are from Fin n and are 1-based.
• Concrete: Constant time access.
• Could be simulated by a hidden tree, but with different runtime cost.
• Hence assumed as builtin.

Tuples

• Abstract: Tuple [a_1, ..., a_n] has n : Nat many elements of fixed arbitrary types a_1, ..., a_n.
  • Access is via pattern matching or special Fin n accessors.
  • The one-tuple exists and boxes its content.
  • The empty tuple is its own type.

Finite DUs

• Abstract: FDU [a_1, ..., a_n] describes n : Nat many alternatives of fixed arbitrary types a_1, ..., a_n.
  • Access is via pattern matching. The DU tag is from Fin n.
  • The empty FDU [] is possible.

Duality

• There is a duality between Tuple [a_1, ..., a_n] and FDU [a_1, ..., a_n], as the share the same types and label set Fin n.

Core algebraic types

Label

• Let Label be an infinite set of distinct symbols used for labelling.

Records

General DUs

Duality

Recursive DUs