
In this post, we will be unifying the types in the expression `fmap . fmap`.

The reason for this exercise is that we want to show that our **informal** algorithm for works _so far_.

In a subsequent post, we will be using the results of this exercise to show where our informal algorithm falls short, and extend it to fix this shortcoming.

## Informal Algorithm

As a reminder, our informal algorithm for type unification goes something like this:

1. Rearrange the expression to make it obvious to spot the function applications
2. Gather the types of the **function application** - remember, we only deal with **one application** at a time
3. Ensure that the **type variable names are unique** between function and argument - renaming if necessary
4. Line up the types to figure out the equalities between type variables
5. Erase the argument from the function, replacing type variables and adding in constraints

## The type of `fmap . fmap`

Let's see how well this algorithm works on the expression `fmap . fmap`.

### Step #1 - Rearrange Expression

We will re-arrange the expression to make the application of functions to arguments obvious. In our case `fmap . fmap` is equivalent to `(.) fmap fmap`.

### Step #2 - Gather types of the application

Now that we can clearly spot the two arguments to `(.)`, let's gather the types:

```text 
(.) :: (b -> c) -> (a -> b) -> a -> c

fmap :: Functor f => (a -> b) -> f a -> f b
```

### Step 3 - Ensure Unique Type Variable Names

We can see that the type variable names `a` and `b` are re-used, so let's rename those in `fmap`

```text
(.) :: (b -> c) -> (a -> b) -> a -> c

fmap :: Functor f => (d -> e) -> f d -> f e
```

### Step 4 - Line Up the types

```text
(.) :: (b -> c) -> (a -> b) -> a -> c

fmap :: Functor f => (d -> e) -> f d -> f e
```

Our goal is to unify `b -> c` with `(d -> e) -> f d -> f e`.

Remember that the function type constructor is right-associative. If we take advantage of this fact, we can re-write fmap's signature as: `(d -> e) -> (f d -> f e)`. This leads us to unify as follows:

`b ~ (d -> e)`
`c ~ (f d -> f e)`

### Step 5 - Erase the argument

```text

1 -- (.) fmap :: (a -> b) -> a -> c

b ~ (d -> e)
c ~ (f d -> f e)

2 -- (.) fmap :: (a -> (d -> e)) -> a -> (f d -> f e)

3 -- (.) fmap :: Functor f => (a -> d -> e) -> a -> f d -> f e
```

### Second Application

Now that we've figured out the type of `(.) fmap`, we can rinse and repease:

```text
(.) fmap :: Functor f => (a -> d -> e) -> a -> f d -> f e

fmap :: Functor f => (a -> b) -> f a -> f b

-- Ensure unique type variables
fmap :: Functor g => (c -> b) -> g c -> g b


-- Unify (a -> d -> e) with (c -> b) -> g c -> g b
a ~ (c -> b)
d ~ g c
e ~ g b

-- Erase the first argument
(.) fmap fmap :: a -> f d -> f e

-- Replace type variables, add in constraints
(.) fmap fmap :: (Functor f, Functor g) => (c -> b) -> f (g c) -> f (g b)
```


The type of (fmap . fmap)


I recently ran into a type error at work involving a monad transformer stack
with multiple `Reader` monads and multiple environments. I have distilled the
problem to its essential components below:

```haskell
#!/usr/bin/env stack
-- stack --resolver lts-18.2 exec ghci --package mtl

{-# LANGUAGE FlexibleContexts #-}


import           Control.Monad.Reader

firstReader :: MonadReader env m => Int -> SqlPersistT m ()
firstReader i = do
  _   <- secondReader -- run a computation

  env <- lift ask -- get the `env` 

  -- more work using the `env` environment

  pure ()

secondReader :: MonadReader Int m => SqlPersistT m ()
secondReader = undefined

-- Note: This is a dummy type synonym, but it motivates the reason for the
-- multiple Reader monads.
type SqlPersistT = ReaderT Char
```

The idea here is that we are in a monad - `SqlPersistT` - which can perform
database actions. That monad  and that is stacked upon another monad that
requires its own environment.

If we run the script above, we will get a type error that boils down to `env`
does not match `Int`. Let's try to figure out how we ended up with this type
error.

## Unifying the Types

It is always good exercise to try to determine how GHC is arriving at a
particular type error. We can re-write `firstReader`:

```haskell
firstReader :: MonadReader env m => Int -> SqlPersistT m ()
firstReader i =
  secondReader
    >> (do
         env <- lift ask
         pure ()
       )
```

And then, we can convert from infix notation to prefix:

```haskell
firstReader :: MonadReader env m => Int -> SqlPersistT m ()
firstReader i = (>>)
  secondReader
  (do
    env <- lift ask
    pure ()
  )
```

The lexical order of the expression now mirrors order in which expression are
being applied. We can now proceed to the unification of the types.

One of the most important rules regarding type unification exercises is that we
want to **apply an expression to a single argument at a time**. This is simply
how Haskell works (remember, all functions are curried), and it has the
enormously beneficial consequence that we only have to think of two expressions
at a time. In our case, we want to apply `>> :: m a -> m b -> m b` to
`secondReader :: MonadReader Int m => SqlPersistT m ()`.

