在Idris中运行时键入函数

Question

我已经讨论了类型驱动的开发,并且有一个类型很好的部分printf,其中类型是从第一个参数计算的,它是一个格式字符串:

printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))

toFormat从a创建格式表示,List Char并PrintfType从这种格式表示中创建函数类型.完整的代码在这里:https://github.com/edwinb/TypeDD-Samples/blob/master/Chapter6/Printf.idr

我理解代码printf "%c %c" 'a' 'b'的作用printf "%c %c是什么- 计算的类型Char -> Char -> String.

我不明白的是当第一个参数在运行时未知时会发生什么.我理解为什么一般这样的代码不应该编译:格式字符串和结果类型,如果用户在运行时输入它们,则无法在编译时知道,但我不知道背后的实际技术推理这种直觉.

例如:

main : IO ()
main = do fmt <- getLine
          c1 <- getChar
          c2 <- getChar
          printf fmt c1 c2

导致以下错误消息:

When checking an application of function Prelude.Monad.>>=:
        printf fmt does not have a function type (PrintfType (toFormat (unpack fmt)))

我想我正在尝试理解这个错误信息.伊德里斯是否将此类功能视为一种特殊情况？

Answer 1

的类型printf fmt : PrintfType (toFormat (unpack fmt))不能被进一步评估,因为fmt : String在编译时是未知的.所以对于伊德里斯来说,这不是一个功能 - 它A不是A -> B.这就是错误信息所说的内容.

对于你的情况,你必须在运行时检查是否PrintfType (toFormat (unpack fmt))是String -> String.

作为一个例子,这里有两个函数采用格式,并可能返回一个证明它是正确的格式:

endFmt : (fmt : Format) -> Maybe (PrintfType fmt = String)
endFmt End = Just Refl
endFmt (Lit str fmt) = endFmt fmt
endFmt fmt = Nothing

strFmt : (fmt : Format) -> Maybe ((PrintfType fmt) = (String -> String))
strFmt (Str fmt) = case endFmt fmt of
  Just ok => rewrite ok in Just Refl
  Nothing => Nothing
strFmt (Lit str fmt) = strFmt fmt
strFmt fmt = Nothing

然后,我们可以调用strFmt用toFormat (unpack fmt),并有处理这两种Maybe情况.因为Idris在应用证明方面存在问题,所以我们提供帮助replace.

main : IO ()
main = do fmt <- getLine
          str <- getLine
          case strFmt (toFormat (unpack fmt)) of
            Just ok => let printer = replace ok {P=id} (printf fmt) in
              putStrLn $ printer str
              -- in a better world you would only need
              -- putStrLn $ printf fmt str
            Nothing => putStrLn "Wrong format"

有了这个,我们可以运行:

:exec main
foo %s bar  -- fmt
and         -- str
foo and bar -- printf fmt str