In this post, we’ll be crossing the type/value barrier. If stuff like encoding path to a directory in a type doesn’t scare you to death, read on!

In the previous post, we saw how to make the Glorious Glasgow Haskell compiler (GHC) check we don’t lie about the side effects of our function. The specification of the function was

makeFileWriter :: FilePath -> FileWriter
type FileWriter =
  Eff (StateC Integer (Eff (TraceByPrintingC (Eff (LiftC IO)))))
()

What I don’t like about the specification is that it’s far too general. It only tells us there is some fiddling with an integer variable under the hood, some printing to the console, and some I/O. Whether we print “Hello, world!” or a credit card PIN, whether we write an empty text file to the disk or delete the entire disk, the type is the same.

Refining the type

We might want, at least, to encode in the type the directory affected by our side effects. To this end, let’s wrap the original type of our effectful computation in a new data type parametrized by a symbol representing the directory:

data FileWriter' (dir :: Symbol) = FileWriter' {stripDir :: FileWriter}

This way, we effectively tag the computation with the directory it is constrained to. Since we’ve promoted the directory from the value level to the type level, we no longer need to pass it to makeFileWriter and we are left with the following specification:

fileWriter' :: forall dir. KnownSymbol dir => FileWriter' dir

In words, for any particular symbol, fileWriter' is our effectful computation constrained to the directory represented by that symbol. Incidentally, to let us know that we are revving it up, GHC starts throwing errors on us; we need to change gear by activating some of its many extensions:

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

Crossing the type/value barrier

Now, how on Earth are we going to grab the directory from the type and pass it as an argument to the I/O function? Rest assured that Haskell has a trick or two up its sleeve. We just need to pull it in from the standard library:

import Data.Proxy (Proxy (Proxy))
import GHC.TypeLits (Symbol, KnownSymbol, symbolVal)

Behold, the magic:

fileWriter' :: forall dir. KnownSymbol dir => FileWriter' dir
fileWriter' =
  FileWriter' $ makeFileWriter (symbolVal (Proxy :: Proxy dir))

The symbolVal (Proxy :: Proxy dir) trickery does the heavy lifting of converting the type-level directory symbol to a plain String value which is then passed to our good old makeFileWriter function. Finally, the returned FileWriter value is wrapped in FileWriter' dir. To run the FileWriter' dir computation, we strip it of the directory tag and run the resulting FileWriter computation using the original writeFiles function:

writeFiles' :: forall dir. KnownSymbol dir => FileWriter' dir -> IO ()
writeFiles' = writeFiles . stripDir

writeFiles' (fileWriter' :: FileWriter' "test/data")

Conclusion

Whew! I must say forcing Haskell to do these crazy things feels like trying to overtake an Audi A6 3.0 TDI with my Lancer 1.6 MIVEC at 180 kmph on a highway. I’m seriously pushing it to the limits. Damn it, in the next post, we are going for the Evo of programming languages: Clojure!