Random Numbers in Idris

Our example demonstrates how to generate random numbers in Idris. Idris doesn’t have a built-in random number generator in its standard library, so we’ll use the random package from the contrib library.

module Main

import System.Random

main : IO ()
main = do
    -- Generate a random integer between 0 and 99
    n1 <- randomRIO (0, 99)
    n2 <- randomRIO (0, 99)
    putStrLn $ show n1 ++ "," ++ show n2

    -- Generate a random float between 0.0 and 1.0
    f <- randomRIO (0.0, 1.0)
    putStrLn $ show f

    -- Generate random floats between 5.0 and 10.0
    f1 <- randomRIO (5.0, 10.0)
    f2 <- randomRIO (5.0, 10.0)
    putStrLn $ show f1 ++ "," ++ show f2

    -- Use a specific seed for reproducible results
    let seed = 42
    let gen = mkStdGen seed
    let (n3, gen') = randomR (0, 99) gen
    let (n4, _) = randomR (0, 99) gen'
    putStrLn $ show n3 ++ "," ++ show n4

    -- Using the same seed will produce the same sequence
    let gen2 = mkStdGen seed
    let (n5, gen2') = randomR (0, 99) gen2
    let (n6, _) = randomR (0, 99) gen2'
    putStrLn $ show n5 ++ "," ++ show n6

To use this code, you’ll need to install the contrib package and import System.Random. Here’s a brief explanation of what the code does:

1. We use randomRIO to generate random numbers within a specified range. This function returns an IO action that produces a random number.

2. For floating-point numbers between 0.0 and 1.0, we use randomRIO (0.0, 1.0).

3. To generate floats in a different range (e.g., 5.0 to 10.0), we directly specify the range in randomRIO.

4. To use a specific seed for reproducible results, we use mkStdGen to create a random number generator with a given seed. We then use randomR to generate random numbers from this generator.

5. Using the same seed will produce the same sequence of random numbers, as demonstrated in the last part of the code.

When you run this program, you might see output similar to this:

$ idris -p contrib Main.idr -o random-numbers
$ ./random-numbers
68,56
0.8090228139659177
5.840125017402497,6.937056298890035
94,49
94,49

Note that the actual numbers will be different each time you run the program, except for the last two lines which use a fixed seed.

Idris’s random number generation is based on the Haskell implementation, which uses a splittable random number generator. This is different from the PCG algorithm mentioned in the original example, but it serves a similar purpose of providing pseudorandom numbers.

For more advanced random number generation techniques or different distributions, you might need to implement them yourself or look for additional libraries.