```haskell
>> :: m a -> m b -> m b

secondReader :: MonadReader Int m => SqlPersistT m ()
```

Another important rule of type unfication exercises is that we want to use
**unique type variables** among the two expressions that we are comparing. For
example, because both `>>` and `secondReader` use the `m` type variable name,
we will have to change one of them to something these:

```haskell
>> :: m a -> m b -> m b

secondReader :: MonadReader Int m0 => SqlPersistT m0 ()
```

Now, we can proceed to match `m a ` to `SqlPersistT m0 ()`. In other words, if
`m a ~ SqlPersistT m0 ()`, that implies that `m ~ SqlPersistT m0` and `a ~ ()`.
We can remove the firt argument to `>>`, and then replace the resulting type
signature with that information:

```haskell
-- Remove the first argument in the type signature to `>>`
>> secondReader :: m b -> m b

-- Replace m ~ SqlPersistT m0
-- Replace a ~ ()
>> secondReader :: SqlPersistT m0 b -> SqlPersistT m0 b

-- Add constraints that we know about:
>> secondReader :: MonadReader Int m0 => SqlPersistT m0 b -> SqlPersistT m0 b
```

Now, let's apply `>> secondReader` to the `do` expression. Here, we can take a
shortcut to figure out the type of the `do` expression. We know that `pure () ~
SqlPersistT m ()`, and that that will be the type of the entire `do` expression.

```haskell
>> secondReader :: MonadReader Int m0 => SqlPersistT m0 b -> SqlPersistT m0 b

<do expression> :: MonadReader env m => SqlPersistT m ()
```

`SqlPersistT m0 b ~ SqlPersistT m ()` implies that `SqlPersistT ~ SqlPersistT`,
`m0 ~ m` and `b ~ ()`. Again, we can get rid of an argument to `>>
secondReader`, and then replace the type variable left with the information we
know.

```haskell
-- Remove the first argument to the type signature `>> secondReader`
>> secondReader <do expression> :: MonadReader Int m0 => SqlPersistT m0 b

-- Replace `m0` with `m`
-- Replace `b` with `()`
>> secondReader <do expression> :: MonadReader Int m => SqlPersistT m ()

-- Add constraints we know about:
>> secondReader <do expression> :: (MonadReader env m, MonadReader Int m) => SqlPersistT m ()
```

Now, we can clearly see our type error. The first constraint `MonadReader env
m` disagres with `MonadReader Int m`. Let's look at the head of the
`MonadReader` type class declaration:

```haskell
class Monad m => MonadReader r m | m -> r where
```

The first constraint is saying that the `m` will resolve the `r` to `env`, and
the second constraint is saying that the `m` will resolve the `r` to `Int`. Our
two constraints disagree with one another.

## runReader

With that diversion into a type unfication exercise done, we can continue on how to define `firstReader` in terms of `secondReader`. `firstReader` has an `Int` in scope, which we want to use as the environment for `secondReader`. We can do this by using `runReaderT` to satisfy the `MonadReader` constraint:

```haskell
firstReader :: MonadReader env m => Int -> SqlPersistT m ()
firstReader i = do
  backend <- ask
  _ <- runReaderT (runReaderT secondReader backend) i

  pure ()
```

Why does the above compile? Well, remember that `secondReader` is a monad
transformer stack, where the first transformer is `ReaderT`. We can "peel this
transformer off" using `runReaderT`. Critically, the value that we are left
with has the type `MonadReader Int env`, which we can also peel off using
`runReaderT`!

## Using mapReaderT

The above solution is perfectly valid, but there is a more idiomatic solution - `mapReaderT`. As the documentation states, `mapReaderT` allows us to "[t]ransform the computation inside a ReaderT". That's exactly what we are looking for!

```haskell
firstReader :: MonadReader env m => Int -> SqlPersistT m ()
firstReader i = do
  _ <- mapReaderT (\m -> runReaderT m i) secondReader
  pure ()
```

`mapReaderT` is giving us access to the computation inside of `secondReader`,
which has the type `MonadReader Int m => m ()`. Again, we use `runReaderT` to
satisfy the `MonadReader Int m` constraint!

## Conclusion

Given my previous experience with these subjects, this post served to reinforce previously learned lessons.

In terms of **type unification exercises**, there is a simple algorithm that works for me:

1. Re-write the expression into something that is lexically mirrors the order of application
2. Do **one application at a time**
3. Make sure that the type variables in a given application are unique between the two expressions

In terms of dealing with monadic expression:

1. We can "peel off" the outter monadic structure by using the `runX` functions
   for that monad (unless, of course, if we are dealing with `IO`).


Readers on Readers


Type errors are a common source of frustration for new users to Haskell. Truth
be told, depending on the amount of type-level programming involved, type errors
can be inscrutable even to seasoned Haskell programmers.

