[Agda] Using Haskell randomRIO functions from Agda

[Serge Leblanc]

Hi, could someone explain to me how to adapt the aguments in my 
primRandomRIO function?

{-# OPTIONS --guardedness #-}

module Random2 where

   import IO.Primitive as Prim
   open import IO
   open import Agda.Builtin.Char

   randomRIO : Char → Char → IO Char
   randomRIO lo hi = lift (primRandomRIO lo hi) where

     postulate
       primRandomRIO : Char → Char → Prim.IO Char

     {-# FOREIGN GHC import qualified System.Random as Random #-}
     {-# COMPILE GHC primRandomRIO = \ _ l h -> Random.randomRIO (l , h) #-}

   open import Agda.Builtin.String using (primShowChar)
   open import Function

   main : Main
   main = run $ randomRIO 'a' 'z' >>=  putStrLn ∘ primShowChar

Thanks.

Compiling Random2 in /home/serge/agda/Random2.agdai to 
/home/serge/agda/MAlonzo/Code/Random2.hs
Calling: ghc -O -o /home/serge/agda/Random2 -Werror -i/home/serge/agda 
-main-is MAlonzo.Code.Random2 /home/serge/agda/MAlonzo/Code/Random2.hs 
--make -fwarn-incomplete-patterns -fno-warn-overlapping-patterns
[13 of 13] Compiling MAlonzo.Code.Random2 ( 
/home/serge/agda/MAlonzo/Code/Random2.hs, 
/home/serge/agda/MAlonzo/Code/Random2.o )
Compilation error:

/home/serge/agda/MAlonzo/Code/Random2.hs:32:18: error:
     • Couldn't match type ‘Char’
                      with ‘IO MAlonzo.Code.Agda.Builtin.Char.T6’
       Expected type: MAlonzo.Code.Agda.Builtin.Char.T6
                      -> MAlonzo.Code.Agda.Builtin.IO.T8
                           () MAlonzo.Code.Agda.Builtin.Char.T6
         Actual type: MAlonzo.Code.Agda.Builtin.Char.T6
                      -> MAlonzo.Code.Agda.Builtin.Char.T6
     • In the expression: Random.randomRIO (l, h)
       In the expression: \ _ l h -> Random.randomRIO (l, h)
       In an equation for ‘d12’: d12 = \ _ l h -> Random.randomRIO (l, h)
    |
32 | d12 = \ _ l h -> Random.randomRIO (l , h)
    |                  ^^^^^^^^^^^^^^^^^^^^^^^^

-- 
Serge Leblanc
------------------------------------------------------------------------
GnuPG Fingerprint = 123E 9312 453A 8F8E 7FDB ABD7 D2B8 A282 5F8D ABB7
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20211016/90c4778d/attachment.html>
-------------- next part --------------
{-# OPTIONS --guardedness #-}

module Random2 where

  import IO.Primitive as Prim
  open import IO
  open import Agda.Builtin.Char

  randomRIO : Char → Char → IO Char
  randomRIO lo hi = lift (primRandomRIO lo hi) where

    postulate
      primRandomRIO : Char → Char → Prim.IO Char

    {-# FOREIGN GHC import qualified System.Random as Random #-}
    {-# COMPILE GHC primRandomRIO = \ _ l h -> Random.randomRIO (l , h) #-}

  open import Agda.Builtin.String using (primShowChar)
  open import Function

  main : Main
  main = run $ randomRIO 'a' 'z' >>=  putStrLn ∘ primShowChar
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xD2B8A2825F8DABB7.asc
Type: application/pgp-keys
Size: 654 bytes
Desc: OpenPGP public key
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20211016/90c4778d/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 236 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20211016/90c4778d/attachment.sig>