❮❮❮
Bonsai
❮❮❮
❯❯❯
Using Gurobi operators from F#
❯❯❯

Algebraic_datastructures

Thoughts about algebraic datastructures.

Reading time: 2 min.

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`[]`

.

- the type

# 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.

- Indices are from
- 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.

- Access is via pattern matching or special

## 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.

- Access is via pattern matching. The DU tag is from

## 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.