In this post, we are going to start off with an ill-typed Haskell program, and
explore how different type-level features affect how we eventually get the
program to compile.

## The Ill-Typed Source Code

```haskell
#!/usr/bin/env stack
-- stack --resolver lts-18.2 script

import           Data.Pool            (Pool)
import           Database.Persist.Sql (SqlBackend)
import           Test.Hspec

main :: IO ()
main = hspec spec

spec :: Spec
spec =
  withPool $ do
    describe "insertAdmin" $ do
      it "is successful when email has not been taken" pending

withPool :: SpecWith SqlPool -> Spec
withPool = undefined

type SqlPool = Pool SqlBackend
```

## The Type Error

The file above is a Haskell Script[^1], and it contains the following type error:

```text
• Couldn't match type ‘()’ with ‘Pool SqlBackend’
  Expected type: SpecWith SqlPool
    Actual type: SpecWith (Arg Expectation)
• In a stmt of a 'do' block:
    it "is successful when email has not been taken" pending
  In the second argument of ‘($)’, namely
    ‘do it "is successful when email has not been taken" pending’
  In a stmt of a 'do' block:
    describe "insertAdmin"
      $ do it "is successful when email has not been taken" pending
```

## What Went Wrong

At a simplified level, we can GHC's job as making sure that our "types line up".
If a function expects a value of type `Int`, and we are applying it to a value
of type `Bool`, GHC will detect that the *types do not line up*. This will
result in a type error.

In this particular case, GCH is information us that there are two types that do
not line up:

1. On the first line of the error message, we can see that the type `()` is not
   the same as the type `Pool SqlBackend`.

2. On the second and third lines of the error message, GHC could not match the
   type `SpecWith SqlPool` with `SpecWith (Arg Expectation)`. Because `SqlPool`
   is a type alias for `Pool SqlBackend`, we substitute `Pool SqlBackend` for
   `SqlPool`. Therefore, we will consider the second line of the error message
   to reference `Pool SqlBackend`[^2].

Where did we expect the type `SpecWith SqlPool`, and why? Though a tad
convoluted, the error message does eventually point us to the argument to
`withPool`. The argument - spanning from the `describe` to the `pending` - has
the type `SpecWith ()`, and *that* is clearly not the same as `SpecWith
SqlPool`.

## Where Did `()` Come From?

Despite the fact that the expression `describe ...` has the wrong type, it was
not wholly wrong, in the sense that the type constructor did match. A graphical
example might be more... illustrative:

```markdown
|          | Type Constructor | Type            |
|----------|------------------|-----------------|
| Expected | SpecWith         | Pool SqlBackend |
| Actual   | SpecWith         | Arg Expectation |
```


Notice how the type constructor - i.e. `SpecWith` - of the expected type **is**
the same as the type constructor of the actual type. What didn't match was
`SqlPool` with `Arg Expectation`. Not only can we *see* that the type
constructor matched in our table above, but GHC told us as much in the first
line of the error message, which, importantly *doesn't* mention the type
constructor `SpecWith`.

However, a mystery arises here. If the types that failed to match are `Pool
SqlBackend` with `Arg Expectation`, why does the first line of the error message
compare `Pool SqlBackend` to `()`? Shouldn't the failure read, instead,
`Couldn't match type ‘Arg Expectation’ with ‘Pool SqlBackend’`?

## Type Families

The reason for this seeming inconsistentcy is that `Arg` is a type family[^3].
This means that it is a type-level function from one type to another. In our
program, we applied the type `Expectation` to the type family `Arg`, and the
*instance* of `Arg` for `Expectation` is in fact `()`[^4]:

```haskell
type Arg Expectation = ()
```

## Solving Our Type Error

Let's recap what we know so far:

1. The `describe ...` expression is reducing to the type `SpecWith ()`.
2. The `withPool` function expects the type `SpecWith (Pool SqlBackend)`.
3. The type family `Arg Expectation` reduces to `()`.
4. `Arg Expectation` is not `Pool SqlBackend`

Here, we can pursue two lines of inquiry. First, we can investigate the
`describe ...` expression to figure out why it reduced to `SpecWith ()`.

Secondly, we can try to find an instance of `Arg` that reduces to `Pool
SqlBackend`.

Note: It is important to point out here that we are assuming that the type
signature of `withPool` is correct. Our error would be gone if we changed
`withPool :: SpecWith () -> Spec`. However, we are assuming that, in a
real-world scenario, what `withPool` does with the `SpecWith SqlPool` value
would mean that there is no other type signature possible.

Let's start with `describe`.

### `describe`

`describe` has the the type:

```haskell
describe :: HasCallStack => String -> SpecWith a -> SpecWith a
```

This type signature tell us that the return type of `describe` is wholly
dependent on the type of its second argument. In our case, that second argument
is `it "is successful when email has not been taken" pending`.

What is the type of `it`?

```haskell
it :: (HasCallStack, Example a) => String -> a -> SpecWith (Arg a)
```

