如何在Lean中使用sockets？Lean4实现TCP服务端与客户端方法

前置准备 #

Lean 4 核心库默认没有封装套接字相关API，所有TCP相关能力都由官方维护的std扩展库提供，你需要先在项目中引入该库，导入对应模块的语句为：

import Std.Net.Socket
open Std.Net Std.Net.Socket

实现TCP客户端 #

客户端核心逻辑为创建套接字、连接远程地址、读写数据、释放资源，示例代码如下：

def tcpClient (host : String) (port : UInt16) : IO Unit := do
  -- 解析远程地址
  let addr ← SockAddr.mk host port AddressFamily.INET SocketType.STREAM Protocol.TCP
  -- 创建TCP套接字
  let sock ← Socket.mk AddressFamily.INET SocketType.STREAM Protocol.TCP
  try
    -- 连接远程服务器
    sock.connect addr
    -- 发送数据
    let sendBytes := "Hello from Lean 4 client".toUTF8
    let _ ← sock.send sendBytes 0
    -- 接收响应
    let mut recvBuf := ByteArray.mkEmpty 1024
    let received ← sock.recv recvBuf 1024 0
    if received > 0 then
      let resp := String.fromUTF8Unchecked (recvBuf.extract 0 received)
      IO.println s!"收到服务器响应：{resp}"
  finally
    -- 关闭套接字释放资源
    sock.close

你可以直接调用tcpClient "127.0.0.1" 8080连接本地的8080端口服务。

实现TCP服务器 #

服务器核心逻辑为创建套接字、绑定本地端口、监听连接、处理客户端请求，示例代码如下：

def tcpServer (port : UInt16) : IO Unit := do
  -- 绑定到所有网卡的指定端口
  let addr ← SockAddr.mkAny port AddressFamily.INET SocketType.STREAM Protocol.TCP
  -- 创建TCP套接字
  let sock ← Socket.mk AddressFamily.INET SocketType.STREAM Protocol.TCP
  try
    -- 允许端口复用
    sock.setOption SocketOption.REUSEADDR true
    -- 绑定地址
    sock.bind addr
    -- 开始监听，backlog设为10
    sock.listen 10
    IO.println s!"TCP服务器已启动，监听端口{port}..."
    -- 循环接受连接
    while true do
      -- 接受新客户端连接
      let (clientSock, clientAddr) ← sock.accept
      IO.println s!"新客户端接入：{clientAddr}"
      -- 异步处理客户端请求避免阻塞主线程
      IO.asTask do
        try
          let mut recvBuf := ByteArray.mkEmpty 1024
          let received ← clientSock.recv recvBuf 1024 0
          if received > 0 then
            let msg := String.fromUTF8Unchecked (recvBuf.extract 0 received)
            IO.println s!"收到客户端消息：{msg}"
            -- 回写响应
            let resp := "Received: " ++ msg
            let _ ← clientSock.send resp.toUTF8 0
        finally
          clientSock.close
  finally
    sock.close

调用tcpServer 8080即可启动监听本地8080端口的TCP服务。

注意事项 #

• 所有套接字操作都属于IO操作，必须运行在IO Monad中
• 示例中省略了详细的错误处理逻辑，生产环境建议对send、recv、connect等方法的返回值做错误判断
• 套接字属于系统资源，使用完毕后必须调用close方法释放，避免资源泄漏
• 如果需要使用IPv6，把AddressFamily.INET替换为AddressFamily.INET6即可

内容的提问来源于stack exchange，提问作者eyelash