Writing Files in Idris

Here’s the translation of the Go code to Idris, formatted in Markdown suitable for Hugo:

Our first example demonstrates writing files in Idris. Writing files in Idris follows similar patterns to the ones we use for reading.

import System.File
import Data.String

-- Helper function to handle errors
check : Either FileError a -> IO a
check (Left err) = putStrLn ("Error: " ++ show err) >> exitFailure
check (Right val) = pure val

main : IO ()
main = do
    -- To start, here's how to dump a string into a file.
    let content = "hello\nidris\n"
    Right () <- writeFile "/tmp/dat1" content
        | Left err => putStrLn $ "Error writing file: " ++ show err

    -- For more granular writes, open a file for writing.
    Right file <- openFile "/tmp/dat2" WriteTruncate
        | Left err => putStrLn $ "Error opening file: " ++ show err

    -- Write byte slices
    let bytes = [115, 111, 109, 101, 10]
    Right n <- fWrite file (pack $ map cast bytes)
        | Left err => putStrLn $ "Error writing bytes: " ++ show err
    putStrLn $ "Wrote " ++ show n ++ " bytes"

    -- Write a string
    Right n <- fWrite file "writes\n"
        | Left err => putStrLn $ "Error writing string: " ++ show err
    putStrLn $ "Wrote " ++ show n ++ " bytes"

    -- Idris doesn't have a direct equivalent to bufio,
    -- but we can simulate buffered writing by accumulating strings
    let bufferedContent = "buffered\n"
    Right n <- fWrite file bufferedContent
        | Left err => putStrLn $ "Error writing buffered content: " ++ show err
    putStrLn $ "Wrote " ++ show n ++ " bytes"

    -- Close the file
    closeFile file

    putStrLn "File writing complete"

To run the file-writing code:

$ idris -o writing-files writing-files.idr
$ ./writing-files
Wrote 5 bytes
Wrote 7 bytes
Wrote 9 bytes
File writing complete

Then check the contents of the written files:

$ cat /tmp/dat1
hello
idris
$ cat /tmp/dat2
some
writes
buffered

In this Idris version:

We use the System.File module for file operations.
Error handling is done using Either type, with a check helper function.
We open files using openFile and close them with closeFile.
Writing is done with fWrite, which works for both byte slices and strings.
Idris doesn’t have a direct equivalent to Go’s bufio, so we simulate buffered writing by accumulating strings.
File permissions are not explicitly set in this example, as Idris file operations typically use default permissions.

Note that Idris’s approach to IO and error handling is more explicit and type-safe compared to Go, reflecting its functional programming paradigm.

Random Numbers in Idris

Number Parsing in Idris

Learn X By Example

Title here

Writing Files in Idris