从寒假开始，断断续续地玩了两个月 Idris。最开始让我决定开 Idris 这个坑的还是 这篇文章 中的这句话：
Idris 是极少几种可以实现强类型 printf 的语言。
那么下面就开始利用依赖类型构造一个强类型的 printf 函数吧！
¶HList
为了更容易实现强类型 printf，我需要实现一个 HList（heterogenous list）类型。HList 是一种可以包含不同类型元素的列表，其定义类似于 Vect（带长度的列表，依赖类型里一般叫作 vector）：
（以后 Idris 源码中都默认带有 %access public export 和 %default total。）
1data HList : {default Type t : _} -> (ts : List t) -> Type where
2 Nil : HList []
3 (::) : a -> HList ts -> HList (a :: ts)
它的类型中有一个 List t 参数来指定每个元素的类型。在 我的 GitHub 上还有一些简单函数的定义，但这里只需要这个类型定义就够了。
（prism.js 不支持 Idris，差评……）
¶实现 format 函数
要实现一个简单的类型安全的 format 函数，其第二个参数（格式化数据）的类型要依赖于第一个参数（格式化字符串），因此需要先实现由第一个参数得到第二个参数类型的函数。一开始我是由第一个参数直接得到第二个参数，但不明原因导致编译不过。参考了 GitHub 上已有的实现以后添加了一个中间类型来表示格式化字符串的解析结果：
1data Fmt = FInt | FInteger | FNat | FDouble | FString | FLiteral Char
2
3toFmt : String -> List Fmt
4toFmt = toFmt' . unpack
5 where toFmt' ('%' :: c :: r) =
6 (:: toFmt' r) $ case c of
7 'd' => FInt
8 'l' => FInteger
9 'u' => FNat
10 'e' => FDouble
11 's' => FString
12 '%' => FLiteral '%'
13 _ => assert_unreachable
14 toFmt' (c :: r) = FLiteral c :: toFmt' r
15 toFmt' [] = []
toFmt 函数用于把字符串转换为 Fmt 类型。由于这个函数只用于类型推导，所以那个 assert_unreachable 是没有影响的。
然后就是函数 formatTy：
1formatTy : List Fmt -> List Type
2formatTy = flip foldr [] $ \fmt => case fmt of
3 FInt => (Int ::)
4 FInteger => (Integer ::)
5 FNat => (Nat ::)
6 FDouble => (Double ::)
7 FString => (String ::)
8 _ => id
把这个函数的值喂给 HList 就是第二个参数的类型了。（这里函数式的 point-free 技巧用得有点多，希望不影响阅读。）
这样，formatHList 函数就很好定义了：
1formatHList : (fmtStr : String) -> HList (formatTy $ toFmt fmtStr) -> String
2formatHList fmtStr = formatHList' (toFmt fmtStr)
3 where formatHList' : (fmt : List Fmt) -> HList (formatTy fmt) -> String
4 formatHList' (FInt :: rFmt) (x :: r) = show x ++ formatHList' rFmt r
5 formatHList' (FInteger :: rFmt) (x :: r) = show x ++ formatHList' rFmt r
6 (...)
下面大段的重复代码被我省略了。这里的重点是函数的类型：第一个参数为 String 类型，第二个参数的类型为 HList (formatTy $ toFmt fmtStr) 依赖了第一个参数的值。当第一个参数改变，第二个参数所需要的类型也会相应改变。实际的效果就是：当使用者写错了格式化字符串或格式化参数，程序都会编译不过。这就是我们的目的。
¶柯里化
目的达到了，但是注意这个函数接受了一个 HList 作为参数列表。这在函数式语言中是非常难看的。由于这里用了 HList，所以可以写一个通用的函数来柯里化所有接受 HList 作为参数的函数：
1curryHListTy : List Type -> Type -> Type
2curryHListTy (t :: r) u = t -> curryHListTy r u
3curryHListTy [] u = u
4
5curryHList : (HList ts -> u) -> curryHListTy ts u
6curryHList {ts = _ :: _} f = \x => curryHList (\l => f (x :: l))
7curryHList {ts = []} f = f []
curryHList 的第二个参数的类型同样依赖于第一个参数的类型。它接受一个函数，返回一个柯里化的函数。于是之前的 formatHList 函数可以用它柯里化成多参数的函数了：
1format : (fmtStr : String) -> curryHListTy (formatTy $ toFmt fmtStr) String
2format fmtStr = curryHList $ formatHList fmtStr
最后实现 printfHList 和 printf 函数：
1printfHList : (fmtStr : String) -> HList (formatTy $ toFmt fmtStr) -> IO ()
2printfHList fmtStr args = putStr $ formatHList fmtStr args
3
4printf : (fmtStr : String) -> curryHListTy (formatTy $ toFmt fmtStr) (IO ())
5printf fmtStr = curryHList $ printfHList fmtStr
完成！从这个函数的实现可以窥见类型系统的强大之处。效果：
1*Sandbox> format "hello, %s" "problem233"
2"hello, problem233" : String
3*Sandbox> format "hello, %s" 1
4(input):1:1-20:String is not a numeric type
5*Sandbox> format "hello, %s. you're the %uth visitor" "problem233" 20
6"hello, problem233. you're the 20th visitor" : String
7*Sandbox> format "hello, %s. you're the %uth visitor" "problem233" (-1)
8(input):1:1-61:Can't find implementation for Neg Nat
9*Sandbox> format "hello, %p" "problem233"
10(input):1:1-31:format "hello, %p" does not have a function type (curryHListTy (formatTy (toFmt "hello, %p")) String)