本文介绍了如何在依赖类型语言 Idris 中实现类似 C 语言 printf 函数的功能，同时保持内存和类型安全，且无需使用宏。

• 游戏计划：目标是提供一个 printf 函数，其调用方式类似于 C 语言中的 printf。Idris 缺乏专门的可变参数设施，但可在类型签名中调用函数来实现。通过将格式字符串解析为数据结构，并将其传递给计算 printf 函数其余类型签名的类型级函数来实现可变参数的 printf 函数。
• 解析格式字符串：定义了 Format 数据类型来描述格式字符串，包括各种格式说明符和字面量组件的构造函数。还编写了辅助函数 parseNumber 和 parseLiteral 来解析数字和字面量。通过基本的模式匹配来解析格式字符串，并返回 Maybe Format 以表示格式字符串的有效性。
• 根据格式字符串计算类型：定义了两个变体的 PrintfType 类型级函数，一个处理 Format，另一个处理 Maybe Format。通过模式匹配和递归调用计算类型签名。
• 使用运行时格式字符串：定义了一个辅助函数 blackbox 来隐藏值以避免类型检查。构造了一个可与运行时格式字符串一起使用的 printf 变体，通过定义自定义的数据结构 PrintfInput 和相应的 printfFmtInput 函数来处理输入。
• 结论：实现了一个类似于 C 语言 printf 函数的函数，但避免了使用宏和不安全的可变参数机制。然而，该函数的接口并不理想，存在一些问题，如在格式字符串无效时没有编译器错误，错误消息模糊等，这些问题将在后续的系列文章中进行改进。
• 附录：介绍了如何在编译时已知格式字符串的情况下，通过索引容器类型来选择具有匹配类型签名的格式字符串，并可以对相同的字符串应用所有包含的格式化函数。