419593 (17) [Avatar] Offline
When checking the types described in Listing 15.1 on my system I discovered a mismatch in the type of spawn.

  • - Listing 15.1 mentions a type being spawn : (process : IO ()) -> IO (Maybe PID)
    - My instance of Idris Version 0.12.3 returns the type

  • *AdderChannel> :doc spawn
    System.Concurrency.Channels.spawn : (process : IO ()) -> IO PID
        Spawn a process in a new thread, returning the process ID
        The function is Total

    As a result the rest of the listings in chapter 15 have the same mismatch as does the accompanying source files.

    In hindsight it seems obvious, but it looks like this is a Idris-0.12.3 specific issue which has already been solved in the source code, See: Idris GitHub - Fix 'spawn' to return Maybe PID
    Edwin Brady (65) [Avatar] Offline
    Ah, sorry, this is a correction I've recently made to spawn following a comment made by a reviewer, and I expected the release of Idris (which is imminent) to beat the release of the updated chapter. Spawn really needs to return Maybe PID because spawning a process could fail if there's not enough resources.

    There'll be a new release of Idris in the next day or so which fixes this.
    419593 (17) [Avatar] Offline
    Nice. I will update to the new release when its available.

    As a side-note. I bumped into this issue because I am stepping through chapter 15 line by line as it seems to ramp-up in difficulty a bit to much for me (an old C programmer). To many new things going on a the same time. Loving it tough. Can't wait to get my hands dirty, taking it for a spin.