Idrisに依存型printf

Question

私はIdryに翻訳しようとしていますからの例Cayenne - 従属型の言語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])) 

私はすぐにパターンがStringに一致すると複雑に走ったようなパターンマッチングを容易にするために、私はフォーマット引数にStringの代わりにList Charを使用しています：ここで

は、私がこれまで持っているものです。私は3つの PrintfTypeの要素（ '%' :: ...を持つもの）と printfで、すべてのパターンマッチの例をコメントアウトした場合、その後、

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 

：

は、残念ながら、私は私がの意味を理解することはできませんよ、エラーメッセージが表示されますコードはコンパイルされます（しかし、明らかに興味深いことはありません）。

printf "the %s is %d" "answer" 42が機能するようにコードを修正するにはどうすればよいですか？ 。

Answer 1

はパターンが重複する機能を定義するときイドリスでいくつかcurrent limitationsがあるように見えます（'%' :: '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はcharリテラルです。Formatを使用してPrintfTypeを定義し、​​を実装できます。そこからスムーズに拡張できますList CharまたはFormatの値ではなく文字列を使用してください。最終結果は

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