在 Idris 中将字符串转换为整数或自然的最佳方法

Question

在 Idris 中将 String 转换为 Integer 或 Natural 的最佳方法是什么？

我知道标准库仍在进行中，所以如果答案是我应该将它添加到标准库中，那很好，我会尝试这样做，但在我想我会确认之前没有一种方式。

如果我想从用户那里读取索引，我能想到的最好方法是这样的：

indexAsString <- getLine
let indexAsInt : Integer = cast indexAsString
let items: Vect _ _ = ["shoe", "bat", "hat"]
let i = integerToFin indexAsInt $ length items
maybe (print "invalid index") (\ii => print $ index ii items) i

但是这样，我没有从演员表中得到失败的迹象。不仅 indexAsString 的格式可能不允许将其转换为整数，而且最重要的是它在运行时甚至不会失败，由于“错误转换”而产生 0。

请告诉我有更好的方法和/或指出正确的方向。

顺便说一句，Idris 中没有 Read 类型类是否有特殊原因？还是只是还没有进入？

提前致谢。

Answer 1

Idris 在Data.String 中有一个parseInteger 和parsePositive 函数，带有类型签名

Num a => Neg a => String -> Maybe a

和

Num a => String -> Maybe a

http://www.idris-lang.org/docs/current/base_doc/docs/Data.String.html

Answer 2

我可能会出错，但我会尝试分享我的想法。 指示失败是关于解析的。

在旧的 idris 存储库中，我可以看到 readInt，即 String -> Maybe Int，但我不知道它现在在哪里。

但是我找到了自定义实现 here:

charToInt : Char -> Maybe Int
charToInt c = let i = cast {to=Int} c in
              let zero = cast {to=Int} '0' in
              let nine = cast {to=Int} '9' in
              if i < zero || i > nine
                then Nothing
                else Just (i - zero)

total
parse' : Int -> List Int -> Maybe Int
parse' _   []      = Nothing
parse' acc [d]     = Just (10 * acc + d)
parse' acc (d::ds) = parse' (10 * acc + d) ds


total parseInt : String -> Maybe Int
parseInt str = (sequence (map charToInt (unpack str))) >>= parse' 0

main : IO ()
main = do let r = parseInt !getLine
          putStrLn "."

很容易阅读它是如何工作的。 charToInt （可能我认为它可以更好地编码，但我不知道如何）基于 cast ，parse 正在处理整数，对 List 中的每个新整数（例如符号) 和parseInt 将解压的String 与charToInt 映射，并将结果传递给parse。 ! 与 Haskell 中的 =<< 相似。