Agda 实现类型安全的 printf

by

完整问题描述

首先我自己想了一个比较 naive 的实现,是把printf的填充变量的参数做成一个List,然后对这个List通过 dependent function 的特性进行一些限制,达到类型安全的效果(比如传入一个该List合法的证明)。
于是我写了一个很丑很幼稚很年轻很简单的实现,最后发现传递证明比较繁琐,肯定是不理想的,遂放弃(并没有很好地理由 dependent type 的类型系统对输入做约束)。代码已经写不下去了,存了一个在gist上。
然后我看到了 dram 的回答,写的很 inspiring(首先用一个函数根据输入类型返回printf的类型,然后再写真正的实现),然后我学习了一波之后弄了一个 Agda 的。由于 Agda 对浮点的支持好像很挫,我就把对浮点数的支持改成了对Char类型的支持。
我们先导入一些必需的东西,需要标准库。

module Printf where

open import Data.List using (List; _∷_; [])
open import Data.Char renaming (Char to ℂ; show to showℂ)
open import Data.Nat using (ℕ; _+_)
open import Data.Nat.Show renaming (show to showℕ)
open import Data.Empty
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary using (yes; no)
open import Function
open import Coinduction

open import Data.String using (toList; fromList; String; _++_)

思路是:

  1. 对格式化字符串进行解析,返回一个带元信息的List
  2. 实现一个带元信息的List到完整printf类型的函数
  3. 实现printf

首先我们需要定义这个带元信息的List的成员的 ADT:

data Fmt : Set where
  fmt : ℂ → Fmt
  lit : ℂ → Fmt

然后实现『根据格式化字符判断类型』的函数和『根据格式化字符和对应的类型的值返回字符串』的函数(过于简单,不予赘述。全部照抄 dram 版本):

ftype : ℂ → Set
ftype 'd' = ℕ
ftype 'c' = ℂ
ftype _ = ⊥

format : (c : ℂ) → ftype c → String
format 'd' = showℕ
format 'c' c = fromList $ c ∷ []
format _ = const ""

然后实现『解析格式化字符串,返回带元信息的List』:

parseF : List ℂ → List Fmt
parseF [] = []
parseF (x ∷ xs) with xs | x ≟ '%'
...         | '%' ∷ xss | yes _ = lit '%' ∷ parseF xss
...         |  c  ∷ xss | yes _ = fmt c ∷ parseF xss
...         | [] | yes _ = lit '%' ∷ []
...         | _  | no  _ = lit x ∷ parseF xs

然后这个函数 Agda 给我报了个 termination error,我觉得不大对劲。于是我去问了,维护者说是因为with给函数加了一层 pm 导致 Agda 无法判断这个函数是正确的。
这也太智障了吧,但好在我看懂了 dram 的实现,就重写了一个不用with的(其实我也不是很懂为什么 dram 要用with,我觉得超难用):

parseF : List ℂ → List Fmt
parseF [] = []
parseF ('%' ∷ '%' ∷ cs) = lit '%' ∷ parseF cs
parseF ('%' ∷  c  ∷ cs) = fmt c ∷ parseF cs
parseF ( c  ∷  cs) = lit c ∷ parseF cs

然后这个就 check 了,我们再实现『根据格式化字符串判断printf完整类型』的函数:

ptype : List Fmt → Set
ptype [] = String
ptype (fmt x ∷ xs) = ftype x → ptype xs
ptype (lit x ∷ xs) = ptype xs

printfType : String → Set
printfType = ptype ∘ parseF ∘ toList

最后实现printf的逻辑:

printfImpl : (fmt : List Fmt) → String → ptype fmt
printfImpl [] pref = pref
printfImpl (fmt x ∷ xs) pref val = printfImpl xs $ pref ++ format x val
printfImpl (lit x ∷ xs) pref = printfImpl xs $ pref ++ (fromList $ x ∷ [])

然后把它包一层:

printf : (fmt : String) → printfType fmt
printf s = printfImpl (parseF $ toList s) ""

随手证明:

proof₀ : printf "Hello, World!"
              ≡ "Hello, World!"
proof₀ = refl

proof₁ : printf "%% %% (%d + %d = %d) (toChar %d = %c)" 114 514 628 6 '6'
              ≡ "% % (114 + 514 = 628) (toChar 6 = 6)"
proof₁ = refl

我们还可以加入字符串支持。 修改以下函数:

ftype : ℂ → Set
ftype 'd' = ℕ
ftype 'c' = ℂ
ftype 's' = String
ftype _ = ⊥

format : (c : ℂ) → ftype c → String
format 'd' = showℕ
format 'c' c = fromList $ c ∷ []
format 's' = id
format _ = const ""

然后验证:

proof₂ : printf "%d岁,是%s" 24 "学生"
              ≡ "24岁,是学生"
proof₂ = refl

错误情况的证明:

proof₃ : printf "%d岁,是%s" 25 "学生"
              ≢ "24岁,是学生"
proof₃ ()

怎么样,是不是妙不可言。 错误情况的证明需要修改一句import

open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)

完整实现


Tweet this
Top


创建一个 issue 以申请评论
Create an issue to apply for commentary


协议/License

本作品 Agda 实现类型安全的 printf 采用 知识共享署名-非商业性使用-禁止演绎 4.0 国际许可协议 进行许可,基于 http://ice1000.org/2018/08/04/TypeSafePrintf/ 上的作品创作。
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
知识共享许可协议