Update libraries and docs with HasIO/MonadIO

docs/source/ffi/ffi.rst

@@ -88,17 +88,19 @@ returns a primitive IO action:
 
 Internally, ``PrimIO Int`` is a function which takes the current (linear)
 state of the world, and returns an ``Int`` with an updated state of the world.
-We can convert this into an ``IO`` action using ``primIO``:
+In general, ``IO`` operations in an Idris program are defined as instances
+of the ``HasIO`` interface (or ``MonadIO``). We can convert a primitive
+operation to one usable in ``HasIO`` using ``primIO``:
 
 .. code-block:: idris
 
-    primIO : PrimIO a -> IO a
+    primIO : HasIO a => PrimIO a -> io a
 
 So, we can extend our program as follows:
 
 .. code-block:: idris
 
-  addWithMessage : String -> Int -> Int -> IO Int
+  addWithMessage : HasIO io => String -> Int -> Int -> io Int
   addWithMessage s x y = primIO $ prim_addWithMessage s x y
   
   main : IO ()
@@ -218,16 +220,17 @@ which takes a callback that takes a ``char*`` and an ``int`` and returns a
         return f(x, y);
     }
 
-Then, we can access this from Idris by declaring it as a ``%foreign``
-function and wrapping it in ``IO``, with the C function calling the Idris
-function as the callback:
+Then, we can access this from Idris by declaring it as a ``%foreign`` function
+and wrapping it in the ``HasIO`` interface, with the C function calling the
+Idris function as the callback:
 
 .. code-block:: idris
 
     %foreign (libsmall "applyFn")
     prim_applyFn : String -> Int -> (String -> Int -> String) -> PrimIO String
     
-    applyFn : String -> Int -> (String -> Int -> String) -> IO String
+    applyFn : HasIO io =>
+              String -> Int -> (String -> Int -> String) -> io String
     applyFn c i f = primIO $ prim_applyFn c i f
 
 For example, we can try this as follows:
@@ -256,14 +259,18 @@ As a variant, the callback could have a side effect:
     prim_applyFnIO : String -> Int -> (String -> Int -> PrimIO String) ->
                      PrimIO String
   
-This is a little more fiddly to lift to an ``IO`` function, due to the callback,
-but we can do so using ``toPrim : IO a -> PrimIO a``:
+This is a little more fiddly to lift to a ``HasIO`` function,
+due to the callback, but we can do so using ``toPrim : IO a -> PrimIO a``:
   
 .. code-block:: idris
 
-    applyFnIO : String -> Int -> (String -> Int -> IO String) -> IO String
+    applyFnIO : HasIO io =>
+                String -> Int -> (String -> Int -> IO String) -> io String
     applyFnIO c i f = primIO $ prim_applyFnIO c i (\s, i => toPrim $ f s i)
   
+Note that the callback is explicitly in ``IO`` here, since ``HasIO`` doesn't
+have a general method for extracting the primitive ``IO`` operation.
+
 For example, we can extend the above ``pluralise`` example to print a message
 in the callback:
 

docs/source/tutorial/interfaces.rst

@@ -428,6 +428,25 @@ would be:
     m_add : Maybe Int -> Maybe Int -> Maybe Int
     m_add x y = [ x' + y' | x' <- x, y' <- y ]
 
+Interfaces and IO
+=================
+
+In general, ``IO`` operations in the libraries aren't written using ``IO``
+directly, but rather via one of the following interfaces:
+
+.. code-block:: idris
+
+    interface HasIO io where
+      liftIO : (1 _ : IO a) -> io a
+
+    interface (Monad io, HasIO io) => MonadIO io where
+
+``HasIO`` explains, via ``liftIO``, how to convert a primitive ``IO`` operation
+to an operation in some underlying type. ``MonadIO`` has no methods, but
+adds an additional ``Monad`` constraint. These interfaces allow a programmer
+to define some more expressive notion of interactive program, while still
+giving direct access to ``IO`` primitives.
+
 Idiom brackets
 ==============
 

libs/contrib/Debug/Buffer.idr

@@ -31,14 +31,14 @@ group n xs = worker [] xs
         worker acc ys = worker ((take n ys)::acc) (drop n ys)
 
 export
