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)
= a . f invertedMap f a
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 @(SillyConstructor f) = f silly doSilly silly makeSilly :: Silly = SillyConstructor doSilly makeSilly anythingYouWant :: a = doSilly makeSilly anythingYouWant
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)
("Haskell-student"
"Why-are-you-putting-credentials-in-code?-You-absolute-potato!"
"todolists"
runSessionAndClose :: Hasql.Session.Session a -> IO a
=
runSessionAndClose session do
<- Hasql.Connection.acquire connectionSettings
connectionResult case connectionResult of
Left (Just errMsg) -> error $ StrictUTF8.toString errMsg
Left Nothing -> error "Unspecified connection error"
Right connection -> do
<- Hasql.Session.run session connection
sessionResult
Hasql.Connection.release connectioncase sessionResult of
Right result -> return result
Left err -> error $ show err
fetchFromDB :: IO [Task]
= runSessionAndClose selectTasksSession fetchFromDB
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.unitTrue
taskNameEncoder :: Hasql.Encoders.Params String
= error "Encoder not implemented yet" taskNameEncoder
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
= Hasql.Encoders.param taskNameEncoder_value
taskNameEncoder
taskNameEncoder_value :: Hasql.Encoders.Value String
= contramap Data.Text.pack Hasql.Encoders.text taskNameEncoder_value
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 ()
= Hasql.Session.statement taskDescription pushTaskStatement
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 ()
= do
startServer "implement new feature request for client"
TaskDB.pushTaskToDB 8080 requestHandler Warp.run
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.