Seamless, Correct, and Generic Programming over Serialised Data

<h1>Seamless, Correct, and Generic Programming over Serialised Data</h1>


<h2>Overview</h2>

- Introduction
- Data types
- Serialized representations
- Pointers and Buffers
- Serializing
- Results & Conclusion

<h2>Idris2</h2>

The code in this paper are written in Idris2.

- Dependent Types
- Totality

<h2>Dependent types</h2>

The type is influecents by the value. For example we can have the length of a list inside the type.  We can have functions that depend on types.

<h2>Induction tree</h2>
<img title="a title" alt="Alt text" src="plaatje.png">

In the Iris2, how does it store this tree? One idea: We have a value that describes the kind of the constructor, values and pointers to pointer to another constructor. We want to end up having a solution that uses buffers, which is very fast.

<h2>Data types</h2>

- Descriptor: 
- Constructor: Give a name to a description
- Data: List of constructors, such that we can build a tree or list

<h2>Serialized representations</h2>

The format they have chosen is a hex file. The header describes the way the data is build up.

<h2>Pointers and Buffers</h2>

Given some fixed point over data we have location and a datatype.

The type family singleton represents all types that are described uniquely by their
variables.

Now we can a view function that takes a type an a pointer and returns what is stored in the location. The main constructor is the (#) to combine serialization processes.

<h2>Conclusion</h2>
In this language it is impossible to have faulty pointer arithmetic, because the datatype does not allow it.