loading...
Cover image for Haskell for madmen: Contravariant input

Haskell for madmen: Contravariant input

drbearhands profile image DrBearhands Originally published at drbearhands.com ・6 min read

Haskell for madmen (8 Part Series)

1) Haskell for madmen: Setup 2) Haskell for madmen: Hello, monad! 3 ... 6 3) Haskell for madmen: Hello, web server! 4) Haskell for madmen: Types of TODO 5) Haskell for madmen: Connecting to a database 6) Haskell for madmen: Reflection and cleanup 7) Haskell for madmen: Contravariant input 8) Haskell for madmen: Wrapping up and closing remarks

Post from my blog. If you're enjoying the series, please consider buying me a coffee. A lot is happening in my life so this one took a bit longer, my apologies.

In this chapter we will handle input into the database, which will require a 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 Contravariants 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
    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.

Haskell for madmen (8 Part Series)

1) Haskell for madmen: Setup 2) Haskell for madmen: Hello, monad! 3 ... 6 3) Haskell for madmen: Hello, web server! 4) Haskell for madmen: Types of TODO 5) Haskell for madmen: Connecting to a database 6) Haskell for madmen: Reflection and cleanup 7) Haskell for madmen: Contravariant input 8) Haskell for madmen: Wrapping up and closing remarks

Posted on by:

Discussion

markdown guide