Much like `describe`, the return type of `it` is wholly dependent on the type of
its second argument. In our case, we used `pending`, which has the type
`Expectation`, and which caused the return type of the entire `describe ...`
expression to be `SpecWith (Arg Expectation)` - a.k.a. `SpecWith ()`.

However, this line of inquiry has gotten us very far. Our goal is now to find a
type `a` such that `SpecWith (Arg a)` reduces to `SpecWith (Pool SqlBackend)`.
We know that such a type must have an instance of `Example` because of the
constraint in the type signature of `it`, and because we know that the type
family `Arg` is a associated with the `Example` type class.

Notice that this excursion into what our `describe ...` expression reduced to
led us to the same conclusion we had before. Namely:

> Secondly, we can try to find an instance of `Arg` that reduces to `Pool
> SqlBackend`.

We can argue, convincingly, that it was unneccesary work, but it is very useful
from a pedagogical perspective.

## Reaching Our Goal

At this point, we have boiled down our problem to finding an instance of `Arg`
that reduces to `Pool SqlBackend`.

Unfortunately, I have no general way of finding such an instance. Because `Arg`
is an open type family, such an instance can be defined anywhere. The best I
have come up with is good 'ol `grep`ing of the code base. We have two hooks that
we can search for `instance Example` (again, since `Arg` is an associated type
family) and `type Arg`. This will work if the instance is defined within your
code base, but not if the instance is defined in a library whose source code is
not in your project.

Alas, in our case, it was the former. A library that I was using had the
following instance of `Example`:

```haskell
instance Example (AppExample app a) where
  type Arg (AppExample app a) = app
```

This meant that if I had the type `Arg (AppExample (Pool SqlBackend) a)` would
reduce to `Pool SqlBackend` - exactly what we are looking for. Since
`AppExample app` is also a monad, we can create a value of the correct type by
using the monad interface:

```haskell
#!/usr/bin/env stack
-- stack --resolver lts-18.2 script

import           Data.Pool            (Pool)
import           Database.Persist.Sql (SqlBackend)
import           FrontRow.App.Test
import           Test.Hspec

main :: IO ()
main = hspec spec

spec :: Spec
spec = withPool $ do
  describe "insertAdmin" $ do
    let myPending :: AppExample SqlPool ()
        myPending = pure ()

    it "is successful when email has not been taken" myPending

withPool :: SpecWith SqlPool -> Spec
withPool = undefined

type SqlPool = Pool SqlBackend
```

[^1]: Assuming you've saved this file into `type_error.hs`, you can run the
  script with `stack type_error.hs`.

[^2]: I have changed mentions of `SqlPool` to `Pool SqlBackend`. The former is a
  type synonym for the later, which means that these are two different names for
  the same type. They can be used interchangeably, but when trying to figure out
  why our types don't line up, it is much easier to avoid having to remember
  that these are the same thing, and simply use one name.

