# Contravariant input

In this chapter we will handle input into the database, which will require new typeclass. In order to truly understand what we’re doing we’ll first look at the mathematics of types.

# Algebraic data types

We’ve seen a few ways to declare types in Haskell, but have not declared their mathematical properties. There is an algebra for types just like there is one for numbers. The Unit type that we already know acts a lot like the number 1. There is also a 0, the Void, but that’s mostly a type for theoretical use, since it has no inhabitants, and we couldn’t possibly pass a value for a type that has no values. We also have some kind of addition and multiplication, plus one other operator.

Let’s look at how this type algebra works using type constructs we’ve covered previously.

denotes a type `MyType1`

that is inhabited by every combination of inhabitants from `TypeA`

and `TypeB`

. We call this a *product* type, corresponding to the *Cartesian product* in set theory and the *product* in category theory. The number of its inhabitants is also equal (ignoring bottoms) to the product of the number of elements of its constituents, so pick your favorite memory aid! We also call it a *conjunctive* type for its correspondence to a conjunction (logical `AND`

) in constructive logic.

We’ve also know the following type:

which denotes a type `MyType2`

that is inhabited by either a `TypeA`

or a `TypeB`

. We call this a *sum* type, but also a *union* type in reference to Set theory, a *co-product* in reference to category theory (category theory likes to use “co-” to indicate that something is the dual of another thing), a *disjunctive* type in reference to disjunctions (logical `OR`

) or an *enum* type in reference to the fact that its constructors act as enumerators telling us how to interpret bits stored in memory.

As you can see, many fields in mathematics seem to be coming together here. That’s because they are.

There’s one more type operator that we’ve also encountered, the arrow for functions:

No easy names from elementary mathematics for this one. It’s an arrow, a *relation* in set theory, a *morphism* in category theory, an *implication* in constructive logic.

Products, sums and arrows are the basic type operators from which we can create every other type (well, mostly).

The following table might help you put type algebra into context, you absolutely do not need to understand every field, it *might* help you understand, if not, forget about it. Keep in mind that where numbers use equality, types use isomorphism (`≌`

) and logic uses provability (`⊢`

).

Types | Numbers | Logic | Sets |
---|---|---|---|

Void | 0 | False | ∅ |

Unit | 1 | True | {∅} |

a × b | a * b | a ∧ b | a × b |

a + b | a + b | a ∨ b | a ∪ b |

a → b | a → b | ||

a × Void ≌ Void | a * 0 = 0 | a ∧ False ⊢ False | a × ∅ = ∅ |

a + Void ≌ a | a + 0 = a | a ∨ False ⊢ a | a ∪ ∅ = a |

a × Unit ≌ a | a * 1 = a | a ∧ True ⊢ a | a × {∅} = {(x, ∅) | x ∈ a} ≌ a |

function application | modus ponens |

I’ve left relations in set theory out of this as they don’t translate well symbolically from arrows.

# Simple type functions

We’ve used functors, applicatives, and monads on a few occasions. These are all classes of type functions. Now we’re going to roll our own functor, and do something we wouldn’t usually do, namely manually define its instance declarations rather than using `deriving`

. We do this to illustrate a problem.

```
data MyFunctor1 b = MyType1A TypeA | MyType1B b
instance Functor MyFunctor1 where
fmap someFunction myFunctor = case myFunctor of
MyType1A ta -> MyType1A ta
MyType1B someValue -> MyType1B $ someFunction someValue
```

There’s a few things going on here.

First, we’ve declared a type which takes a type variable called `b`

. Remember that functors have kind `* -> *`

? We must therefore have some input type with kind `*`

. So `MyFunctor1 Int`

would construct the type `MyType1A TypeA | MyType1B Int`

. With the type algebra from above, we would write this type as:

$MyFunctor1(b) = TypeA + b$

Second, we’ve declared `MyFunctor1`

to be an instance of `Functor`

. `Functor`

requires the declaration of a function `fmap :: (a -> b) -> f a -> f b`

, in our case, `f`

is `MyFunctor1`

, so we need a:

Note that this `b`

is not necessarily the same `b`

as the type declaration, as they are in different scopes.

There is really only one way to turn an `f a`

into `f b`

if we’re using sum and product types, which is to apply the function to every `a`

, because the only thing we know about `a`

is that it is input to `f`

