Блог

Мне нужно сгенерировать простое случайное число в 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 достигнет тех же результатов (если это возможно)?

Рабочий код будет оценен по достоинству!

Вероятно, самый простой способ — постулировать существование такого примитива, а затем объяснить Agda, как его скомпилировать с помощью 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)
  

Я включил a main , чтобы вы могли скомпилировать этот файл (используя agda -c FILENAME ) и запустить его, чтобы убедиться, что вы действительно получаете случайные числа с плавающей запятой.