Introduction

DependoBuf is a novel structured data serialization format that incorporates dependent types into the data model. It is designed to be a more expressive and safe alternative by providing the ability to describe not only the structure of the data, but the relationships between the data as well and enforcing those relationships at both compile and runtime.

Protocol BuffersDependoBuf

message TreeH {
    message TreeHLeaf {
        int32 value = 1;
        uint32 height = 2;
    }

    message TreeHNode {
        int32 value = 1;
        uint32 height = 2;
        TreeH left = 3;
        TreeH right = 4;
    }

    oneof treeh_type {
        TreeHLeaf leaf = 1;
        TreeHNode node = 2;
    }
}

Constraints not obvious

No way to define constraints in schema

No way to validate constraints soundness

Need to write custom code to validate constraints

enum TreeH (height Unsigned) {
    0 => {
        TreeHLeaf {
            value Int
        }
    }
    * => {
        TreeHNode {
            value Int
            left TreeH (height - 1)
            right TreeH (height - 1)
        }
    }
}

Obvious constraints

Constraint definition in schema

Soundness validation at compile time

Automatic validation of constraints at runtime

This documentation is meant to be a reference for the language and its features. This documentation is not meant to be an explanation of the internal workings of the compiler or the runtime. They are both works in progress, but you can find the source code project's GitHub.

Warning

This is a work in progress. The language and its features are subject to change. If you have any suggestions or feedback, please open an issue on GitHub.