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).
  • 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 }
  • 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.
• 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).

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
  • 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 [])
  • 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

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)