Agda实现自定义sprintf函数时字符模式匹配报错，能否匹配指定字符？

没问题！你完全可以在Agda里对'1'、't'、'O'这类字符字面量进行模式匹配——你遇到的编译错误根本不是字符匹配本身的问题，而是两个容易和Idris语法混淆的细节导致的：

错误原因解析 #

1. 列表构造符用错了：Idris里的列表构造符是ASCII的::，但Agda里对应的是Unicode符号∷（可以通过输入\cons或者\::来插入这个符号）。你写的::在Agda里会被当成未定义的运算符，导致编译器无法解析列表模式。
2. 多余的括号：Agda中函数应用是靠空格分隔参数的，不需要给参数模式包裹括号。你给parseFormat的参数加了括号，打乱了编译器的语法解析逻辑。

修正后的代码 #

把这两个问题修复后，你的代码就能正常编译了：

module Printf where
open import Agda.Builtin.List
open import Agda.Builtin.Char
open import Agda.Builtin.String
open import Agda.Builtin.Float
open import Agda.Builtin.Int

data Format : Set where
  TChar : Char → Format → Format
  TString : Format → Format
  TFloat : Format → Format
  TInt : Format → Format
  TEnd : Format

parseFormat : List Char → Format
parseFormat ('%' ∷ 's' ∷ rest) = TString (parseFormat rest)
parseFormat ('%' ∷ 'f' ∷ rest) = TFloat (parseFormat rest)
parseFormat ('%' ∷ 'd' ∷ rest) = TInt (parseFormat rest)
parseFormat ('%' ∷ '%' ∷ rest) = TChar '%' (parseFormat rest)
parseFormat (x ∷ rest) = TChar x (parseFormat rest)
parseFormat [] = TEnd

额外说明 #

之后如果要扩展模式匹配，比如匹配't'或者'O'这类字符，直接像下面这样写模式就可以了：

parseFormat ('t' ∷ rest) = -- 你的处理逻辑
parseFormat ('O' ∷ rest) = -- 你的处理逻辑

内容的提问来源于stack exchange，提问作者Артём Мухамед-Каримов МПБ-802