Branded Types

These two examples use the logical relation of Heaplang to define arrays and vectors. Arrays are fixed-size and provide safe and unsafe functions to access their elements. Vectors can grow in size and use the unsafe array methods to access their elements. Safety is ensured by branding vectors, meaning each vector is tagged with a fresh type variable. Statically, this has a similar effect as existential types. Semantically, the type variable is used to encode an ADT, i.e. impose invariants on the vector.