❮❮❮
Bonsai FS
❮❮❮
❯❯❯
Algebraic_datastructures
❯❯❯

Bonsai

Thoughts about a tree serialisation library.

Reading time: 5 min.

These are some thoughts about the design of a functional library to serialize partially abstract finite tree-shaped data.

# Type context

- Types:
- We have
**primitive atomic types**:`int`

,`string`

,`bool`

,`unit`

and some others. - We have
**primitive composite types**:- arrays via
`Array a`

and written as`[v_1, ..., v_n]`

- tuples via
`*`

and`Tuple [a_1, ..., a_n]`

and written as`(v_1, ..., v_n)`

.

- arrays via
- We have
**primitive algebraic types**:- Variants (non-recursive) via
`| l_1 of t_1 | ... | l_n of t_n`

.- No recursive definitions allowed.

- Records via
`{ l_1 : t_1, ..., l_n : t_n }`

- Variants (non-recursive) via
**Abstract types**with a mapping to a representation as other types.**Type parameters**are universally quantified and written in applicative syntax, i.e.`Map (key, value)`

.- Only a single argument and fully applied, several type parameters grouped with array or tuple syntax.

- We have
- Type universes.
- All closed types from a set of type constructors.
- Closed: no free type parameters.

- Universe
`Prim`

: all primitive atomic types. - Universe
`Alg`

: all primitive types. - Universe
`App`

: all primitive and abstract types (with possible type parameters).

- All closed types from a set of type constructors.

# Representation of representation mappings (RoRM)

- There is a
`Map (App, App)`

containing the representation mappings.- A type with a type parameter can only be contained in the generic form as a key.

- Core operations are:
- addition, merging

# Type representation

- Go from
`T : App`

to universe`Alg`

. - Helper datatypes:

```
type Label = string
type Shape prim =
| Prim of prim
| Tuple of Array (Shape prim)
| Array of (Shape prim)
| Variant of Map (Label, Shape prim)
| Record of Map (Label, Shape prim)
type PrimType =
| PT_Unit
| PT_Int
| PT_Bool
| ...
type YetUnresolved =
| Prim of PrimType
| Unknown of App // If an abstract type is not in the RoRM.
| Recursion of App // If an abstract type is encountered twice along the same branch of the shape tree.
type Stepwise =
| Prim of PrimType
| Unknown of App
| Recursion of App
| NextStep of App * (Set App) // Type to respresent/expand next and the set of abstract types encoured along the branch to here.
```

- The core functions are:
`resolveNextStep : Map (App, App) -> Shape Stepwise -> Shape Stepwise`

- Given a RoRM, expands all NextStep cases in Stepwise once
- Abstract types by their representation in the RoRM
- updates set of abstract types in NextSteps

- Primitive algebraic and compositive types by their rep in Shape
- Primitive atomic types by the primitive case in Stepwise.Prim

- Abstract types by their representation in the RoRM

- Given a RoRM, expands all NextStep cases in Stepwise once
`searchPrimitiveRepresentation : Map (App, App) -> (T : App) -> Shape YetUnresolved`

- Given a RoRM, try to find its shape by following the representations.
- Could use
`resolveNextStep`

, but is maybe better coded recursively

`expansionSteps : Map (App, App) -> (T : App) -> List (Shape Stepwise)`

- give the history of
`searchPrimitiveRepresentation`

- start value for
`representAbstractOnce`

is`NextStep (T, Set [])`

- give the history of
`isAlgebraic: Shape YetUnresolved -> Result (Shape PrimType, { Unknowns : Set App, Recursive : Set App })`

- Collapse the search result
- Error case: sets of unknown and recursive types

`isSubtype: Shape PrimType * Shape PrimType -> bool`

- subtyping relationship on fully resolved shapes

## Example

Given the setup

```
type PrimType =
| PT_Unit
| PT_Int
| PT_Bool
let RoRM : Map (App, App) =
{
Map ('a, 'b) -> Array ('a * 'b)
Abs1 -> int * (Abs2 bool)
Abs2 'a -> bool * 'a
}
let steps = expansionSteps RoRM
```

The derivations are

```
steps unit = [
NextStep (unit, Set []),
Prim PT_Unit,
]
steps (array int) = [
NextStep (array int, Set []),
Array (NextStep int, Set []),
Array (Prim PT_Int)
]
steps { A : bool, b : int * bool } = [
NextStep ({ A : bool, b : int * bool }, Set []),
Record { "A" -> (NextStep bool, Set []), "B" -> (NextStep (int * bool), Set [])},
Record { "A" -> Prim PT_Bool, "B" -> Tuple [NextStep (int, Set []), NextStep (bool, Set [])]},
Record { "A" -> Prim PT_Bool, "B" -> Tuple [Prim PT_Int, Prim PT_Bool]},
]
steps Abs1 = [
NextStep (Abs1, Set []),
NextStep (int * Abs2 bool, Set [Abs1]),
Tuple [NextStep (int, Set [Abs1]), NextStep (Abs2 bool, Set [Abs1])],
Tuple [Prim PT_Int, NextStep (bool * bool, Set [Abs1, Abs2])],
Tuple [Prim PT_Int, Tuple [NextStep (bool, Set [Abs1, Abs2]), NextStep (bool, Set [Abs1, Abs2])]],
Tuple [Prim PT_Int, Tuple [Prim PT_Bool, Prim PT_Bool]],
] // int * (bool * bool)
```

# Value representation

- Value rep

```
type PrimVal =
| PV_Unit
| PV_Int of int
| PV_Bool of bool
| ...
type RepValue =
| Prim of prim
| Tuple of Array RepValue
| Array of Array RepValue
| Variant of Label * RepValue
| Record of Map (Label, RepValue)
```

- the core functions are:
`fitsType : Shape PrimType -> RepValue -> bool`

`represent : (T : App) -> RepValue`

`construct : App -> RepValue -> (T : App)`

- the first argument is a type to guide the construction, if the result type
`T`

is not inferrable

- the first argument is a type to guide the construction, if the result type

## Gotcha

```
let crazy : RepValue = Array [PV_Unit, PV_Int 2, PV_Int 2]
// not possible as represent t
```

```
let t : Array int = [1, 2, 3, 4]
let r : RepValue = Array [PV_Int 1, PV_Int 2, PV_Int 3, PV_Int 4]
```

```
let t : Array (int * bool) = [(1, true), (2, false), (3, true)]
let r : RepValue = Array [Tuple [PV_Int 1, PV_Bool true], Tuple [PV_Int 2, PV_Bool false], Tuple [PV_Int 3, PV_Bool true]]
```

# Recursive types

- Much more complicated.
- Could apply to variants and abstract types.
- Would introduced cycles in
`Shape`

, i.e. this would become a rooted forest. - Termination not really checkable on type level only, as value mappings need to be monotonic.
- This is classic for mutually recursive variants.

- Classic example: functional lists.

```
type rec List a =
| Nil
| Cons of a, * (List a)
```