However, it is based on a theory of algebraic data types and aims to be a more natural fit for users of proof assistants and purely functional, strongly typed programming languages.
Background and motivation
Once we find a suitable way to express ADTs, we futhermore want to:
- Serialize and deserialize types into bytes,
- Serialize and deserialize typed terms into bytes,
- Interpret definitions (as types) in various programming languages,
- Compute new type definitions from existing ones.
We need to do all of this safely both at compile time and at runtime.
Safe runtime type manipulation
To write code that safely deals with type definitions that are not known at compile time one needs a language with dependent types, so our system is implemented in the Idris programming language. The code comes with various correctness proofs checked by the Idris compiler and allows to programmatically manipulate types and interpret them safely as
Type at runtime, very cool.
Specifying type definitions
To input type definitions, you can use Idris directly, but this is not needed: you can instead use our S-expression (LISP syntax) based frontend.
See the last part of the introduction.
Another way to work with type definitions is by generating code in a target language that describes the types and can serialize and deserialize their terms.
Code generation can be seen in action in your browser, surf to try.typedefs.com.