Notes on Notation

Notation.markdown

Non-standard operators I use :) linked to from my twitter profile

I use kind synonyms

type T   = Type
type TT  = T -> T
type TTT = T -> TT
type C   = Constraint
type TC  = T -> C
..

Most of my categorical thinking comes from Edward Kmett's hask

-- Cat :: TT
type Cat ob = ob -> ob -> Type

-- Functor :: (d -> c) -> Constraint
class (Category (Dom f), Category (Cod f)) => Functor (f :: d -> c) where
  type Dom f :: Cat d
  type Cod f :: Cat c
  
  fmap :: (Dom f) a a' -> (Cod f) (f a) (f a')

A Functor f fully determines its domain (Dom f) and codomain (Cod f) categories, but we often want to be explicit about it. I use FunctorOf dom cod f for this, it can be thought of as a type synonym but it is actually encoded as a class alias/synonym to allow partial application

-- FunctorOf :: Cat d -> Cat c -> (d -> c) -> Constraint
type FunctorOf dom cod f = (Functor f, Cod f ~ cod, Dom f ~ dom)

In this language, the usual Haskell "old" Functors are defined as type OldFunctor = FunctorOf (->) (->)

class OldFunctor (f :: TT) where
  fmap :: (->) a a' -> (->) (f a) (f a')

instance OldFunctor ([] :: TT) where
  fmap :: (->) a a' -> (->) [a] [a']
  fmap f = \case
    []   -> []
    a:as -> f a:fmap f as

instance Functor ([] :: TT) where
  type Dom [] = ((->) :: Cat T)
  type Cod [] = ((->) :: Cat T)
  
  fmap :: (->) a a' -> (->) [a] [a']
  fmap = map

Also use f ~> g to represent "natural transformations", or polymorphic functions from f to g

type f ~>   g = (forall xx.       f xx       -> g xx)
type f ~~>  g = (forall xx yy.    f xx yy    -> g xx yy)
type f ~~~> g = (forall xx yy zz. f xx yy zz -> g xx yy zz)

--   (->) :: Cat                   (T)
--   (~>) :: Cat            (k'' -> T)
--  (~~>) :: Cat      (k' -> k'' -> T)
-- (~~~>) :: Cat (k -> k' -> k'' -> T)

I am experiment with using flipped function composition (>) = (>>>) = flip (.) and (<) = (.)