, so there is nothing else we can do with it. This is also why we can simply `derive`

the functor instance for all our types, there at most 1 way to do it.

Things get a bit complicated with arrows:

```
-- This one is easy, we just use function composition
data MyFunctor2 b = MyFunctor2 (TypeA -> b)
instance Functor MyFunctor2 where
fmap someFunction (MyFunctor2 f) =
MyFunctor2 $ someFunction . f
-- This one is impossible
data MyFunctor3 a = MyFunctor3 (a -> TypeB)
instance Functor MyFunctor3 where
fmap someFunction (MyFunctor3 f) = ..?
```

We simply have no way to combine an `a -> b`

and `a -> c`

into a `c -> b`

.

What’s happening here?

In the sum type `a + b`

, both arguments `a`

and `b`

are said to be in a positive position. Same for products `a ✕ b`

. In arrow types `a → b`

, `b`

is in a positive position, but `a`

is in a negative position. To “map” type variables in negative position, we need to flip the order of arrows:

If `a`

is in a negative position in the type `f a`

, we call `f`

a *contravariant* functor. Regular functors are *covariant*.

## Note:

Remember two ways in which Haskell is not total from last chapter? Contravariant type recursion is the third:

# Encoders

Hasql uses contravariant functors in its encoders. That makes sense, since encoders are also a sort of “input taker”. It uses the module `Data.Functor.Contravariant`

, which requires `Contravariant`

s to have the function `contramap :: (a -> b) -> f b -> f a`

, which should look rather familiar with the knowledge above. Let’s import the module:

Before we dive into writing encoders, let’s generalize our code a bit. Replace the old fetchFromDB:

```
connectionSettings :: Hasql.Connection.Settings
connectionSettings =
Hasql.Connection.settings
"localhost"
(fromInteger 5432)
"Haskell-student"
"Why-are-you-putting-credentials-in-code?-You-absolute-potato!"
"todolists"
runSessionAndClose :: Hasql.Session.Session a -> IO a
runSessionAndClose session =
do
connectionResult <- Hasql.Connection.acquire connectionSettings
case connectionResult of
Left (Just errMsg) -> error $ StrictUTF8.toString errMsg
Left Nothing -> error "Unspecified connection error"
Right connection -> do
sessionResult <- Hasql.Session.run session connection
Hasql.Connection.release connection
case sessionResult of
Right result -> return result
Left err -> error $ show err
fetchFromDB :: IO [Task]
fetchFromDB = runSessionAndClose selectTasksSession
```

Then, let’s start with the statement, just as we did for decoders:

```
pushTaskStatement :: Hasql.Statement.Statement String ()
pushTaskStatement =
Hasql.Statement.Statement
"INSERT INTO todolist_ch5 ( \
\ task, \
\ done \
\)\
\VALUES \
\ ( $1, FALSE );"
taskNameEncoder
Hasql.Decoders.unit
True
taskNameEncoder :: Hasql.Encoders.Params String
taskNameEncoder = error "Encoder not implemented yet"
```

Hasql come swith a `Value Text`

decoder, but we need a `Value String`

! This time we will need a function `String -> Text`

rather than `Text -> String`

, because `Value`

is contravariant. We use the `pack`

from `Data.Text`

.

```
taskNameEncoder :: Hasql.Encoders.Params String
taskNameEncoder = Hasql.Encoders.param taskNameEncoder_value
taskNameEncoder_value :: Hasql.Encoders.Value String
taskNameEncoder_value = contramap Data.Text.pack Hasql.Encoders.text
```

Now we only need to put it all together in a session and run it:

```
pushTaskToDB :: String -> IO ()
pushTaskToDB taskDescription =
let
session :: Hasql.Session.Session ()
session = Hasql.Session.statement taskDescription pushTaskStatement
in
runSessionAndClose session
```

Don’t forget to add `pushTaskToDB`

to the exports list.

Finally, let’s call this function every time we start our server:

##### src/ServerMain.hs

```
startServer :: IO ()
startServer = do
TaskDB.pushTaskToDB "implement new feature request for client"
Warp.run 8080 requestHandler
```

You may have noticed this will create an ever-increasing list of tasks. That is correct, because feature requests from clients will never cease, which is why achieving world domination comes first.

If you like my work, please consider buying me a coffee or using the brave browser.