Search code examples
stringintegertype-conversionidris

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


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.


Solution

  • 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