# 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.

``data MyType1 = MyType2 TypeA TypeB``

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:

``````data MyType2
= MyType2A TypeA
| MyType2B TypeB``````

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:

``data MyType3 = MyType3 (TypeA -> TypeB)``

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:

``fmap :: (a -> b) -> MyFunctor1 a -> MyFunctor1 b``

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:

``````invertedMap :: (c -> a) -> (a -> b) -> (c -> b)
invertedMap f a = a . f``````

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:

``````data Silly = SillyConstructor (Silly -> a)

doSilly :: Silly -> a
doSilly silly@(SillyConstructor f) = f silly

makeSilly :: Silly
makeSilly = SillyConstructor doSilly

anythingYouWant :: a
anythingYouWant = doSilly makeSilly``````

# 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:

``import Data.Functor.Contravariant (contramap)``

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)
"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

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

``````pushTaskStatement :: Hasql.Statement.Statement String ()
Hasql.Statement.Statement
"INSERT INTO todolist_ch5 ( \
\  done \
\)\
\VALUES \
\  ( \$1, FALSE );"
Hasql.Decoders.unit
True

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

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

``````pushTaskToDB :: String -> IO ()
let
session :: Hasql.Session.Session ()
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