-dumpBuffer : Buffer -> IO String
+dumpBuffer : MonadIO io => Buffer -> io String
 dumpBuffer buf = do
-    size <- rawSize buf
-    dat <- bufferData buf
+    size <- liftIO $ rawSize buf
+    dat <- liftIO $ bufferData buf
     let rows = group 16 dat
     let hex = showSep "\n" 0 (map renderRow rows)
     pure $ hex ++ "\n\ntotal size = " ++ show size
 
 export
-printBuffer : Buffer -> IO ()
-printBuffer buf = putStrLn $ !(dumpBuffer buf)
+printBuffer : MonadIO io => Buffer -> io ()
+printBuffer buf = putStrLn $ !(dumpBuffer buf)

libs/contrib/System/Random.idr

@@ -6,12 +6,12 @@ import Data.List
 
 public export
 interface Random a where
-  randomIO : IO a
+  randomIO : MonadIO io => io a
 
   -- Takes a range (lo, hi), and returns a random value uniformly
   -- distributed in the closed interval [lo, hi]. It is unspecified what
   -- happens if lo > hi.
-  randomRIO : (a, a) -> IO a
+  randomRIO : MonadIO io => (a, a) -> io a
 
 prim_randomInt : Int -> IO Int
 prim_randomInt upperBound = schemeCall Int "blodwen-random" [upperBound]
@@ -23,12 +23,12 @@ Random Int where
     let maxInt = shiftL 1 31 - 1
         minInt = negate $ shiftL 1 31
         range = maxInt - minInt
-     in map (+ minInt) $ prim_randomInt range
+     in map (+ minInt) $ liftIO $ prim_randomInt range
 
   -- Generate a random value within [lo, hi].
   randomRIO (lo, hi) =
     let range = hi - lo + 1
-     in map (+ lo) $ prim_randomInt range
+     in map (+ lo) $ liftIO $ prim_randomInt range
 
 prim_randomDouble : IO Double
 prim_randomDouble = schemeCall Double "blodwen-random" []
@@ -36,10 +36,10 @@ prim_randomDouble = schemeCall Double "blodwen-random" []
 public export
 Random Double where
   -- Generate a random value within [0, 1].
-  randomIO = prim_randomDouble
+  randomIO = liftIO prim_randomDouble
 
   -- Generate a random value within [lo, hi].
-  randomRIO (lo, hi) = map ((+ lo) . (* (hi - lo))) prim_randomDouble
+  randomRIO (lo, hi) = map ((+ lo) . (* (hi - lo))) (liftIO prim_randomDouble)
 
 ||| Sets the random seed
 export

libs/network/Network/Socket.idr

@@ -14,10 +14,11 @@ import Network.FFI
 ||| Creates a UNIX socket with the given family, socket type and protocol
 ||| number. Returns either a socket or an error.
 export
-socket : (fam  : SocketFamily)
+socket : MonadIO io
+      => (fam  : SocketFamily)
       -> (ty   : SocketType)
       -> (pnum : ProtocolNumber)
-      -> IO (Either SocketError Socket)
+      -> io (Either SocketError Socket)
 socket sf st pn = do
   socket_res <- primIO $ idrnet_socket (toCode sf) (toCode st) pn
 
@@ -27,17 +28,18 @@ socket sf st pn = do
 
 ||| Close a socket
 export
-close : Socket -> IO ()
+close : MonadIO io => Socket -> io ()
 close sock = do _ <- primIO $ socket_close $ descriptor sock
                 pure ()
 
 ||| Binds a socket to the given socket address and port.
 ||| Returns 0 on success, an error code otherwise.
 export
-bind : (sock : Socket)
+bind : MonadIO io
+    => (sock : Socket)
     -> (addr : Maybe SocketAddress)
     -> (port : Port)
-    -> IO Int
+    -> io Int
 bind sock addr port = do
     bind_res <- primIO $ idrnet_bind
                   (descriptor sock)
@@ -57,10 +59,11 @@ bind sock addr port = do
 ||| Connects to a given address and port.
 ||| Returns 0 on success, and an error number on error.
 export
