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

在Idris 中将字符串转换为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可能没有采用允许将其转换为Integer的格式，而且甚至在运行时也不会失败，由于的“错误转换”而产生0的事实。

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

附带说明一下，是否有特定原因导致Idris中没有Read类型类？还是它还没有加入呢？

提前谢谢。

最佳答案

Idris在parseInteger中具有类型签名的parsePositive和Data.String函数

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