From 1b15463746a688de38a7af44576b3b540a5bf555 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 21 Jun 2020 15:25:40 +0100 Subject: [PATCH] Update libraries and docs with HasIO/MonadIO --- docs/source/ffi/ffi.rst | 27 ++++++++++------ docs/source/tutorial/interfaces.rst | 19 +++++++++++ libs/contrib/Debug/Buffer.idr | 10 +++--- libs/contrib/System/Random.idr | 12 +++---- libs/network/Network/Socket.idr | 48 ++++++++++++++++------------ libs/network/Network/Socket/Data.idr | 4 +-- libs/network/Network/Socket/Raw.idr | 44 +++++++++++++------------ tests/chez/chez010/CB.idr | 4 +-- 8 files changed, 103 insertions(+), 65 deletions(-) diff --git a/docs/source/ffi/ffi.rst b/docs/source/ffi/ffi.rst index 0179a7cf0..8296c60b8 100644 --- a/docs/source/ffi/ffi.rst +++ b/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: diff --git a/docs/source/tutorial/interfaces.rst b/docs/source/tutorial/interfaces.rst index 13601a9ae..95cd37206 100644 --- a/docs/source/tutorial/interfaces.rst +++ b/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 ============== diff --git a/libs/contrib/Debug/Buffer.idr b/libs/contrib/Debug/Buffer.idr index 5671c7f6c..2f7161402 100644 --- a/libs/contrib/Debug/Buffer.idr +++ b/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) \ No newline at end of file +printBuffer : MonadIO io => Buffer -> io () +printBuffer buf = putStrLn $ !(dumpBuffer buf) diff --git a/libs/contrib/System/Random.idr b/libs/contrib/System/Random.idr index d5ddf438a..c0de3261b 100644 --- a/libs/contrib/System/Random.idr +++ b/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 diff --git a/libs/network/Network/Socket.idr b/libs/network/Network/Socket.idr index e7ebf26e0..38a1d4bd5 100644 --- a/libs/network/Network/Socket.idr +++ b/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 diff --git a/libs/network/Network/Socket/Data.idr b/libs/network/Network/Socket/Data.idr index 0310ce7af..a5df9f585 100644 --- a/libs/network/Network/Socket/Data.idr +++ b/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 diff --git a/libs/network/Network/Socket/Raw.idr b/libs/network/Network/Socket/Raw.idr index 8bbebb8e7..ad4d3f16d 100644 --- a/libs/network/Network/Socket/Raw.idr +++ b/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 diff --git a/tests/chez/chez010/CB.idr b/tests/chez/chez010/CB.idr index 3407df547..80b46cdf0 100644 --- a/tests/chez/chez010/CB.idr +++ b/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))