我正在尝试将 Cayenne 中的一个示例翻译成 Idris - 一种具有依赖类型的语言 paper .
这是我到目前为止所拥有的:
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
用于格式参数,以促进模式匹配,因为我在 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
如果我在
'%' :: ...
中用 3 个元素(带有 PrintfType
的那些)注释掉所有模式匹配案例和 printf
,然后代码编译(但显然没有做任何有趣的事情)。如何修复我的代码,以便
printf "the %s is %d" "answer" 42
作品?
最佳答案
好像有一些current limitations在 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
是一个字 rune 字。使用 Format
我可以定义 PrintfType
并实现printFormat
.从那里,我可以顺利扩展以获取字符串而不是 List Char
或 Format
值(value)。最终结果是:*sprintf> printf "the %s is %d" "answer" 42
"the answer is 42" : String
关于idris - 在 Idris 中依赖类型的 printf,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/17905537/