The best way to convert a String to an Integer or Natural in Idris

Question

What is the best way to convert a String to an Integer or Natural in Idris?

I know the standard library is still a work in progress and so if the answer is I should add it to the standard library then that's fine I will try and do that, but before I thought I would confirm there isn't already a way.

The best I could come up with is this if I want to read an Index from the user:

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

But this way, I get no indication of failure from cast. Not only is the fact that indexAsString might not be in format allowing it to be converted to an Integer, but on top of that it doesn't even fail at runtime, producing 0 as a result of a "bad cast".

Please tell me there is a better way and/or point me in the right direction.

As a side note, is there a particular reason there is no Read typeclass in Idris? Or has it just not made it in yet?

Thx in advance.

Answer 1

Idris has a parseInteger and parsePositive function in Data.String with the type signatures

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

and

Num a => String -> Maybe a

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

Answer 2

I may mistake but I try to share what I think about it. indication of failure is about parsing.

In old idris repository I can see readInt which is String -> Maybe Int but I don't know where is it now.

Howerver there is custom implementation I found 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 "."

It's easy to read how does it work. charToInt (probably I think it could be coded better but I don't know how) is based on cast , parse is processing Integers one by one recursive doing *10 for each new Integer from List (e.g. symbol) and parseInt maps unpacked String with charToInt and getting the result passing it to parse. ! is alike =<< in Haskell.