IdrisDoc: Network.Socket

# Network.Socket

Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.

Original (C) SimonJF, MIT Licensed, 2014
Modified (C) The Idris Community, 2015, 2016

socket : (fam : SocketFamily) -> (ty : SocketType) -> (pnum : ProtocolNumber) -> IO (Either SocketError Socket)

  Creates a UNIX socket with the given family, socket type and protocol
  number. Returns either a socket or an error.

sockaddr_free : SockaddrPtr -> IO ()
sock_free : BufPtr -> IO ()

  Frees a given pointer

sock_alloc : ByteLength -> IO BufPtr

  Allocates an amount of memory given by the ByteLength parameter.

  Used to allocate a mutable pointer to be given to the Recv functions.

sendTo : (sock : Socket) -> (addr : SocketAddress) -> (port : Port) -> (msg : String) -> IO (Either SocketError ByteLength)

  Send a message.

  Returns on failure a `SocketError`
  Returns on success the `ResultCode`

  sock

    The socket on which to send the message.

  addr

    Address of the recipient.

  port

    The port on which to send the message.

  msg

    The message to send.

send : (sock : Socket) -> (msg : String) -> IO (Either SocketError ResultCode)

  Send data on the specified socket.

  Returns on failure a `SocketError`.
  Returns on success the `ResultCode`.

  sock

    The socket on which to send the message.

  msg

    The data to send.

recvFrom : (sock : Socket) -> (len : ByteLength) -> IO (Either SocketError ( UDPAddrInfo, String, ResultCode))

  Receive a message.

  Returns on failure a `SocketError`.
  Returns on success a triple of

  - `UDPAddrInfo` :: The address of the sender.
  - `String` :: The payload.
  - `Int` :: Result value from underlying function.
  sock

    The channel on which to receive.

  len

    Size of the expected message.

recv : (sock : Socket) -> (len : ByteLength) -> IO (Either SocketError ( String, ResultCode))

  Receive data on the specified socket.

  Returns on failure a `SocketError`
  Returns on success a pairing of:

  - `String` :: The payload.
  - `ResultCode` :: The result of the underlying function.
  sock

    The socket on which to receive the message.

  len

    How much of the data to send.

listen : (sock : Socket) -> IO Int

  Listens on a bound socket.

  sock

    The socket to listen on.

connect : (sock : Socket) -> (addr : SocketAddress) -> (port : Port) -> IO ResultCode

  Connects to a given address and port.
  Returns 0 on success, and an error number on error.

close : Socket -> IO ()

  Close a socket

bind : (sock : Socket) -> (addr : Maybe SocketAddress) -> (port : Port) -> IO Int

  Binds a socket to the given socket address and port.
  Returns 0 on success, an error code otherwise.

accept : (sock : Socket) -> IO (Either SocketError ( Socket, SocketAddress))

  Accept a connection on the provided socket.

  Returns on failure a `SocketError`
  Returns on success a pairing of:

  - `Socket` :: The socket representing the connection.
  - `SocketAddress` :: The
  sock

    The socket used to establish connection.

record UDPRecvData
  MkUDPRecvData : (remote_addr : SocketAddress) -> (remote_port : Port) -> (recv_data : String) -> (data_len : Int) -> UDPRecvData
  remote_addr : (rec : UDPRecvData) -> SocketAddress
  remote_port : (rec : UDPRecvData) -> Port
  recv_data : (rec : UDPRecvData) -> String
  data_len : (rec : UDPRecvData) -> Int
record UDPAddrInfo
  MkUDPAddrInfo : (remote_addr : SocketAddress) -> (remote_port : Port) -> UDPAddrInfo
  remote_addr : (rec : UDPAddrInfo) -> SocketAddress
  remote_port : (rec : UDPAddrInfo) -> Port
interface ToCode
  toCode : ToCode a => a -> Int
data SocketType : Type

  Socket Types.

  NotASocket : SocketType

    Not a socket, used in certain operations

  Stream : SocketType

    TCP

  Datagram : SocketType

    UDP

  RawSocket : SocketType

    Raw sockets

data SocketFamily : Type

  Socket Families

  The ones that people might actually use. We're not going to need US
  Government proprietary ones.

  AF_UNSPEC : SocketFamily

    Unspecified

  AF_INET : SocketFamily

    IP / UDP etc. IPv4

  AF_INET6 : SocketFamily

    IP / UDP etc. IPv6

SocketError : Type

  SocketError: Error thrown by a socket operation

SocketDescriptor : Type

  SocketDescriptor: Native C Socket Descriptor

data SocketAddress : Type

  Network Addresses

  IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress
  IPv6Addr : SocketAddress

    Not implemented (yet)

  Hostname : String -> SocketAddress
  InvalidAddress : SocketAddress

    Used when there's a parse error

record Socket

  The metadata about a socket

  MkSocket : (descriptor : SocketDescriptor) -> (family : SocketFamily) -> (socketType : SocketType) -> (protocolNumber : ProtocolNumber) -> Socket
  descriptor : (rec : Socket) -> SocketDescriptor
  family : (rec : Socket) -> SocketFamily
  socketType : (rec : Socket) -> SocketType
  protocolNumber : (rec : Socket) -> ProtocolNumber
data SockaddrPtr : Type
  SAPtr : Ptr -> SockaddrPtr
ResultCode : Type
ProtocolNumber : Type

  Protocol Number.

  Generally good enough to just set it to 0.

Port : Type
MkUDPRecvData : (remote_addr : SocketAddress) -> (remote_port : Port) -> (recv_data : String) -> (data_len : Int) -> UDPRecvData
MkUDPAddrInfo : (remote_addr : SocketAddress) -> (remote_port : Port) -> UDPAddrInfo
MkSocket : (descriptor : SocketDescriptor) -> (family : SocketFamily) -> (socketType : SocketType) -> (protocolNumber : ProtocolNumber) -> Socket
EAGAIN : Int
ByteLength : Type
data BufPtr : Type
  BPtr : Ptr -> BufPtr
BACKLOG : Int

  Backlog used within listen() call -- number of incoming calls