This project originally started as an offspring from the SAC project. Our notion of array programming is based on a formal calculus of multi-dimensional arrays as pioneered by APL. This calculus sets arrays into relationship regarding two fundamental structural properties: rank (the number of axes/dimensions) and shape (the vector of extents along each axis/dimension). Any array operation defines a relationship between ranks and shapes of argument arrays and result arrays. In interpreted array languages structural consistency is checked by every operation at runtime. In a compiled setting, however, we were keen to define even complex shapely relationships in a precise manner and statically prove structural correctness of array programs through the compiler. This is the essence of dependently typed array programming.
It became clear that the legacy of a fully-fledged programming language like SAC with many years of development and an existing type system with subtyping and overloading would be a difficult playground to try these new ideas. As a consequence, Qube is designed as a complete but concise array language with dependent array types. Qube's rigorous design allows the compiler to provide strong correctness guarantees, e.g. the absence of out-of-bound array indexing, without overly restricting the set of legal programs, a typical issue in dependently typed programming languages elsewhere.
Dr Clemens Grelck