Consider Different Structure

[superfunc]

Transferring a nice sugg from @gallais on reddit to here:

Wouldn't it make sense to store the path as:

• a starting point (i.e. whether it's relative or absolute)
• a list of directory names
• (possibly) a file name and (possibly) an extension rather than a sum type of strings? In other words: expose the structure rather than storing validated raw data.

[superfunc]

Just to write a sketch here for myself later, this would look something like:

data PathRoot = Absolute | Relative String
type PathSegments = List String
type FileBaseName = String
type FileExtensionName = String

data Path = MkPath PathRoot PathSegments (Maybe FileBaseName) (Maybe FileExtensionName)

[gallais]

I meant something more akin to this (because having an extension without a basename does not make sense AFAIK):

data Path = MkPath PathRoot PathSegments (Maybe (FileBaseName, Maybe FileExtensionName))

But you can have multiple extensions (e.g. .tar.gz) so maybe the right thing is (using a record to get projection functions):

record Path where
  constructor MkPath
  pathRoot      : PathRoot
  pathSegments  : PathSegments
  pathMaybeFile : Maybe (FileBaseName, List FileExtensionName)

Might be worth factoring out File too which gives us:

data PathRoot = Absolute | Relative String
PathSegments : Type
PathSegments = List String
FileBaseName : Type
FileBaseName = String
FileExtensionName : Type
FileExtensionName = String

record FileName where
  constructor MkFileName
  fileBaseName   : FileBaseName
  fileExtensions : List FileExtensionName

record Path where
  constructor MkPath
  pathRoot      : PathRoot
  pathSegments  : PathSegments
  pathMaybeFile : Maybe FileName

[superfunc]

Ah, that makes sense, thanks for the detailed reply! My initial concern(I'm not sure why) was losing the ability to pattern match on the absoluteness and such, but I don't think this approach loses any of that. With that said, the general form of the API would stay the same, type sigs & implementations aside. Will do some exploring.