CODEWITHSUNDEEP
randomagda
Adjam
Adjam

Reputation: 640

How to generate random numbers in Agda

I need to generate a simple random number in Agda.

I tried googling phrases like 'random number agda' but couldn't find any working code.

In Haskell the code would be

    import System.Random

main :: IO ()
main = do
    -- num :: Float
    num <- randomIO :: IO Float
    -- This "extracts" the float from IO Float and binds it to the name num
    print $ num

outputs would be

0.7665119

or

0.43071353

What Agda code would achieve the same results (if it's possible)?

Working code would be appreciated!

Upvotes: 1

Views: 296

Answers (1)

gallais
gallais

Reputation: 12103

The easiest route is probably to postulate the existence of such a primitive and then to explain to Agda how to compile it by using a COMPILE pragma.

open import Agda.Builtin.Float
import IO.Primitive as Prim
open import IO

random : IO Float
random = lift primRandom where

 postulate primRandom : Prim.IO Float
 {-# FOREIGN GHC import qualified System.Random as Random #-}
 {-# COMPILE GHC primRandom = Random.randomIO #-}

open import Codata.Musical.Notation
open import Function

main : Prim.IO _
main = run $
  ♯ random >>= λ f → ♯ putStrLn (primShowFloat f)

I've included a main so that you can compile this file (using agda -c FILENAME) and run it to see that you indeed get random floats.

Upvotes: 4

Related Questions