Path

Path: lexical file paths, with no filesystem in sight.

A Path is a list of components and a flag saying whether it starts at the root. Every operation here is pure: none of them asks the host whether a path exists, what a symlink points at, or what the current directory is. Those are filesystem questions and belong to a capability, not to a value.

Parsing normalizes only what is lexically certain. Repeated separators, a trailing separator, and . components carry no meaning, so they are dropped and "a//./b/" is the same path as "a/b". A .. component is kept as it is, because erasing it together with the component before it is only right when that component is not a symlink, and nothing here can know. For the same reason parent refuses a path whose last component is .. rather than guessing.

Paths combine with </>: dir </> name is name inside dir. The operator groups to the left, so root() </> etc </> hosts builds outward from the root, and an absolute right side replaces what is on its left, since it is already anchored. With the empty relative path as identity this makes Path a monoid, and the module gives it the Semigroup and Monoid instances.

The host boundary is UTF-8. A Path is built from a String, so a name the host spells in bytes that are not valid UTF-8 cannot be written down here at all; path fails on the one string a host can never accept, one containing a NUL byte, rather than letting it reach a process call and be cut short there.

match path("/usr//local/./bin/") of
  Ok(p) => path_str(p </> relative(["prism"]))
  Err(_) => "invalid"

/usr/local/bin/prism

Types

PathError

type PathError = EmptyPath | ContainsNul deriving (Eq, Show)

Why a string is not a path.

Path

type Path = Path(Bool, List(String))

A lexical path: whether it is rooted, and its components in order.

Instances

pathJoinPath

instance pathJoinPath : PathJoin(Path)

p </> q is join(p, q). The operator groups to the left and binds looser than :: and arithmetic, tighter than comparison.

path_str(root() </> relative(["usr"]) </> relative(["local", "bin"]))

/usr/local/bin

A rooted right operand discards everything on its left:

path_str(relative(["build"]) </> root() </> relative(["tmp"]))

/tmp

semigroupPath

instance semigroupPath : Semigroup(Path)

Joining is associative: components concatenate, and an absolute operand resets the result wherever it falls. No .. is ever collapsed, so the law holds exactly rather than only up to the filesystem.

let a = relative(["a"])
let b = root() </> relative(["b"])
let c = relative(["c"])
path_eq((a </> b) </> c, a </> (b </> c))

true

monoidPath

instance monoidPath : Monoid(Path)

The empty relative path is the identity on both sides. It prints as ..

let p = relative(["docs", "index.md"])
path_eq(mappend(mempty(), p), p) && path_eq(mappend(p, mempty()), p)

true

Functions and Values

path

path : (String) -> Result(Path.Path, Path.PathError)

Parse a path, normalizing it lexically. Fails on the empty string, which names nothing, and on a string containing a NUL byte, which no host accepts.

match path("a//b/./c/") of
  Ok(p) => path_str(p)
  Err(_) => "invalid"

a/b/c

relative

relative : (List(String)) -> Path.Path

A relative path from components, each of which must be a single name. Components that are empty, ., or contain a separator or NUL are dropped.

path_str(relative(["src", "main.pr"]))

src/main.pr

root

root : () -> Path.Path

The root directory.

path_str

path_str : (Path.Path) -> String

Render a path for the host. The relative path with no components is ..

is_absolute

is_absolute : (Path.Path) -> Bool

Is the path rooted?

components

components : (Path.Path) -> List(String)

The components, in order. The root is not a component.

join

join : (Path.Path, Path.Path) -> Path.Path

q relative to p, the function behind p </> q. An absolute q is already anchored, so it is the answer as it stands.

path_str(join(relative(["src"]), relative(["main.pr"])))

src/main.pr

parent

parent : (Path.Path) -> Option(Path.Path)

The path one component up, or None when that is not lexically known: at the root, at the empty relative path, and after a ...

match path("/a/b") of
  Ok(p) => map_option(path_str, parent(p))
  Err(_) => None

Some(/a)

file_name

file_name : (Path.Path) -> Option(String)

The last component, unless it is .. or there is none.

extension

extension : (Path.Path) -> Option(String)

The file name after its last .. A name with no dot, a dot only in first position (a hidden file), or a dot only in last position has none.

match path("dist/prism.tar.gz") of
  Ok(p) => extension(p)
  Err(_) => None

Some(gz)

stem

stem : (Path.Path) -> Option(String)

The file name before its extension.

path_eq

path_eq : (Path.Path, Path.Path) -> Bool

Equality of paths is equality of their lexical forms.