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

Question

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

我知道标准库仍然是一个正在进行中的工作,所以如果答案是我应该将它添加到标准库然后我会尝试这样做,但在我认为我会确认还没有办法之前.

如果我想从用户那里读取索引,我能想到的最好的是:

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类型类？或者它还没有成功呢？

Thx提前.

Answer 1

伊德里斯拥有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