idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.46k stars 368 forks source link

Remove 'Closed' state from linear network API #3252

Open Alex1005a opened 3 months ago

Alex1005a commented 3 months ago

Motivation

Currently, using the linear network API, you can close the same socket many times. This could be a problem because a new socket could be created with the same descriptor and we could affect how it works.

The program below will output "Error 2: errno 9" from the problem described. Return code 9 means "Bad file descriptor". This error occurs when using a socket that is already closed.

example2 : LinearIO io => (1 sock : Socket Ready) -> L io ()
example2 sock = do
    sleep 2
    (Nothing # sock) <- bind sock Nothing 1111
        | (Just err # sock) => do
            printLn "Error 3: errno \{show err}"
            done sock
    sleep 3
    (Nothing # sock) <- listen sock
        | (Just err # sock) => do
            printLn "Error 2: errno \{show err}"
            done sock
    close sock >>= done

example1 : LinearIO io => (1 sock : Socket Ready) -> L io ()
example1 sock = do
    (Nothing # sock) <- bind sock Nothing 1111
        | (Just err # sock) => do
            printLn "Error 1: errno \{show err}"
            done sock
    sock <- close sock
    sleep 4
    close sock >>= done

main : IO ()
main = do
    th1 <- fork $ run $ newSocket AF_INET Stream 0
        example1
        (\err => pure ())
    th2 <- fork $ run $ newSocket AF_INET Stream 0
        example2
        (\err => pure ())
    threadWait th1
    threadWait th2
    pure ()

The proposal

In Control.Linear.Network:

  1. Remove the Closed state
  2. Remove done function
  3. Сhange close function and all functions returning Socket Closed

The result will be a similar API as in the article Linear Haskell and ATS.

Alternatives considered

You can impose a constraint on the state of the socket in the close function as in this Haskell library. This fixes the problem, but it's more complicated and makes less sense since there's hardly any use for a closed socket handle.