如何在Agda中生成随机数

Question

我需要在Agda中生成一个简单的随机数。

我尝试使用谷歌搜索“随机数agda”之类的短语，但找不到任何正常工作的代码。

在Haskell中，代码将是

    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

产出将是

0.7665119

要么

0.43071353

什么Agda代码可以实现相同的结果（如果可能的话）？

工作代码将不胜感激！

Answer 1

最简单的路径可能是假设存在这样一个原语，然后向Agda解释如何使用COMPILE编译指示编译它。

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)

我已经包含了一个main，以便您可以编译此文件（使用agda -c FILENAME）并运行它以查看您确实获得随机浮动。