如何解决我怎么知道什么时候类型签名是完整的?
module Print
data Format : Type where
Num : Format -> Format
Str : Format -> Format
Lit : String -> Format -> Format
End : Format
PrintfType : Format -> Type
PrintfType (Num f) = (i : Int) -> PrintfType f
PrintfType (Str f) = (s : String) -> PrintfType f
PrintfType (Lit _ f) = PrintfType f
PrintfType End = String
printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Num f) acc = \i => printfFmt f (acc ++ show i)
printfFmt (Str f) acc = \s => printfFmt f (acc ++ s)
printfFmt (Lit s f) acc = printfFmt f (acc ++ s)
printfFmt End acc = acc
printf : (fmt : Format) -> PrintfType fmt
printf fmt = printfFmt fmt ""
-- Is this function possible?
printLst : {fmt : Format} -> List Format -> String -> PrintfType fmt
printLst [] x = ?printLst_rhs_1
printLst (y :: xs) x = let now = printfFmt y ""
in printLst xs ?now
-- printLst [Str End,Num End] "" ["a",1]
-- # "a1"
扩展论文实践中的定量类型理论,第 2.3.1 节计算类型中的示例。
参考:https://arxiv.org/pdf/2104.00480.pdf
如果我想实现一个适用于格式列表的 printLst
函数。
更新:printLst
函数将采用格式列表和遵循格式列表中指定格式的输入列表。
printLst [Str End,1]
# output: "a1"
我怎么知道这个类型签名是否完整?
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。