Refinement Kinds

Automated code generation, domain specific languages, and meta-programming are increasingly becoming productivity drivers for the software industry, while also making programming more accessible to non-experts, and, more generally, increasing the level of abstraction expressible in languages and tools for program construction.

Unfortunately, meta-programming constructs and idioms aggressively challenge the safety guarantees of static typing, which becomes especially problematic given that meta-programs are notoriously hard to test for correctness. To address this issue, I have co-developed the concept of refinement kind. Refinement kinds lift the now well-known concept of refinement types to the realm of kinds (i.e., the classifiers of types). By introducing logical refinements in the kind structure, we are able to express predicates on the structure of types, effectively allowing us to manipulate types as first-class labelled trees, statically and at runtime, in a declarative way. This general framework allows us to support sophisticated statically typed meta-programming concepts. Moreover, by leveraging the stratification between types and kinds, our design shows that arguably advanced type-level features can be integrated into a general purpose language without the need to fundamentally alter the language’s type system and its associated rules.

We have only begun to flesh out the concept of refinement kinds and its implications.

  1. Refinement kinds: Type-safe Programming with Practical Type-level Computation
    Luís Caires and Bernardo Toninho
    Proc. of the ACM on Programming Languages (PACMPL) issue ACM SIGPLAN Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH-OOPSLA), vol. 3, 2019
    [PDF, Code, Talk]