在Idris中依赖类型的printf
发布时间:2020-12-14 00:46:43 所属栏目:百科 来源:网络整理
导读:我正在尝试将Idris翻译成Cayenne的一个例子 – 一种依赖类型为 paper的语言. 这是我到目前为止 PrintfType : (List Char) - TypePrintfType Nil = StringPrintfType ('%' :: 'd' :: cs) = Int - PrintfType csPrintfType ('%' :: 's' :: cs) = String - Prin
我正在尝试将Idris翻译成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])) 我使用列表字符而不是字符串作为格式参数,以便于模式匹配,因为我很快遇到了与字符串模式匹配的复杂性. 不幸的是,我收到一条错误消息,我无法理解: 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“%s是%d”“答案”42作品?
看起来像idris中有一些
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])) 格式是表示格式字符串的递归数据类型. FInt是一个int占位符,FString是字符串占位符,FChar是一个字符文字.使用格式我可以定义PrintfType并实现printFormat.从那里,我可以顺利地扩展到一个字符串,而不是列表字符或格式值.最终的结果是: *sprintf> printf "the %s is %d" "answer" 42 "the answer is 42" : String (编辑:李大同) 【声明】本站内容均来自网络,其相关言论仅代表作者个人观点,不代表本站立场。若无意侵犯到您的权利,请及时与联系站长删除相关内容! |