时间戳

首页 > 解决方案 > 如何在 Agda 中生成随机数

random - 如何在 Agda 中生成随机数

问题描述

我需要在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 代码会达到相同的结果（如果可能的话）？

工作代码将不胜感激！

标签： randomagda

解决方案

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

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）并运行它以查看您确实得到了随机浮点数。

推荐阅读