依赖类型的printf在Idris中的应用

Question

依赖类型的printf在Idris中的应用

16

我正在尝试将来自《Cayenne - 一种依赖类型语言》paper的示例翻译成 Idris。

以下是我目前的进展：

PrintfType : (List Char) -> Type
PrintfType Nil                = String
PrintfType ('%' :: 'd' :: cs) = Int -> PrintfType cs
PrintfType ('%' :: 's' :: cs) = String -> PrintfType cs
PrintfType ('%' ::  _  :: cs) = PrintfType cs
PrintfType ( _  :: cs)        = PrintfType cs

printf : (fmt: List Char) -> PrintfType fmt
printf fmt = rec fmt "" where
  rec : (f: List Char) -> String -> PrintfType f
  rec Nil acc = acc
  rec ('%' :: 'd' :: cs) acc = \i => rec cs (acc ++ (show i))
  rec ('%' :: 's' :: cs) acc = \s => rec cs (acc ++ s) 
  rec ('%' ::  _  :: cs) acc = rec cs acc  -- this is line 49
  rec ( c  :: cs)        acc = rec cs (acc ++ (pack [c]))

我将使用List Char代替String作为format参数，以便更容易地进行模式匹配，因为在String上进行模式匹配时很容易遇到复杂性问题。

不幸的是，我收到了一个错误消息，我无法理解：

Type checking ./sprintf.idr
sprintf.idr:49:Can't unify PrintfType (Prelude.List.:: '%' (Prelude.List.:: t cs)) with PrintfType cs

Specifically:
    Can't convert PrintfType (Prelude.List.:: '%' (Prelude.List.:: t cs)) with PrintfType cs

如果我在PrintfType和printf中注释掉所有具有3个元素的模式匹配案例（即带有'%' :: ...的案例），那么代码就可以编译（但显然不会执行任何有趣的操作）。

我该如何修复我的代码，以便printf "the %s is %d" "answer" 42能够正常工作？

- huynhjl

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- huynhjl · Accepted Answer

看起来在idris中定义有重叠模式的函数时存在一些当前限制（例如'%' :: 'd'与c :: cs重叠）。经过多次尝试，我终于想出了一个解决方法：

data Format = End | FInt Format | FString Format | FChar Char Format
fromList : List Char -> Format
fromList Nil                = End
fromList ('%' :: 'd' :: cs) = FInt    (fromList cs)
fromList ('%' :: 's' :: cs) = FString (fromList cs)
fromList (c :: cs)          = FChar c (fromList cs)

PrintfType : Format -> Type
PrintfType End            = String
PrintfType (FInt rest)    = Int -> PrintfType rest
PrintfType (FString rest) = String -> PrintfType rest
PrintfType (FChar c rest) = PrintfType rest

printf : (fmt: String) -> PrintfType (fromList $ unpack fmt)
printf fmt = printFormat (fromList $ unpack fmt) where
  printFormat : (fmt: Format) -> PrintfType fmt
  printFormat fmt = rec fmt "" where
    rec : (f: Format) -> String -> PrintfType f
    rec End acc            = acc
    rec (FInt rest) acc    = \i: Int => rec rest (acc ++ (show i))
    rec (FString rest) acc = \s: String => rec rest (acc ++ s)
    rec (FChar c rest) acc = rec rest (acc ++ (pack [c]))

Format是一个递归数据类型，代表格式化字符串。 FInt是一个int占位符，FString是一个字符串占位符，而FChar则表示字符文字。使用Format我可以定义PrintfType并实现printFormat。从那里开始，我可以顺畅地扩展以接受字符串，而不是List Char或Format值。最终结果如下：

*sprintf> printf "the %s is %d" "answer" 42
"the answer is 42" : String