<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<p><font color="#0070ff"><font color="#000000">Hi, could someone
explain to me how to adapt the aguments in my primRandomRIO
function?<br>
</font></font></p>
<p><font color="#0070ff"><font color="#000000">{-# OPTIONS
--guardedness #-}<br>
<br>
module Random2 where<br>
<br>
import IO.Primitive as Prim<br>
open import IO<br>
open import Agda.Builtin.Char<br>
<br>
randomRIO : Char → Char → IO Char<br>
randomRIO lo hi = lift (primRandomRIO lo hi) where<br>
<br>
postulate<br>
primRandomRIO : Char → Char → Prim.IO Char<br>
<br>
{-# FOREIGN GHC import qualified System.Random as Random
#-}<br>
{-# COMPILE GHC primRandomRIO = \ _ l h ->
Random.randomRIO (l , h) #-}<br>
<br>
open import Agda.Builtin.String using (primShowChar)<br>
open import Function<br>
<br>
main : Main<br>
main = run $ randomRIO 'a' 'z' >>= putStrLn ∘
primShowChar<br>
<br>
</font></font></p>
<p><font color="#0070ff"><font color="#000000">Thanks.</font><br>
</font></p>
<p><font color="#0070ff">Compiling Random2 in
/home/serge/agda/Random2.agdai to
/home/serge/agda/MAlonzo/Code/Random2.hs<br>
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<br>
[13 of 13] Compiling MAlonzo.Code.Random2 (
/home/serge/agda/MAlonzo/Code/Random2.hs,
/home/serge/agda/MAlonzo/Code/Random2.o )<br>
Compilation error:<br>
<br>
/home/serge/agda/MAlonzo/Code/<a class="moz-txt-link-freetext" href="Random2.hs:32:18">Random2.hs:32:18</a>: error:<br>
• Couldn't match type ‘Char’<br>
with ‘IO MAlonzo.Code.Agda.Builtin.Char.T6’<br>
Expected type: MAlonzo.Code.Agda.Builtin.Char.T6<br>
-> MAlonzo.Code.Agda.Builtin.IO.T8<br>
() MAlonzo.Code.Agda.Builtin.Char.T6<br>
Actual type: MAlonzo.Code.Agda.Builtin.Char.T6<br>
-> MAlonzo.Code.Agda.Builtin.Char.T6<br>
• In the expression: Random.randomRIO (l, h)<br>
In the expression: \ _ l h -> Random.randomRIO (l, h)<br>
In an equation for ‘d12’: d12 = \ _ l h ->
Random.randomRIO (l, h)<br>
|<br>
32 | d12 = \ _ l h -> Random.randomRIO (l , h)<br>
| ^^^^^^^^^^^^^^^^^^^^^^^^<br>
</font><br>
</p>
<div class="moz-signature">-- <br>
Serge Leblanc
<hr>
GnuPG Fingerprint = 123E 9312 453A 8F8E 7FDB ABD7 D2B8 A282 5F8D
ABB7</div>
</body>
</html>