-connect : (sock : Socket)
+connect : MonadIO io
+       => (sock : Socket)
        -> (addr : SocketAddress)
        -> (port : Port)
-       -> IO ResultCode
+       -> io ResultCode
 connect sock addr port = do
   conn_res <- primIO $ idrnet_connect
               (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port
@@ -73,7 +76,7 @@ connect sock addr port = do
 |||
 ||| @sock The socket to listen on.
 export
-listen : (sock : Socket) -> IO Int
+listen : MonadIO io => (sock : Socket) -> io Int
 listen sock = do
   listen_res <- primIO $ socket_listen (descriptor sock) BACKLOG 
   if listen_res == (-1)
@@ -89,8 +92,9 @@ listen sock = do
 |||
 ||| @sock The socket used to establish connection.
 export
-accept : (sock : Socket)
-      -> IO (Either SocketError (Socket, SocketAddress))
+accept : MonadIO io
+      => (sock : Socket)
+      -> io (Either SocketError (Socket, SocketAddress))
 accept sock = do
 
   -- We need a pointer to a sockaddr structure. This is then passed into
@@ -115,9 +119,10 @@ accept sock = do
 ||| @sock The socket on which to send the message.
 ||| @msg  The data to send.
 export
-send : (sock : Socket)
+send : MonadIO io
+    => (sock : Socket)
     -> (msg  : String)
-    -> IO (Either SocketError ResultCode)
+    -> io (Either SocketError ResultCode)
 send sock dat = do
   send_res <- primIO $ idrnet_send (descriptor sock) dat 
 
@@ -135,9 +140,10 @@ send sock dat = do
 ||| @sock The socket on which to receive the message.
 ||| @len  How much of the data to receive.
 export
-recv : (sock : Socket)
+recv : MonadIO io
+    => (sock : Socket)
     -> (len : ByteLength)
-    -> IO (Either SocketError (String, ResultCode))
+    -> io (Either SocketError (String, ResultCode))
 recv sock len = do
   -- Firstly make the request, get some kind of recv structure which
   -- contains the result of the recv and possibly the retrieved payload
@@ -166,11 +172,11 @@ recv sock len = do
 |||
 ||| @sock The socket on which to receive the message.
 export
-recvAll : (sock : Socket) -> IO (Either SocketError String)
+recvAll : MonadIO io => (sock : Socket) -> io (Either SocketError String)
 recvAll sock = recvRec sock [] 64
   where
     partial
-    recvRec : Socket -> List String -> ByteLength -> IO (Either SocketError String)
+    recvRec : Socket -> List String -> ByteLength -> io (Either SocketError String)
     recvRec sock acc n = do res <- recv sock n
                             case res of
                               Left c => pure (Left c)
@@ -188,11 +194,12 @@ recvAll sock = recvRec sock [] 64
 ||| @port The port on which to send the message.
 ||| @msg  The message to send.
 export
-sendTo : (sock : Socket)
+sendTo : MonadIO io
+      => (sock : Socket)
       -> (addr : SocketAddress)
       -> (port : Port)
       -> (msg  : String)
-      -> IO (Either SocketError ByteLength)
+      -> io (Either SocketError ByteLength)
 sendTo sock addr p dat = do
   sendto_res <- primIO $ idrnet_sendto
                 (descriptor sock) dat (show addr) p (toCode $ family sock)
@@ -213,9 +220,10 @@ sendTo sock addr p dat = do
 ||| @len  Size of the expected message.
 |||
 export
-recvFrom : (sock : Socket)
+recvFrom : MonadIO io
+        => (sock : Socket)
         -> (len  : ByteLength)
-        -> IO (Either SocketError (UDPAddrInfo, String, ResultCode))
+        -> io (Either SocketError (UDPAddrInfo, String, ResultCode))
 recvFrom sock bl = do
   recv_ptr <- primIO $ idrnet_recvfrom
                        (descriptor sock) bl 

libs/network/Network/Socket/Data.idr

@@ -68,11 +68,11 @@ idrnet_isNull : (ptr : AnyPtr) -> PrimIO Int
 
 
 export
-getErrno : IO SocketError
+getErrno : HasIO io => io SocketError
 getErrno = primIO $ idrnet_errno
 
 export
-nullPtr : AnyPtr -> IO Bool
+nullPtr : MonadIO io => AnyPtr -> io Bool
 nullPtr p = do 0 <- primIO  $ idrnet_isNull p
                | _ => pure True
                pure False

libs/network/Network/Socket/Raw.idr

@@ -27,39 +27,39 @@ data SockaddrPtr = SAPtr AnyPtr
 
 ||| Put a value in a buffer
 export
-sock_poke : BufPtr -> Int -> Int -> IO ()
+sock_poke : HasIO io => BufPtr -> Int -> Int -> io ()
 sock_poke (BPtr ptr) offset val = primIO $ idrnet_poke ptr offset val
 
 ||| Take a value from a buffer
 export
-sock_peek : BufPtr -> Int -> IO Int
+sock_peek : HasIO io => BufPtr -> Int -> io Int
 sock_peek (BPtr ptr) offset = primIO $ idrnet_peek ptr offset
 
 ||| Frees a given pointer
 export
-sock_free : BufPtr -> IO ()
+sock_free : HasIO io => BufPtr -> io ()
 sock_free (BPtr ptr) = primIO $ idrnet_free ptr
 
 export
-sockaddr_free : SockaddrPtr -> IO ()
+sockaddr_free : HasIO io => SockaddrPtr -> io ()
 sockaddr_free (SAPtr ptr) = primIO $ idrnet_free ptr
 
 ||| Allocates an amount of memory given by the ByteLength parameter.
 |||
 ||| Used to allocate a mutable pointer to be given to the Recv functions.
 export
-sock_alloc : ByteLength -> IO BufPtr
+sock_alloc : MonadIO io => ByteLength -> io BufPtr
 sock_alloc bl = map BPtr $ primIO $ idrnet_malloc bl
 
 ||| Retrieves the port the given socket is bound to
 export
-getSockPort : Socket -> IO Port
+getSockPort : HasIO io => Socket -> io Port
 getSockPort sock = primIO $ idrnet_sockaddr_port $ descriptor sock
 
 
 ||| Retrieves a socket address from a sockaddr pointer
 export
-getSockAddr : SockaddrPtr -> IO SocketAddress
+getSockAddr : MonadIO io => SockaddrPtr -> io SocketAddress
 getSockAddr (SAPtr ptr) = do
   addr_family_int <- primIO $ idrnet_sockaddr_family ptr
 
@@ -73,12 +73,12 @@ getSockAddr (SAPtr ptr) = do
     Just AF_UNSPEC => pure InvalidAddress)
 
 export
