_jack Glossary

glossary.md

A function mapped on each side.

Any function (profunctor/category) has "inputs" and "outputs". First argument: input (contravariant), second argument: output (covariant). covariant argument.

🟥🟦 :: 🟥 -> 🟦
🟦🟩 :: 🟦 -> 🟩

When composing, it works like domino pieces: 🀺 >>> 🁂 = 🀻 the connecting parts must be match but prefer using colours for it.

🟥🟦 >>> 🟦🟩 :: 🟥 -> 🟩

The middle type has disappeared from the input/output interface of the function. 🟦, as far as composition goes, is an existential type which is not reflected in the output.

(>>>) :: cat 🟥 🟦 -> cat 🟦 🟩 -> cat 🟥 🟩 

If we want to modify the input and output of 🟥🟦 :: 🟥 -> 🟦, a natural pattern emerges: They are mapped at a different variance. What can compose on the left 🟥? Anything that outputs 🟥.

🟥'🟥 :: 🟥' -> 🟥
     :: 🟥 <- 🟥'

And what about the right 🟦? Anything that takes in 🟦.

🟦🟦' :: 🟦 -> 🟦'

This natural observation demonstrates through child-like toys how contravariance emerges from the nature of composition.

🟥'🟥 >>> 🟥🟦 >>> 🟦🟦' :: 🟥' -> 🟦'

Here is how this observation is interprated as annotated functors.

        ,------------------- Op Hask :: Cat Type
        |       ,----------- Hask    :: Cat Type
        |       |       ,--- Hask    :: Cat Type
        |       |       |
(->) :: Type -> Type -> Type

with the mapping function

dimap :: (іn <- іn') -> (out -> out') -> ((іn -> out) -> (іn' -> out'))
dimap pre post f = pre >>> f >>> post

dimap :: (🟥 <- 🟥') -> (🟦 -> 🟦') -> ((🟥 -> 🟦) -> (🟥' -> 🟦'))
dimap 🟥'🟥 🟦🟦' 🟥🟦 = 🟥'🟥 >>> 🟥🟦 >>> 🟦🟦'

And here is how it is interpreted for an arbitrary category cat :: Cat k:

       ,------------- Op cat :: Cat k
       |    ,-------- cat    :: Cat k
       |    |    ,--- Hask   :: Cat Type
       |    |    |
cat :: k -> k -> Type

dimap :: Category cat => Op cat іn іn' -> cat out out' -> (cat іn out -> cat іn' out')
dimap (Op pre) post f = pre >>> f >>> post

Every category gives rise to a Profunctor { Input = cat, Output = cat } using record syntax for associated types.

  Profunctor { Input = cat, Output = cat }
=  Bifunctor { Source1 = Op cat, Source2 = cat, Target = Hask }
=    Functor { Source = Op cat, Target = Nat cat Hask }

dimap :: Profunctor { Input = input, Output = output } pro
      -> Op input іn іn'
      -> output out out'
      -> (pro іn out -> pro іn' out')

Annotated functors