在 Idris 中生成一个随机整数

【问题标题】：Generate a random integer in Idris在 Idris 中生成一个随机整数
【发布时间】：2021-05-22 23:55:19
【问题描述】：

如何在 Idris 1.3.3 中生成随机整数？

不起作用的示例程序：

module Random

import Effect.Random --This gets me access to the rndInt function

我运行程序如下：

idris random.idr -p effects

尝试 REPL 中的 rndInt 函数，我收到以下错误消息：

*random> rndInt 1 10
(input):Can't infer argument m to rndInt

请在您的答案中包含完整的源代码。谢谢。

【问题讨论】：

标签： idris

【解决方案1】：

详细阐述 Alissa Tung 的回答，这是完整的工作源代码，包括使用系统时间设置随机种子 (srand)：

module Random

import Effect.Random 
import Effects
import System

main : IO ()
main = do
    t <- time
    n <- run $ do 
        srand t
        rndInt 1 100
    putStrLn $ show n

运行：

idris random.idr -p effects

输出：

*random> :exec main
88
*random> :exec main
96
*random> :exec main
19

【讨论】：