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

Why we can't have nice things

Reflection and Subtyping

Dedication: sk

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