Как генерировать случайные числа в Агде - PullRequest
Новая
       15

Как генерировать случайные числа в Агде

0 голосов
/ 11 апреля 2019

Мне нужно сгенерировать простое случайное число в Agda .

Я попробовал поискать в Google фразы вроде «случайное число 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

Какой код Агды достиг бы таких же результатов (если это возможно)?

Хотелось бы получить рабочий код!

1 Ответ

4 голосов
/ 11 апреля 2019

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

...