Path.lhs

\documentclass{article}
%include polycode.fmt
\begin{document}

> {-# LANGUAGE DeriveDataTypeable #-}
> {-# LANGUAGE EmptyDataDecls #-}
> {-# LANGUAGE QuasiQuotes #-}
> {-# LANGUAGE TemplateHaskell #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE UndecidableInstances #-}
> {-# LANGUAGE AllowAmbiguousTypes #-}
> {-# LANGUAGE TypeInType #-}
> module Path where

> import Data.Maybe
> import Data.Typeable
> import GHC.TypeLits (ErrorMessage(..), TypeError)
> import System.Directory


In this module we want to create a Path type that is
a wrapper around FilePath and gives additional guarantees.

We could start with the definition:

> {-
> data Path = Path FilePath
>          deriving (Show, Eq, Ord)
> -}

However, this doesn't allow us to encode additional information yet.
We would like to know if a Path is relative or absolute and maybe
if it is a filename even. This will allow to make some
operations impossible on type level, such as concatenating
two absolute paths, which has surprising behavior in System.FilePath.

This looks like a good idea:

> data Path a = Path FilePath
>            deriving (Show, Eq, Ord, Typeable)

We then create 3 empty data type declarations:

> data Abs
> data Rel
> data Fn

In order to construct a 'Path Abs' etc. we need smart constructors:

> parseAbs :: FilePath -> Maybe (Path Abs)
> parseAbs = pure . Path -- simplified
> parseRel :: FilePath -> Maybe (Path Rel)
> parseRel = pure . Path
> parseFn :: FilePath -> Maybe (Path Fn)
> parseFn = pure . Path

Then we create a function to concatenate Paths:

> {-
> (</>) :: Path b -> Path r -> Path b
> -}

This still allows to concatenate two absolute Paths. Maybe we would be
able to express this with a class:

> {-
> class Relative a
> instance Relative Rel
> instance Relative Fn
>
> (</>) :: Relative r => Path b -> Path r -> Path b
> -}

This would be possible. But then we could concatenate two filenames
and would get a filename as a result, which is wrong!

Here's an attempt to introduce type families to fix the problem:

> type family Append k l :: * where
>   Append Abs Rel = Abs
>   Append Abs Fn  = Abs
>   Append Rel Rel = Rel
>   Append Rel Fn  = Rel
>   Append Fn Rel  = Rel
>   Append Fn Fn   = Rel
>   Append k l = TypeError ('ShowType k
>                           ':<>: 'Text " cannot be appended with "
>                           ':<>: 'ShowType l)

And the concatenation function would be:

> (</>) :: Path b -> Path r -> Path (Append b r)
> (</>) (Path a) (Path b) = Path (a ++ b) -- simplified

Indeed, doing

> -- parseAbs "/foo" >>= \p1 -> parseAbs "/bar" >>= \p2 -> Just (p1 </> p2)

yields

error:
    • Abs cannot be appended with Abs
    • When checking the inferred type
        it :: Maybe (Path (TypeError ...))

But since the type is still polymorhpic, we can get into trouble easily.

> getDirsFiles :: Path b        -- ^ dir to read
>              -> IO [Path (Append b Fn)]
> getDirsFiles p@(Path fp) = do
>   contents <- listDirectory fp
>   let parsedContents = catMaybes $ fmap parseFn contents
>   pure $ fmap (p </>) parsedContents

And indeed, this seems to work:
*Path> :t getDirsFiles (fromJust (parseAbs "/home"))
getDirsFiles (fromJust (parseAbs "/home")) :: IO [Path Abs]

However, this also works:
*Path> :t getDirsFiles (Path "/home")
getDirsFiles (Path "/home") :: IO [Path (Append b Fn)]

And unfortunately, we can construct values that way.