Number Parsing in Idris

Here’s the translation of the number parsing example from Go to Idris, formatted in Markdown suitable for Hugo:

import Data.String

main : IO ()
main = do
    -- With parseDouble, we can parse floating-point numbers
    let f = fromMaybe 0.0 $ parseDouble "1.234"
    putStrLn $ show f

    -- For parseInt, we can specify the base (10 for decimal)
    let i = fromMaybe 0 $ parseInteger 10 "123"
    putStrLn $ show i

    -- parseInt will recognize hex-formatted numbers with base 16
    let d = fromMaybe 0 $ parseInteger 16 "1c8"
    putStrLn $ show d

    -- For parsing unsigned integers, we can use parsePositive
    let u = fromMaybe 0 $ parsePositive "789"
    putStrLn $ show u

    -- For basic base-10 integer parsing, we can use cast
    let k = cast "135" :: Integer
    putStrLn $ show k

    -- Parse functions return a Maybe type, which is None on bad input
    let e = parseInteger 10 "wat"
    putStrLn $ show e

This program demonstrates number parsing in Idris. Here’s a breakdown of the code:

1. We use parseDouble from the Data.String module to parse floating-point numbers. It returns a Maybe Double, so we use fromMaybe to provide a default value if parsing fails.

2. For parsing integers, we use parseInteger which takes a base as its first argument. We use base 10 for decimal numbers.

3. We can parse hexadecimal numbers by using parseInteger with base 16.

4. For parsing unsigned integers, Idris provides parsePositive.

5. Idris allows us to use cast for basic type conversions, including parsing strings to integers.

6. When parsing fails, these functions return Nothing. We demonstrate this by trying to parse an invalid input “wat”.

Note that Idris’s approach to error handling is different. Instead of returning an error value, Idris uses the Maybe type to represent the possibility of parsing failure.

To run this program, save it as NumberParsing.idr and use the Idris interpreter:

$ idris NumberParsing.idr -o number-parsing
$ ./number-parsing
1.234
123
456
789
135
Nothing

This example showcases Idris’s strong type system and its approach to handling potential failures in parsing operations.