Original literate haskell source

`> {-# LANGUAGE DeriveDataTypeable, RankNTypes #-}`

> import Prelude hiding (Functor(..), map, mapM_)

These imports and the `LANGUAGE`

pragma are for the second half.

`> import Control.Applicative`

> import Data.Typeable

> import Data.Foldable

Ye olde (covariant) functor

`> class Functor t where`

> map :: (a -> b) -> t a -> t b

The arrow type constructor is covariantly functorial in its second argument (the first argument is fixed here).

`> instance Functor ((->) a) where`

> map f g = f . g

`> -- Arrow type constructor whose arguments are in reverse order.`

> newtype Co b a = Co (a -> b)

`> -- Contravariant functor`

> class ContraFunctor t where

> contraMap :: (a -> b) -> t b -> t a

`> -- The arrow type with its arguments flipped is a contravariant functor`

> instance ContraFunctor (Co b) where

> contraMap f (Co g) = Co $ g . f

Is `Co`

really a contravariant functor? Check the laws! Law: `contraMap f . contraMap g = contraMap (g . f)`

```
contraMap f . contraMap g {universal quantification}
= (contraMap f . contraMap g) (Co x) {composition}
= contraMap f (contraMap g (Co x)) {definition of contraMap for Co}
= contraMap f (Co (x . g)) {definition of contraMap for Co}
= Co ((x . g) . f) {associativity of composition}
= Co (x . (g . f)) {definition of contraMap for Co}
= contraMap (g . f) (Co x) {universal quantification}
= contraMap (g . f)
```

`Co`

being a contravariant functor means that `(->)`

is contravariantly functorial in its first argument.

A bifunctor is covariantly functorial in two arguments.

`> class BiFunctor t where`

> bimap :: (a -> c) -> (b -> d) -> t a b -> t c d

Is `(->)`

covariantly functorial in both arguments?

`> instance BiFunctor (->) where`

> bimap f g h = undefined

> -- We need to produce a function with domain c, but we don't have one!

`> -- Bifunctor that is contravariant in its first argument`

> class ContraBiFunctor t where

> contraBimap :: (c -> a) -> (b -> d) -> t a b -> t c d

Bingo!

`> instance ContraBiFunctor (->) where`

> contraBimap f g h = g . h . f

A browser provides a DOM to client code. This interface lets client code render a page.

`> class DOM a where`

> putText :: a -> String -> IO ()

Internally, our browser knows other things. Secret things.

`> data BrowserPrivate = BP { bpPutText :: String -> IO ()`

> , password :: String }

> deriving Typeable

Our browser is at least as good as any other browser! Perhaps we can claim that `BrowserPrivate`

is a subtype of `DOM`

.

`> instance DOM BrowserPrivate where putText = bpPutText`

The browser function uses a browser implementation (i.e. something that provides the DOM interface) to run client code that expects a `DOM`

. Our language has also been augmented with reflection, because it's pretty handy.

`> browser :: (Typeable b, DOM b) => `

> b -> (forall a. (Typeable a, DOM a) => a -> IO ()) -> IO ()

> browser browserImpl userCode = userCode browserImpl

Note that `(DOM,secrets) <: DOM`

{by width subtyping of records}, so it's okay to give the extra information to the user code :D

```
BrowserPrivate <: DOM IO () <: IO ()
------------------------------------------
DOM -> IO () <: BrowserPrivate -> IO ()
```

We can treat userCode as though it were of type `BrowserPrivate -> IO ()`

because it is a subtype of that type.

`> -- Typical website`

> website :: (Typeable a, DOM a) => a -> IO ()

> website = mapM_ <$> putText <*> (password <$>) . cast

Enjoy the web!

`> security = browser (BP putStrLn "tacos") website >> putStrLn "dammit!"`

Another browser that takes pains to keep things separate.

`> data JustDOM = JD { jdPutText :: String -> IO () } `

> deriving Typeable

>

> instance DOM JustDOM where putText = jdPutText

`> data BrowserSandbox = BS { dom :: JustDOM, password' :: String }`

> deriving Typeable

Note: `BrowserSandbox`

is *not* an instance (or subtype) of `DOM`

!

`> sandy = browser (dom $ BS (JD putStrLn) "tacos") website >> putStrLn "lolcats"`

Alternately, in a world without reflection...

`> browser' :: DOM b => b -> (forall a. DOM a => a -> IO ()) -> IO ()`

> browser' browserImpl userCode = userCode browserImpl

This doesn't type check because the client code wants to reflect on us but we won't allow it!

`> -- thanksTypes = browser' (BP putStrLn "tacos") website`

```
Prelude> :l ContravariantFunctors.lhs
[1 of 1] Compiling Main ( ContravariantFunctors.lhs, interpreted )
Ok, modules loaded: Main.
*Main> security
tacos
dammit!
*Main> sandy
lolcats
```