FileRead

eff FileReadSource

An effect used to read from the file system.

All operations on this effect are infalliable. If an operation fails the handler must deal with it.

Operations

def accessTime(f: String): Int64 Source

Returns the last access time of the given file f in milliseconds since the epoch.

def creationTime(f: String): Int64 Source

Returns the creation time of the given file f in milliseconds since the epoch.

def exists(f: String): Bool Source

Returns true if the given file f exists.

def isDirectory(f: String): Bool Source

Returns true is the given file f is a directory.

def isExecutable(f: String): Bool Source

Returns true if the given file f is executable.

def isReadable(f: String): Bool Source

Returns true if the given file f is readable.

def isRegularFile(f: String): Bool Source

Returns true if the given file f is a regular file.

def isWritable(f: String): Bool Source

Returns true if the given file f is writable.

def list(f: String): List[String] Source

Returns a list with the names of all files and directories in the given directory d.

def modificationTime(f: String): Int64 Source

Returns the last-modified timestamp of the given file f in milliseconds since the epoch.

def read(f: String): String Source

Returns a string of all lines in the given file f.

def readBytes(f: String): Vector[Int8] Source

Returns a vector of all the bytes in the given file f.

def readLines(f: String): List[String] Source

Returns a list of all lines in the given file f.

def size(f: String): Int64 Source

Returns the size of the given file f in bytes.

Definitions

def handle(f: a -> b \ ef): a -> Result[IoError, b] \ (ef & (~FileRead)) + IO Source

Handles the FileRead effect of the given function f.

In other words, re-interprets the FileRead effect using the IO effect.