Random Double from Haskell in Idris

random_double.idr

module RandomDouble

import Data.Bits
import Data.Vect
import Effects
import Effect.StdIO
import Effect.Random

-- 2^53 as an Integer
twoTo53 : Integer
twoTo53 = cast (pow 2 53)

-- 2^53 as a Double
twoTo53d : Double
twoTo53d = cast twoTo53

-- Bit mask
maskb : Bits 64
maskb = intToBits {n=64} (twoTo53 - 1)

-- Minimum bound for a signed 64-bit integer
minInt : Integer
minInt = -9223372036854775808

-- Maximum bound for a signed 64-bit integer
maxInt : Integer
maxInt = 9223372036854775807

-- Convert a 64-bit Integer into a Double in the half-open unit interval [0.0, 1.0)
intToUnitInterval : Integer -> Double
intToUnitInterval x = let xb = intToBits {n=64} x
                          maskedb = maskb `and` xb 
                          maskedd = the Double (cast (bitsToInt maskedb)) in
                          maskedd / twoTo53d

rndDouble : Eff Double [RND]
rndDouble = pure $ intToUnitInterval !(rndInt 0 maxInt)

Layer : Nat -> Type
Layer n = Vect n Double

initLayer : (n : Nat) -> Layer n
initLayer Z = []
initLayer (S k) = (runPure rndDouble) :: initLayer k

main : IO ()
main = do
  let x = initLayer 5
  putStrLn (show x)