-freeRecvStruct : RecvStructPtr -> IO ()
+freeRecvStruct : HasIO io => RecvStructPtr -> io ()
 freeRecvStruct (RSPtr p) = primIO $ idrnet_free_recv_struct p
 
 ||| Utility to extract data.
 export
-freeRecvfromStruct : RecvfromStructPtr -> IO ()
+freeRecvfromStruct : HasIO io => RecvfromStructPtr -> io ()
 freeRecvfromStruct (RFPtr p) = primIO $ idrnet_free_recvfrom_struct p
 
 ||| Sends the data in a given memory location
@@ -90,10 +90,11 @@ freeRecvfromStruct (RFPtr p) = primIO $ idrnet_free_recvfrom_struct p
 ||| @ptr  The location containing the data to send.
 ||| @len  How much of the data to send.
 export
-sendBuf : (sock : Socket)
+sendBuf : MonadIO io
+       => (sock : Socket)
        -> (ptr  : BufPtr)
        -> (len  : ByteLength)
-       -> IO (Either SocketError ResultCode)
+       -> io (Either SocketError ResultCode)
 sendBuf sock (BPtr ptr) len = do
   send_res <- primIO $ idrnet_send_buf (descriptor sock) ptr len
 
@@ -110,10 +111,11 @@ sendBuf sock (BPtr ptr) len = do
 ||| @ptr  The location containing the data to receive.
 ||| @len  How much of the data to receive.
 export