[^3]: [Arg](https://www.stackage.org/haddock/lts-18.5/hspec-2.7.10/Test-Hspec.html#t:Arg)

[^4]: `Arg` is an open and an associated type family. The *open* adjective means
  that there is no "master" list of all of the instances of `Arg`. A new
  instance can be defined at any time. The *associated* adjective means that the
  type family is associated with a type class. Looking at the [source
  code](https://github.com/hspec/hspec/blob/e990053f35e1c9f2b0b6dfc13475f657d2eef120/hspec-core/src/Test/Hspec/Core/Example.hs#L45),
  we can see that `Arg` is associated with the `Example` type class.


Solving a Type Error - Couldn't Match Type


There are a multitude of "lenses" with which to view typeclasses in Haskell. We
can view typeclasses *as an interface*; or, we can view typeclasses *as a name
for a set of related types*; or, we can view typeclasses *as a form of
dependency injection*.

In this post, I'd like to talk about viewing a typeclass *as dependency
injection* (on steroids). This is not a new idea, and credit goes to Matt
Parsons's, who first explained this to me in a tractable way in his post,
[Invert Your Mocks!][invert-your-mocks]

## What is Dependency Injection

For our purposes, we'll define dependency injection as *passing behavior* to a
program, as opposed to hard-coding the behavior into the program. For example:

```javascript
// Decrease the cost once, and then increase it twice
function computeCost(costIncrease, costDecrease, startingCost) {
  const decreasedCost = costDecrease(startingCost)

  const increasedCost = costIncrease(decreasedCost)

  return costIncrease(increasedCost)
}
```

In the snippet above, we have passed into the `computeCost` function how to
increase a cost and decrease the cost. The benefit of doing this is that we can
change the behavior of `computeCost` by passing in different arguments. In one
scenario, maybe increasing our cost means adding 5. In another scenario,
increasing our cost means adding 10. Because this behavior can be passed into
our `computeCost` function, we can change the behavior as needed.

Now we know what dependency injection is, as well as why it is useful.

## "Manual" Dependency Injection in Haskell

Let's translate the above function from JavaScript to Haskell:

```haskell
computeCost :: (a -> a) -> (a -> a) -> a
computeCost costIncrease costDecrease startingCost =
  let decreasedCost = costDecrease startingCost
      increasedCost = costIncrease decreasedCost
  in costIncrease increasedCost
```

## Dependency Injection via Typeclasses

Let's now use typeclasses to perform the dependency injection for us. We'll
write out the code first, and then explain what is going on:

```haskell

class TrackCost a where
  costDecrease :: a -> a
  costIncrease :: a -> a

computeCost :: TrackCost a => a -> a
computeCost startingCost =
  let decreasedCost = costDecrease startingCost
      increasedCost = costIncrease decreasedCost
  in costIncrease increasedCost

newtype HighCost = HighCost Int deriving Show

newtype LowCost = LowCost Int deriving Show

instance TrackCost HighCost where
  costDecrease (HighCost currentCost) = HighCost (currentCost + 10)
  costIncrease (HighCost currentCost) = HighCost (currentCost - 5)

instance TrackCost LowCost where
  costDecrease (LowCost currentCost) = LowCost (currentCost + 5)
  costIncrease (LowCost currentCost) = LowCost (currentCost - 2)

main :: IO ()
main = do
  print (computeCost (HighCost 10)) # Will print "HighCost 25"
  print (computeCost (LowCost 10))  # Will print "LowCost 18"
```

Let's first focus on the *behavior* of `computeCost`. Notice that the result of
`main` proves that we have *injected* behavior into `commputeCost`. How? Because
even though we have passed in essentially the same argument - barring the
`newtype` wrapper, in both cases we are passing in `10` - `computeCost` resulted
in a different number - specifically, `25` and `18`.

What happened is that instead of passing in the behavior explicitly via
arguments to `computeCost`, we are passing in the behavior implicitly via
typeclasses. The function that `costDecrease` and `costIncrease` will resolve to
depend on what the type variable `a` is specialized to. In the case of
`HighCost`, `costDecrease` will resolve to a fuction that subtracts `5`, and
`costIncrease` will resolve to a function that adds `10`. You can likely figure
out what `costDecrease` and `costIncrease` will resolve to when the type
variable `a` is specialized to `LowCost`.

## Side Notes

I wrote `computeCost` in such a way as to keep a symmetry between the JavaScript
function. In the wild, you are most likely to see the Haskell version of
`computeCost` written with *function composition* and in *point free* style:

```haskell
computeCost :: (a -> a) -> (a -> a) -> a
computeCost costIncrease costDecrease = costIncrease . costIncrease . costDecrease

computeCost' :: TrackCost a => a -> a
computeCost' = costIncrease . costIncrease . costDecrease
```

[invert-your-mocks]: https://www.parsonsmatt.org/2017/07/27/inverted_mocking.html
[dependency-injection]: https://en.wikipedia.org/wiki/Dependency_injection


Haskell Typeclasses & Dependency Injection


N.B. This post is tagged with [Note](/tags/note), which means that my
understanding of the topic at hand is fluid, subject to change, and I am likely
to update the post time and time again as my understanding matures. The post is
not meant for external consumption - you are likely to find incomplete thoughts
that make sense only to me (or maybe don't make sense at all). Maybe one day my
understanding will advance to the point where I can delete the note tag.

## GADTs

Generalized Algebraic Data Types have a fairly intimidating name. Luckily, like
most terminology, it is only intimidating because it is new. As soon as we start
unpacking the reason for that name, this start to be less intimidating. So let's
get started.

What the "Generalized" word in GADTs means is that we generalize over the
**return type** of the data constructors for a data type. Let's compare a data
declaration that uses GADTs and one that doesn't, so that we may see this
"generalization on the return type" in action:

```haskell
-- Not GADTs
data AType a = ATypeNullaryDataConstructor | ATypeUnaryDataConstructor a

-- GADTs
data MyType a where
  MyTypeNullaryDataConstructor :: MyType Int
  MyTypeUnaryDataConstructor :: a -> MyType a
```

In the declaration for `AType`, once the type variable `a` has been initialized,
then every data constructor for `AType` will have the same return type. For
example, in the case when `a ~ Int`, `ATypeNullaryDataConstructor` and
`ATypeUnaryDataConstructor` must have the return type `AType Int`. The key here
is to focus on the return type. The data constructors must return the same type
once `a` has been initialized.

But what about `MyType`? Again, the key is the return type of the data
constructors. They do not have to be the same! If we initialize the type
variable `a` to `Bool`, `MyTypeNullaryDataConstructor` will have the type
`MyType Int`, but **MyTypeUnaryDataConstructor will have the type `MyType
Bool`**. In other words, the return type of the data constructor **depends on
the data constructor itself**, modulo other type information. This is simply not
possible without GADTs In the case of `AType`, the return type of the data
constructors depends not on the data constructors themselves, but on what the
type variable has been initialized to.

## Why Is This Useful?

In the declaration of `MyType`, we focused on how GADTs lift a restriction
imposed (necessarily) by the type system. In practice, GADTs are most useful
when we pair the lifting of one restriction by **the imposition of another**.
Specifically, we can restrict the type of the parameters that the data
constructor accepts. Let's re-write `MyType a` to show an example:

```haskell
data MyType a where
  MyTypeNullaryDataConstructor :: MyType Int
  MyTypeNullaryDataConstructor :: Bool -> MyType Bool
```

Notice how, in this new declaration of `MyType`, we are still making use of the
ability for our data constructors to have different return types. In addition,
we are restricting the type of the parameters to which
`MyTypeUnaryDataConstructor` can be applied to. Of course, restricting the type
of the values to which a function can be applied to is no large feat. We do that
all the time in functional programming, and it is the reason d'etre of types to
begin with. Nevertheless, it is clear that one of the guarantees that we get by
restricting the type of the paramters to the data constructors is that if we
have a value of type `MyType Bool`, then we are guaranteed that the data
constructor `MyTypeUnaryDataConstructor` must have been applied to a value of
type `Bool`. But, **with GADTs**, the relationship also holds the other way
around. If we have a value "tagged" with the data constructor
`MyTypeUnaryDataConstructor`, then we are **guaranteed** to be dealing with a
the type `MyType Bool`!. To quote the [GHC User
Guide](https://downloads.haskell.org/ghc/latest/docs/html/users_guide/glasgow_exts.html#generalised-algebraic-data-types-gadts):

*The key point about GADTs is that pattern matching causes type refinement.*

```haskell
patternMatch :: MyType a -> a
patternMatch (MyTypeUnaryDataConstructor b) = b
```

In the above code, by inference, the compiler initializes `a` to `Bool` **if**
the `MyTypeUnaryDataConstructor` pattern matches!

And just to round out the discussion, let's explore why it is impossible to
determine the type of a value from its data constructor without GADTs:

```haskell
data NoGADT a = NoGADT Int

a :: NoGADT Bool
b = NoGADT 5

b :: NoGADT Int
b = NoGADT 5

c :: NoGADT String
b = NoGADT 5
```

Notice that at the value level, we have the exact same data: `NoGADT 5`.
However, in each case, we have a different type - `NoGADT Bool`, `NoGADT Int`,
and `NoGADT String`. This is why, without GADTs, we cannot determine from the
data constructor what the type is. If we can't do it, neither can Haskell's type
system. Now, try to construct a value using the data constructor
`MyTypeUnaryDataConstructor` and have it **not** result in a value of type
`MyType Bool`. It is impossible!

## Information Flow Between Layers

In my post on [phantm types](/posts/phantom_types), I continually emphasized the
importance of understanding how information flows from one layer of the type
system to another. In that post, we learned three things:

1. Information can be encoded at the type layer; one way to do so is with
   **phantom types**
2. **Typeclasses** allow us to translate type-level information to the term layer
3. We can use **type annotations** to send information from the term layer to
   the type layer

GADTs give us a new tool by which to communicate from the term layer to the type
layer. The **data constructors** at the term layer can be used to determine the
type (at the type layer).

The ability of GADTs to convey information from the term layer - via the data
constructors - to the type layer is how they change the game!


## Misc

When writing this post, the ability to send information from the term layer to
the type layer finally dawned on me. What happened was that I was going to
extoll the fact that when we loosen the restriction on the return type and add
restrictions on the type of the parameter to a GADT, we get a guarantee of the
type of the value to which a data constructor was applied. It dawned on me that
this was true even without GADTs, but that GADTs made possible to infer things
the other way around - given a data constructor, we have a guarantee of the
type.


Type-Level Programming In Haskell - GADTs


N.B. This post is tagged with [Note](/tags/note). This means that the post is
**not** meant for external consumption. Instead, it is a "stream of
conciousness" or "scratchpad" as I learn about new topics.

## Terms, Types, and Kinds

One of the foundations of understanding type-level programming in Haskell is the
realization that Haskell's type system divides itself into three **separate**
layers - the *term* layer; the *type* layer; and the *kind* layer.

Just like the terms `a`, `b`, `c` are grouped into the type `Char`, types
themselves are grouped together into something called a kind. The kind of
`Char`, for example, is `*`.

## Bridging Terms, Types, and Kinds

The separation between *terms*, *types*, and *kinds* is foundational for
understanding type-level programming. Type-level programming simply means that
instead of operating on terms, we are going to be operating on types. Types are
useful only to the extent that they inform the behavior of our system at
runtime. Therefore, we must be able to bridge the the term layer and the type
layer. There must be facilities to take information at one layer and have that
impact the other layer.

This idea of passing information between these two layers of the type system is
so commonplace that we might not even be aware of it. For example, let's pass
some information from the term layer to the type layer:

```haskell
Nothing :: Maybe Int
```

Using a *type annotation*, we can tell type system that our `Nothing` data
constructor has the type `Maybe Int`. We are now passing type information from
the term layer to the type layer. As you can imagine, only type information can
be passed into the type layer.

What about passing information from the type layer to the term layer? This is
done via typeclasses! For example, we can think about the instance of `Show
Int` as a function (loosely speaking) going from the type `Int` to the value
`Int -> String`. In the discussion of *phantom types* below, we will see a more
explicit example of using typeclasses to bridge the type and term layers.

## Phantom Types

Let's imagine for a second that we are building the navigation software for a
space craft. We want to make sure that we never mix up our units. A potential
attempt at this might be as follows:

```haskell
data Distance = Miles Double | Kilometers Double

distanceInMiles :: Distance
distanceInMiles = Miles 10

distanceInKilometers :: Distance
distanceInKilometers = Kilometers 10
```

How does this save us from mixing up our units? Well, in order to access the
double, we have to pattern match on the data constructors, making it obvious
what units we are dealing with. But there are two problems here:

0. The **unit information exists only at the term layer** - the type system is
   not aware of it.
0. It becomes increasingly difficult to perform simple operations values of type `Distance a`
0. No guarantees that something untoward won't happen outside of `addDistances`.


To the first point:

```haskell
addDistances :: Distance -> Distance -> Distance
addDistances first second = ...
```

Notice how, at the type layer, we have no information about the units.

To the second point, let's actually implement `addDistances`:

```haskell
addDistances :: Distance -> Distance -> Distance
addDistances (Miles x) (Miles y) = Miles (x + y)
addDistances (Kilometers x) (Kilometers y) = Kilometers (x + y)
addDistances (Miles x) (Kilometers y) = Kilometers (x * 1.60934 + y)
addDistances kilometers miles = addDistances miles kilometers
```

If we add more data constructors to the `Distance` type, we'd be in a mess of
trouble!

Finally, to the third point, we have no guarantee that a client of `Distance`
won't do the following:

```haskell
distanceToDouble :: Distance -> Double
distanceToDouble (Miles x) = x
distanceToDouble (Kilometers y) = y

distanceToDouble (Miles x) + distanceToDouble (Kilometers y)
```

We could always use Haskell's combinator pattern and make `Distance` an absract
data type, but that leads to its own issues.

## Phantom Types

Let's go back to our original problem. We want to create navigation software in
such a way that avoids the mixup of units. We saw a potential solution, where
the unit information was carried along at the term level. This time, let's
enlist the type system to help us ensure we don't mix up our types by encoding
the unit information at the type level. We can do this using **Phantom Types**:

```haskell
data Mile
data Kilometer

newtype Distance a = Distance { unDistance :: Double }
```

Let's pause here to understand what the above code snippet is doing.

First, we are declaring two new data types - `Mile` and `Kilometer`. Notice that
these data types have *no data constructors*. As a result, we cannot create
values of type `Mile` or `Kilometer`.

Secondly, we are creating a new *type constructor* - `Distance`. `Distance`
is parameterized by a type variable. Crucially, because this type variable does
not appear on the right-hand side of the data declaration, the type variable
(`a`) is known as a **phantom type**. In more esoteric terms, you might here
someone say that the type variable has not witness at the term level. What good
is it then? Well, it might be phantom at the value level, but it is alive and
well at the type level! The types `Distance Mile` and `Distance Kilometer` are
two very distinct types. Using phantom types, our type system is now aware that
distance values have units!

## Operating on Distance

Now that we the unit have been promoted to the type level, the compiler can
ensure we don't mix up our units. Let's how we would go about operating on our
`Distance a` values.

Remember that our `Distance` type constructor is just a wrapper around an
underlying value of type `Double`. For "number like" operations, we just want to
unwrap the `Double`, perform the operation, and wrap things up again in our
`Distance` data constructor. We can use `GeneralizedNewtypeDeriving` to have
Haskell derive this exact instance for us:

```haskell
newtype Distance a = Distance { unDistance :: Double } deriving (Num, Show)

a :: Distance Mile
a = Distance 20

b :: Distance Mile
b = Distance 20

a + b
=> Distance { unDistance = 40.0 }
```

However, if we attempt to add two distances with different units, we get a type
error:

```haskell
a :: Distance Mile
a = Distance 20

b :: Distance Kilometer
b = Distance 20

a + b
=> Couldn't match type ‘Kilometer’ with ‘Mile’
```

```haskell
twentyMiles = (Distance 10 :: Distance Mile) + (Distance 10 :: Distance Kilometer)
```

## Working with Information at the Type Level

So we've gained some type safety. The compiler is helping us ensure that we do
not mix up types, and working with distances of the same type is fairly painless
- we rely on the way that `Double`s work.

But what about working with distances with two different units? What if we
wanted to, in fact, add miles and kilometers together? Well, we know we can
write the functions:

```haskell
addMilesToKilometers :: Distance Mile -> Distance Kilometer -> Distance Kilometer
addMilesToKilometers distanceInMiles distanceInKilometers = Distance (unDistance distanceInKilometers + unDistance distanceInMiles 1.60934)

addKilometersToMiles :: Distance Kilometer -> Distance Mile -> Distance Mile
addKilometersToMiles distanceInKilometers distanceInMiles = Distance (unDistance distanceInMiles + unDistance distanceInKilometers * 0.621371)
```

Now, if we have two distances - one in miles and another in kilometers - we know
whether we need to choose `addKilometersToMiles` or `addKilometersToMiles` based
on the information at the type level. As we've said earlier, going for
information from the type level to the term-level requires a typeclass:

```haskell
class Add a b where
  addDistance :: Distance a -> Distance b -> Distance b

instance Add Mile Kilometer where
  addDistance = addMilesToKilometers

instance Add Kilometer Mile where
  addDistance = addKilometersToMiles

instance Add Mile Mile where
  addDistance = +

instance Add Kilometer Kilometer where
  addDistance = +
```

## Lessons for the Novice Type-Level Programmer

The code snippet above contains a multitude of tidbits for the novice type-level
programmer. Let's start with the typeclass declaration:

```haskell
class Add a b where
  addDistance :: Distance a -> Distance b -> Distance b
```

Notice how we apply the type variable `a` and `b` to the `Distance` type
constructor in our declaration of the typeclass. Thus, even though `Distance`
does not appear anywhere in our typeclass declaration's head, we can only call
`addDistance` to values of type `Distance`. Remember, we need to decide between
using `addMilesToKilometers` or `addKilometersToMiles`. The only information we
need to make this choice is the units of the two distance values we are adding.
And that is precisely the information that our `Add` class is "asking" for.

Now, let's at one of our instance declarations:

```haskell
instance Add Mile Kilometer where
  addDistance = addMilesToKilometers
```

Notice how the typeclass instance is used to go from type level information -
the units of the distances that we are adding - to term level information,
namely, a function from two distances (mile and kilometer) to a single distance
in kilometers.

## What Have We Gained

Our first declaration of `Distance` was conceptually simple, fairly type-safe,
but hard to work with and hard to extend.

Our "phantom type" version of distance was conceptually more complex, just as
type-safe, and we didn't sacrifice much in the way of ergonomics:

```haskell
let tenMiles = Distance 10 :: Distance Mile
let tenKilometers = Distance 10 :: Distance Kilometer

addDistance tenMiles tenMiles
=> Distance {unDistance = 20.0} :: Distance Mile

addDistance tenKilometers tenKilometers
=> Distance {unDistance = 20.0} :: Distance Kilometer

addDistance tenMiles tenKilometers
=> Distance {unDistance = 26.0934} :: Distance Kilometer

addDistance tenKilometers tenMiles
=> Distance {unDistance = 16.21371} :: Distance Mile
```

## Complete Module

The code snippet below is a complete module of the lessons learned here. Notice
that we declare a `Convert` typeclass that lets us convert from miles to
kilometers or kilometers to miles. If you load this module in GHCI, you can run
the `main` action and see the tests pass (hopefully!).

```haskell
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module IntroToTypeLevelProgramming.PhantomTypes where

import           Test.Hspec

newtype Distance a = Distance { unDistance :: Double } deriving (Eq, Show, Num)

data Mile

data Kilometer

milesToKilometers :: Distance Mile -> Distance Kilometer
milesToKilometers distanceInMiles = Distance (unDistance distanceInMiles * 1.60934)

kilometersToMiles :: Distance Kilometer -> Distance Mile
kilometersToMiles distanceInKilometers = Distance (unDistance distanceInKilometers * 0.621371)

class Convert a b where
  convert :: Distance a -> Distance b

-- instance Convert (Distance Mile) (Distance Kilometer); we'd be passing
instance Convert Mile Kilometer where
  convert = milesToKilometers

instance Convert Kilometer Mile where
  convert = kilometersToMiles

class Add a b where
  addDistance :: Distance a -> Distance b -> Distance b

instance Add Mile Kilometer where
  addDistance distanceInMiles distanceInKilometers = convert distanceInMiles + distanceInKilometers

instance Add Kilometer Mile where
  addDistance distanceInKilometers distanceInMiles = convert distanceInKilometers + distanceInMiles

instance Add Mile Mile where
  addDistance = (+)

instance Add Kilometer Kilometer where
  addDistance = (+)

main :: IO ()
main = hspec $ do
  it "converts from miles to kilometers" $ do
    let distanceInMiles = Distance 10 :: Distance Mile
    (convert distanceInMiles :: Distance Kilometer) `shouldBe` Distance 16.0934
  it "converts from kilometers to miles" $ do
    let distainceInKilometers = Distance 10 :: Distance Kilometer
    (convert distainceInKilometers :: Distance Mile) `shouldBe` Distance 6.21371
  it "can add miles to kilometers" $ do
    let distanceInKilometers = Distance 10 :: Distance Kilometer
        distanceInMiles = Distance 10 :: Distance Mile
    (addDistance distanceInMiles distanceInKilometers) `shouldBe` (Distance 26.0934 :: Distance Kilometer)
  it "can add kilometers to miles" $ do
    let distanceInKilometers = Distance 10 :: Distance Kilometer
        distanceInMiles = Distance 10 :: Distance Mile
    (addDistance distanceInKilometers distanceInMiles) `shouldBe` (Distance 16.21371 :: Distance Mile)

```


Haskell Articles