Start of variadic printf post

db/posts/5.json

@@ -0,0 +1,14 @@
+{
+  "edited-at": [
+  ],
+  "hidden": false,
+  "idris": true,
+  "ipkg": "/home/nathan/Projects/Blog/projects/Idris/Idris.ipkg",
+  "posted-at": "2025-02-09T06:23:37.499533-05:00",
+  "slugs": [
+  ],
+  "source": "/home/nathan/Projects/Blog/projects/Idris/src/LessMacrosMoreTypes/Printf.md",
+  "tags": [
+    "idris"
+  ]
+}

db/series/0.json

@@ -0,0 +1,7 @@
+{
+  "desc": "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.",
+  "post-ids": [
+    5
+  ],
+  "title": "Less Macros, More Types"
+}

projects/Idris/Idris.ipkg

@@ -18,6 +18,7 @@ authors = "Nathan McCarty"
 -- modules to install
 modules = Idris
         , Posts.HelloWorld
+        , LessMacrosMoreTypes.Printf
 
 -- main file (i.e. file to load at REPL)
 -- main =

projects/Idris/src/LessMacrosMoreTypes/Printf.md

@@ -0,0 +1,45 @@
+# Type Safe Variadic printf
+
+```idris hide
+module LessMacrosMoreTypes.Printf
+
+%default total
+```
+
+While C can provide convenient string formatting by having hideously memory
+unsafe variadics, and dynamic languages, like python, can do the same while
+being memory safe by not being type safe, 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 saftey, without the need for
+the macro. We will explore this by implementing a simplified version of `printf`
+in Idris from scratch.
+
+This article is inspired by an exercise from chapter 6 of [Type Driven
+Development with
+Idris](https://www.manning.com/books/type-driven-development-with-idris), and is
+written as a literate Idris file.
+
+## Gameplan
+
+Our goal is to provide a printf function that can be called, much like it's C equivlant, like so:
+
+> [!NOTE]
+> As this is a literate Idris document, and we haven't defined our `printf`
+> function yet, we have to use a `failing` block to ask the compiler to check
+> that this code parses, and syntax highlight it for us, but not attempt to
+> actually compile it.
+
+```idris
+failing
+  example_usage : String
+  example_usage = printf "%s %d %02d" "hello" 1 2
+```
+
+
+
+## Parsing a Format String
+
+## Calculating a Type From a Format String
+
+## printf