Less Macros, More Types

Macros are annoying, but an unfortunate fact of life in many programming languages.

Especially in languages with nominally "strong" type systems, like Rust, macros are quite frequently needed to work around the type system to avoid needless repetition when consuming an API, generate formulaic boilerplate that only exists to please the type system, or work around the lack of variadic functions for things like printf. Lets explore the ways we can use dependently typed constructs to eliminate the need for such macros.

 2025-07-14
 55m / 43m / 36m
 2 articles

Type Safe Variadic printf

While C can provide "convenient" string formatting by having hideously unsafe variadics, and dynamic languages, like python, can do the same, many type safe languages, such as Rust, are forced to provide such functionality through the use of a macro. Dependently typed languages, like Idris, can provide a printf like formatting interface, while maintaining both memory and type safety, without the need for macros. We will explore this by implementing a simplified version of printf in Idris from scratch.

Row Polymorphic Programming

Sometimes, especially when dealing with business logic, we have to deal with data that comes in from the real world, or elsewhere, naturally very messily typed, leading to nasty type signatures and messes of macros or code generation to build data structures from a schema. Row polymorphism can help us by abstracting over the fields contained in a record type in the type signature, letting us define records based on data, concatenate records together, and define functions that are generic across any record containing the required fields, all without macros.