
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)

```


Note Articles