14
我想翻譯伊德里斯從Cayenne的例子 - 一種依賴類型的語言paper。在伊德里斯依賴打印printf
這是我到目前爲止有:
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]))
爲了便於與模式匹配爲我趕緊跑進複雜性與String
模式匹配,我使用List Char
代替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
有效? 。
需要提供什麼樣的證明才能使此printf使用運行時字符串? – is7s
@ is7s,好問題,我不知道。自從這個問題/答案以來我沒有和伊德里斯玩過。我可以在http://eb.host.cs.st-andrews.ac.uk/drafts/eff-tutorial.pdf中看到一些想法,它表示_return證明整數與整數本身一起在所需的範圍內_ 。所以我想你將不得不解析格式字符串,並返回一個有格式的證明。 – huynhjl