-recvBuf : (sock : Socket)
+recvBuf : MonadIO io
+       => (sock : Socket)
        -> (ptr  : BufPtr)
        -> (len  : ByteLength)
-       -> IO (Either SocketError ResultCode)
+       -> io (Either SocketError ResultCode)
 recvBuf sock (BPtr ptr) len = do
   recv_res <- primIO $ idrnet_recv_buf (descriptor sock) ptr len
 
@@ -132,12 +134,13 @@ recvBuf sock (BPtr ptr) len = do
 ||| @ptr  A Pointer to the buffer containing the message.
 ||| @len  The size of the message.
 export
-sendToBuf : (sock : Socket)
+sendToBuf : MonadIO io
+         => (sock : Socket)
          -> (addr : SocketAddress)
          -> (port : Port)
          -> (ptr  : BufPtr)
          -> (len  : ByteLength)
-         -> IO (Either SocketError ResultCode)
+         -> io (Either SocketError ResultCode)
 sendToBuf sock addr p (BPtr dat) len = do
   sendto_res <- primIO $ idrnet_sendto_buf
                 (descriptor sock) dat len (show addr) p (toCode $ family sock)
@@ -148,19 +151,19 @@ sendToBuf sock addr p (BPtr dat) len = do
 
 ||| Utility function to get the payload of the sent message as a `String`.
 export
-foreignGetRecvfromPayload : RecvfromStructPtr -> IO String
+foreignGetRecvfromPayload : HasIO io => RecvfromStructPtr -> io String
 foreignGetRecvfromPayload (RFPtr p) = primIO $ idrnet_get_recvfrom_payload p 
 
 ||| Utility function to return senders socket address.
 export
-foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress
+foreignGetRecvfromAddr : MonadIO io => RecvfromStructPtr -> io SocketAddress
 foreignGetRecvfromAddr (RFPtr p) = do
   sockaddr_ptr <- map SAPtr $ primIO $ idrnet_get_recvfrom_sockaddr p
   getSockAddr sockaddr_ptr
 
 ||| Utility function to return sender's IPV4 port.
 export
-foreignGetRecvfromPort : RecvfromStructPtr -> IO Port
+foreignGetRecvfromPort : MonadIO io => RecvfromStructPtr -> io Port
 foreignGetRecvfromPort (RFPtr p) = do
   sockaddr_ptr <- primIO $ idrnet_get_recvfrom_sockaddr p
   port         <- primIO $ idrnet_sockaddr_ipv4_port sockaddr_ptr
@@ -178,10 +181,11 @@ foreignGetRecvfromPort (RFPtr p) = do
 ||| @len  Size of the expected message.
 |||
 export
-recvFromBuf : (sock : Socket)
+recvFromBuf : MonadIO io
+           => (sock : Socket)
            -> (ptr  : BufPtr)
            -> (len  : ByteLength)
-           -> IO (Either SocketError (UDPAddrInfo, ResultCode))
+           -> io (Either SocketError (UDPAddrInfo, ResultCode))
 recvFromBuf sock (BPtr ptr) bl = do
   recv_ptr <- primIO $ idrnet_recvfrom_buf (descriptor sock) ptr bl
 

tests/chez/chez010/CB.idr

@@ -13,11 +13,11 @@ prim_applyCharFn : Char -> Int -> (Char -> Int -> PrimIO Char) -> PrimIO Char
 %foreign libcb "applyIntFnPure"
 applyIntFnPure : Int -> Int -> (Int -> Int -> Int) -> Int
 
-applyIntFn : Int -> Int -> (Int -> Int -> IO Int) -> IO Int
+applyIntFn : HasIO io => Int -> Int -> (Int -> Int -> IO Int) -> io Int
 applyIntFn x y fn
     = primIO $ prim_applyIntFn x y (\a, b => toPrim (fn a b))
 
-applyCharFn : Char -> Int -> (Char -> Int -> IO Char) -> IO Char
+applyCharFn : HasIO io => Char -> Int -> (Char -> Int -> IO Char) -> io Char
 applyCharFn x y fn
     = primIO $ prim_applyCharFn x y (\a, b => toPrim (fn a b))