Select from static format strings at runtime

db/posts/5.json

@@ -1,6 +1,7 @@
 {
   "edited-at": [
-    "2025-02-14T12:00:50.492225-05:00"
+    "2025-02-14T12:00:50.492225-05:00",
+    "2025-02-14T23:42:15.625034-05:00"
   ],
   "hidden": false,
   "idris": true,

projects/Idris/src/LessMacrosMoreTypes/Printf.md

@@ -5,6 +5,9 @@ module LessMacrosMoreTypes.Printf
 
 import Data.List
 import System
+
+-- Only needed for addenda
+import Data.Vect
 ```
 
 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.
@@ -328,6 +331,9 @@ We've made a fun little function that works much like C's `printf` function or R
 
 Avoiding using a macro also gives us a lot of neat bonuses, like `printf` automatically playing nice with partial application and currying, with no extra effort on our part.
 
+> [!NOTE]
+> The `the (List _) x` construction here in explicit type annotation, needed because of an ambiguity in list-type literals introduced by importing `Data.Vect` for the addenda
+
 ```idris hide
 -- @@test partial application
 partialApplication : IO Bool
@@ -336,7 +342,7 @@ partialApplication = do
 ```
 <div class="unit-test">
 ```idris
-  map (printf "Hello %s") ["Alice", "Bob"] == ["Hello Alice", "Hello Bob"]
+  map (printf "Hello %s") (the (List _) ["Alice", "Bob"]) == ["Hello Alice", "Hello Bob"]
 ```
 </div>
 
@@ -393,5 +399,47 @@ The need for a bespoke data structure for `PrintfInput` also isn't ideal.
 
 We will delve in ways to rectify all of these complaints in future entries in this series.
 
+## Addenda
+
+### Selecting from a list of format strings with matching type signatures
+
+As long as the format strings are known at compile time, `PrintfType` will fully expand to a function type signature that contains no references to the string. For example, `PrintfType (parseFormat (unpack "%s"))` expands to `String -> String`.
+
+We can take advantage of this by indexing a container type by the `PrintfType` of a "template" format string, and then our container can hold any formatting function of compatible type signature, like so:
+
+```idris
+formatChoices : Vect 3 (PrintfType (parseFormat (unpack "%s")))
+formatChoices = [printf "Hello %s!", printf "Nice to meet you %s", printf "\"%s\""]
+```
+
+We can then index out a single format function from this container (it doesn't have to be a `Vect`, it could also be a map indexed by the format string itself, for instance):
+
+```idris hide
+-- @@test formatChoicesOne
+formatChoicesOne : IO Bool
+formatChoicesOne = do
+  pure $ 
+```
+<div class="unit-test">
+```idris
+  let f = index 1 formatChoices in f "Alice" == "Nice to meet you Alice"
+```
+</div>
+
+Or apply all of the contained formatting functions to the same string:
+
+```idris hide
+-- @@test formatChoicesAll
+formatChoicesAll : IO Bool
+formatChoicesAll = do
+  pure $ 
+```
+<div class="unit-test">
+```idris
+  (formatChoices <*> replicate _ "World")
+    == ["Hello World!", "Nice to meet you World", "\"World\""]
+```
+</div>
+
 
 [^1]: Ignoring for a second the special handling for format strings in modern compilers