polynomial.tex

% Copyright 2004 by Till Tantau <tantau@users.sourceforge.net>.
%
% In principle, this file can be redistributed and/or modified under
% the terms of the GNU Public License, version 2.
%
% However, this file is supposed to be a template to be modified
% for your own needs. For this reason, if you use this file as a
% template and not specifically distribute it as part of a another
% package/program, I grant the extra permission to freely copy and
% modify this file as you see fit and even to delete this copyright
% notice. 

\documentclass{beamer}

\usepackage{listings}
\usepackage{color}
\usepackage[utf8]{inputenc}
\usepackage{mathtools}


\usepackage[all]{xy}
%%%  Xypic macros
\newcommand{\xycenter}[1]{\vcenter{\hbox{\xymatrix{#1}}}}
\SelectTips{cm}{}
\newdir{ >}{{}*!/-7pt/@{>}}
%%% Pullback symbols
\newcommand{\ulpullback}[1][ul]{\save*!/#1-1.2pc/#1:(-1,1)@^{|-}\restore}
\newcommand{\dlpullback}[1][dl]{\save*!/#1-1.2pc/#1:(-1,1)@^{|-}\restore}
\newcommand{\urpullback}[1][ur]{\save*!/#1-1.2pc/#1:(-1,1)@^{|-}\restore}
\newcommand{\drpullback}[1][dr]{\save*!/#1-1.2pc/#1:(-1,1)@^{|-}\restore}

\newcommand{\NN}{\mathbb{N}}
\newcommand{\Set}{{\tt Set }}
\newcommand{\Type}{{\tt Type }}

\newcommand{\Nil}{\mbox{Nil }}
\newcommand{\Cons}{\mbox{Cons }}
\newcommand\doubleplus{+\kern-1.3ex+\kern0.8ex}


%New colors defined below
\definecolor{codegreen}{rgb}{0,0.6,0}
\definecolor{codegray}{rgb}{0.5,0.5,0.5}
\definecolor{codepurple}{rgb}{0.58,0,0.82}
\definecolor{backcolour}{rgb}{0.95,0.95,0.92}

\setbeamertemplate{footline}[text line]{%
  \parbox{\linewidth}{\vspace*{-8pt}\hfill\insertpagenumber}}
\setbeamertemplate{navigation symbols}{}


%Code listing style named "mystyle"
\lstdefinestyle{mystyle}{
language=Haskell,
  %backgroundcolor=\color{backcolour},   commentstyle=\color{codegreen},
  keywordstyle=\color{blue},
 % numberstyle=\tiny\color{codegray},
  stringstyle=\color{codepurple},
%  basicstyle=\footnotesize,
%  breakatwhitespace=false,         
%  breaklines=true,                 
%  captionpos=b,                    
%  keepspaces=true,                 
%  numbers=left,                    
%  numbersep=5pt,                  
%  showspaces=false,                
%  showstringspaces=false,
%  showtabs=false,                  
%  tabsize=2
  mathescape=true,
  literate=
    {Groth}{$\int$}{1}
    {->}{$\to$}{2}
    {undefined}{$\bot$}{1}
    {()}{$\top$}{1}
}





% There are many different themes available for Beamer. A comprehensive
% list with examples is given here:
% http://deic.uab.es/~iblanes/beamer_gallery/index_by_theme.html
% You can uncomment the themes below if you would like to use a different
% one:
%\usetheme{AnnArbor}
%\usetheme{Antibes}
%\usetheme{Bergen}
%\usetheme{Berkeley}
%\usetheme{Berlin}
%\usetheme{Boadilla}
%\usetheme{boxes}
%\usetheme{CambridgeUS}
%\usetheme{Copenhagen}
%\usetheme{Darmstadt}
\usetheme{default}
%\usetheme{Frankfurt}
%\usetheme{Goettingen}
%\usetheme{Hannover}
%\usetheme{Ilmenau}
%\usetheme{JuanLesPins}
%\usetheme{Luebeck}
%\usetheme{Madrid}
%\usetheme{Malmoe}
%\usetheme{Marburg}
%\usetheme{Montpellier}
%\usetheme{PaloAlto}
%\usetheme{Pittsburgh}
%\usetheme{Rochester}
%\usetheme{Singapore}
%\usetheme{Szeged}
%\usetheme{Warsaw}


% A subtitle is optional and this may be deleted
\title{Rethinking Inheritance with Algebraic Ornaments}

\author{Dai}\\



\institute[MIT] % (optional, but mostly needed)
{ MIT}

% - Use the \inst command only if there are several affiliations.
% - Keep it simple, no one is interested in your street address.

\date{Formal Methods Seminar Series\\April 2015}
% - Either use conference name or its abbreviation.
% - Not really informative to the audience, more for people (including
%   yourself) who are reading the slides online

\subject{Theoretical Computer Science}
% This is only inserted into the PDF information catalog. Can be left
% out. 

% If you have a file called "university-logo-filename.xxx", where xxx
% is a graphic format that can be processed by latex or pdflatex,
% resp., then you can add a logo as follows:

% \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
% \logo{\pgfuseimage{university-logo}}

% Delete this, if you do not want the table of contents to pop up at
% the beginning of each subsection:
\AtBeginSubsection[]
{
  \begin{frame}<beamer>{Outline}
    \tableofcontents[currentsection,currentsubsection]
  \end{frame}
}

% Let's get started
\begin{document}

\begin{frame}
  \titlepage
\end{frame}

\begin{frame}{Rethinking Inheritance}
\begin{itemize}
\item Inheritance allows building more complex types from simpler ones
\item In OO, functions are bundled with data, so we also extend functions
\pause
\item A subtype $A$ of $B$ allows the substitution of $A$ whenever a $B$ is needed.

\end{itemize}
\pause
Inheritance is a construction, subtyping is a property of the type system!
\end{frame}

% Section and subsections will appear in the presentation overview
% and table of contents.

\begin{frame}[fragile]{Simple Data}
\begin{lstlisting}[language=Haskell]
data FooBar = Foo Int Double | Bar String
\end{lstlisting}
\hrulefill
\begin{lstlisting}[language=ML]
datatype foobar = | Foo of (int,double) 
                  | Bar of string
\end{lstlisting}
\hrulefill
\begin{lstlisting}[language=Scala]
sealed abstract class FooBar
final case class Foo(foo1: Int, foo2: Double) extends FooBar
final case class Bar(bar1: String) extends FooBar
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]{Simple Data Cont.}
\begin{lstlisting}[language=C]
struct foo {int foo1; double foo2;}
struct bar {char *bar1;}
union foo_bar_untagged {foo f; bar b;}
enum {FOO,BAR} foo_bar_tag;
struct foo_bar {foo_bar_tag tag; foo_bar_untagged v;}
\end{lstlisting}
\end{frame}
\lstset{style=mystyle}

\begin{frame}{Algebraic Data}
We'll focus on algebraic data for its nice properties and powerful type theory.
\pause
\begin{itemize}
\item $Void \cong 0$
\item $() \cong 1$
\item $\operatorname{Either} a b \cong a + b$
\item $(a,b) \cong a * b$
\item $(a \to b) \cong b^a$
\end{itemize}
\hrulefill
\pause

In fact, calculus, generating functionology, and nearly anything that works with complex number expressions works here.
\end{frame}


\begin{frame}{Algebraic Examples}

\begin{itemize}
\item $\lstinline+data Maybe a = Nothing | Just a+ \hfill \cong  1 + a$
\pause
\item $\lstinline+data Nat = Z | S Nat+  \hfill \cong \mu x. 1 + x$
\item $\lstinline+data Fix f = Fix (f (Fix f))+ \hfill \cong  \mu x. f x$
\item $\mbox{Nat} \cong \mbox{Fix Maybe}$
\pause
\item $\lstinline+data List a = Nil | Cons a (List a)+ \hfill \cong \mu x. 1 + a*x$
\item $\lstinline+data Cell a x = CNil | Cell a x+ \hfill \cong 1 + a*x$ %Write this example down in haskell notation in full
\item $\mbox{List } a \cong \mbox{Fix (Cell a)}$
\end{itemize}

\pause
\begin{definition}[Description]
Every recursive type is the fixed point of some ``base'' polynomial.
\end{definition}

\end{frame}


\begin{frame}{An Extended Type Theory}
$\hat I$, Types indexed by $I$: \[(i : I) \vdash X_i\quad\mbox{or}\quad (i : I) \vdash f(i)\]
\pause
The dependent sum (pair): \[\sum_{a : A} f(a) \quad\mbox{or}\quad (a : A, f(a))\]
\pause
The dependent sum (pair): \[\prod_{a : A} \quad\mbox{or}\quad(a : A) \to f(a)\]
\end{frame}

\begin{frame}[fragile]{What's in a datatype?}
\begin{lstlisting}
data ListA_ x = Nil | Cons A x
type ListA = Fix ListA_
\end{lstlisting}
\pause
The \alert{Description} \lstinline+ListA_+ is made of:
\begin{itemize}
\item A set of shapes/constructors $\int S : \Set$
\begin{itemize}
\item[] $\{\Nil \} \cup \{\Cons a \mid a \in A\}$
\end{itemize}
\pause
\item A function $\int S \xrightarrow{P} \Set$ giving \alert{recursive positions} to shapes
\begin{itemize}
\item[] $\Nil \overset{P}{\mapsto} \emptyset$
\item[] $\Cons a \overset{P}{\mapsto} \{\bullet\}$
\end{itemize}
\end{itemize}

\pause
\begin{block}{Interpretations:}
\begin{itemize}
\item A map of dependent types $X \mapsto (s : \int S, (p : P~s) \to X)$
\item A polynomial $\sum_{(s : \int S)} \prod_{(p : P~s)} X$
\item A forest of forks
\end{itemize} 
\end{block}
\end{frame}

\begin{frame}[fragile]{Indexed Data}
\begin{example}[Packed Data]
\lstinline+data Packed a = Array (Array a) | Bytes ByteString+\\
\hrulefill


But $a$ is free in \lstinline+Bytes :: ByteString -> Packed a+\\
\pause
We want to control the input and output index using \emph{Generalized} ADT (GADTs):

\begin{lstlisting}
data Packed a where
    Array :: Array a -> Packed a
    Bytes :: ByteString -> Packed Char
\end{lstlisting}
\end{example}
\pause
\begin{example}[Length-indexed vectors]
\begin{lstlisting}
data VecA :: Nat -> * where
    VNil :: VecA Z
    VCons :: A -> VecA n -> VecA (S n)
\end{lstlisting}
\end{example}
\pause
Best understood as labeled forks.
\end{frame}

\begin{frame}[fragile]{What's in a datatype? Redux}
\begin{definition}[Description]
A \alert{Data Description} $S \triangleleft^n P$ from from index set $I$ to $J$ is made of:
\begin{itemize}
\item[]  $S : J \to \Set$, A family of \alert{shapes/constructors} indexed by $J$
\item[]  $P : \int S \to \Set$, A family of \alert{positions} indexed by shapes
\item[] $n : \int P \to I$, A \alert{next/recursive} index for each position
\end{itemize}
\end{definition}
Where $\int S = (j : J, S~j) \quad \int P = (s : \int S, P~s)$
\pause
\[I \xleftarrow{n} \int P \xrightarrow{P^{-1}} \int S \xrightarrow{S^{-1}} J\]
\end{frame}

\begin{frame}{Interpretations}
\begin{center}
$\hat I \xrightarrow{\Delta_n} \hat{ \int P} \xrightarrow{\Pi_P} \hat{\int S} \xrightarrow{\Sigma_S} \hat J$
\end{center}
\[\frac{(i : I) \vdash X_i}{(j : J) \vdash (s : S~j, (p : P~s) \to X_{n(p)})} \Sigma_S \Pi_P \Delta_n\]
\hrulefill

\pause
\[\frac{(i : I) \vdash X_i}{(p : \int P) \vdash X_{n(p)}} \Delta_n\]
\begin{columns}
\column{0.5\textwidth}
\[\frac{(s : \int S) \vdash X_s}{(j : J) \vdash (s : S~j, X_s)} \Sigma_S\]
\column{0.5\textwidth}
\[\frac{(p : \int P) \vdash X_p}{(s : \int S) \vdash (p : P~s) \to  X_p} \Pi_P\]
\end{columns}

\end{frame}


\begin{frame}[fragile]{Example: Constant Maybe}
\begin{lstlisting}
data MaybeA = Nothing | Just A
\end{lstlisting}
\pause
\begin{columns}
\column{0.33\textwidth}
\begin{block}{$1 \xrightarrow{Shape} \Set$}
$\bullet \mapsto \{Nothing, Just~a\}$
\end{block}

\column{0.33\textwidth}
\begin{block}{$\int Shape \xrightarrow{Pos} \Set$}
$s \mapsto \emptyset$

\end{block}

\column{0.33\textwidth}
\begin{block}{$\int Pos \xrightarrow{next} 1$}
$p \mapsto 1$
\end{block}
\end{columns}
\\~\\
\pause
 \[\xymatrix{
 1 & \emptyset \ar[l]^_{\bot} \ar[r]^{\bot} & 1 + A \ar[r]^{!} & 1}\]
 \pause
 \[
\frac{\bullet : 1 \vdash X}{\bullet : 1 \vdash (Nothing,\bullet) + (Just~a_1,\bullet) + (Just~a_2,\bullet) + ...}
\]
\end{frame}

\begin{frame}[fragile]{Example: Maybe}
\begin{lstlisting}
data Maybe a = Nothing | Just a  ???

\end{lstlisting}
\pause
\begin{columns}
\column{0.33\textwidth}
\begin{block}{$\Type \xrightarrow{Shape} \Set$}
$a \mapsto \{Nothing, Just\}\\

\end{block}

\column{0.33\textwidth}
\begin{block}{$\int Shape \xrightarrow{Pos} \Set$}
$(a, Nothing) \mapsto \emptyset\\
(a,Just) \mapsto \{\bullet\}$
\end{block}

\column{0.33\textwidth}
\begin{block}{$\int Pos \xrightarrow{next} \Type$}
$(a,Just,\bullet) \mapsto a$
\end{block}
\end{columns}
\\~\\
\pause
 \[\xymatrix{
 \Type & \Type \ar@{=}[l] \ar@{^{(}->}[r] & 2* \Type \ar[r]^{\pi_2} & \Type}\]
 \pause
 \[
\frac{a : \Type \vdash X_a}{ a : \Type \vdash (Nothing,\bullet) + (Just,X_a)}
\]
\pause
\begin{center}
\Large Not what we expect!
\end{center}
\lstinline+data Maybe2 (f :: * -> *) a = Nothing | Just (f a)+
\end{frame}

\begin{frame}[fragile]{Example: Polymorphic Lists}
\begin{lstlisting}
data List_ a x where
    Nil :: List_ a x
    Cons :: a -> x a -> List_ a x
\end{lstlisting}
\pause
\begin{columns}
\column{0.33\textwidth}
\begin{block}{$\Type \xrightarrow{Shape} \Set$}
$t \mapsto \{\Nil,\Cons (a :: t)\}$
\end{block}

\column{0.33\textwidth}
\begin{block}{$\int Shape \xrightarrow{Pos} \Set$}
$(t, \Nil) \mapsto \emptyset\\
(t,\Cons (a :: t)) \mapsto \{\bullet\}$
\end{block}

\column{0.33\textwidth}
\begin{block}{$\int Pos \xrightarrow{next} \NN$}
$(t,\Cons (a : t),\bullet) \mapsto t$
\end{block}
\end{columns}
\\~\\
\pause
 \[\xymatrix{
 \Type & \Type * a \ar[l]_{\pi_1} \ar@{^{(}->}[r] & 1 + \Type * (1 + a) \ar[r]^{\quad\quad\pi_1} & \Type}\]
 \pause
 \[
\frac{t : \Type \vdash X_t}{ t : \Type \vdash (\Nil, \bullet) + (Cons (a :: t), \bullet \to X_t) }
\]
\end{frame}



\begin{frame}[fragile]{Example: Monomorphic Vectors}
\begin{lstlisting}
data AVec_ n x where
    VNilA :: AVec_ 0 x
    VConsA :: A -> x n -> AVec_ (n+1) x
\end{lstlisting}
\pause
\begin{columns}
\column{0.33\textwidth}
\begin{block}{$\NN \xrightarrow{Shape} \Set$}
$A \mapsto \{VNilA\}\\
S~n \mapsto \Cons a$
\end{block}

\column{0.33\textwidth}
\begin{block}{$\int Shape \xrightarrow{Pos} \Set$}
$(Z, VNilA) \mapsto \emptyset\\
(S~n,VConsA a) \mapsto \{\bullet\}$
\end{block}

\column{0.33\textwidth}
\begin{block}{$\int Pos \xrightarrow{next} \NN$}
$(S~n,VConsA a,\bullet) \mapsto n$
\end{block}
\end{columns}
\\~\\
\pause
 \[\xymatrix{
 \NN & A*\NN^+ \ar[l]^{\pi_2} \ar@{^{(}->}[r] & 1 + A*\NN^+ \ar[r]^{\quad\quad Z \nabla snd} & \NN}\]
 \pause
 \[
\frac{n : \NN \vdash X_n}{ n : \NN \vdash (c : Shape(n), p : Pos(c) \to X_{n-1})}
\]
\end{frame}

\begin{frame}{Ornaments}
An \alert{Ornament} from $(S \triangleleft^{n} P)$ to $(S' \triangleleft^{n'} P')$ is a \alert{Morphism of Containers}:

$\alpha \underset{u}{\overset{v}{\blacktriangleleft}} \omega : (S' \triangleleft^{n'} P') \xRightarrow[u]{v} (S \triangleleft^n P)$:
 \[ \xycenter{
  K \ar[dd]^u & \int P'  \ar[r]^{P'^{-1}} \ar[l]_{n'} & \int S' \ar[dd]^{\alpha} \ar[r]^{S'^{-1}} & L 
  \ar[dd]^v   \\
    & \ar[ur]_{\pi_2} \int P \times_{\int S} \int S' \ar[d]^{\pi_1} \ar[u]^{\omega} &  & \\
  I  & \int P \ar[r]_{P^{-1}} \ar[l]^{n} & \int S \ar[r]_{S^{-1}}   &J} 
  \]
  
  Explicitly: 
\begin{itemize}
\item[] $\alpha$ : (l : L,S' l) $\to$ S (v l)
\item[] $\omega$ : (sh' : $\int$ S', P (A sh')) $\to$ P' sh'
\item[] q : (l : L, sh' : S' l, pos : P (A sh')) $\to$ u (n'($\omega$ pos)) = n pos
\end{itemize}
\end{frame}

\begin{frame}[fragile]{Lists from Naturals}
\begin{lstlisting}
data Nat = Z | S Nat
$\Downarrow$
data ListA = Nil | Cons A
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]{Vectors from Lists}
\begin{lstlisting}
data ListA = Nil | Cons A
$\Downarrow$
data VecA :: Nat -> * where
    VNil :: VecA Z
    VCons :: A -> VecA n -> VecA (S n)
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]{Red-Black Trees from Trees}

\begin{lstlisting}
data Tree = Leaf | Branch Tree Tree
$\Downarrow$
data RB = R | B
data RBTreeA :: RB -> * where
Leaf :: RBTree rb
RBranch :: RBTreeA B -> A -> RBTreeA B -> RBTreeA R
BBranch :: RBTreeA R -> A -> RBTreeA R -> RBTreeA B
\end{lstlisting}

\end{frame}

\begin{frame}[fragile]{Singleton Ornaments}
\begin{lstlisting}
data Nat = Z | S
$\Downarrow$
data SNat :: Nat -> * where
    SZ :: SNat Z
    SS :: (n :: Nat) -> SNat (S n)
\end{lstlisting}

\end{frame}

\begin{frame}[fragile]{Combining Ornaments}
\begin{definition}
The \alert{Parallel Composition} of ornaments $A \xRightarrow{F} B$ and $A \xrightarrow{C}$ is a new ornament $A \xrightarrow{F \otimes G} B \times_{A} C$: the most general unifier of both enhancements
\end{definition}
\pause
\begin{example}[Vectors]
\item (List $\Rightarrow$ Vector) $\cong$ (Singleton$_\NN$) $\otimes$ ($\NN \Rightarrow$ List)
\end{example}
\pause
\begin{definition}
The \alert{Optimized Predicate} of an ornament $A \xRightarrow{F} B$ is the parallel composition $F \otimes $ Singleton
\end{definition}
\begin{example}[Optimized Maybe]
\begin{lstlisting}
data IMaybeA :: Bool -> * where
    INothing :: IMaybeA False
    IJust :: A -> IMaybeA True
\end{lstlisting}
\end{example}

\end{frame}


\begin{frame}[fragile]{Re-Rethinking Inheritance}
\begin{itemize}
\item Inheritance allows code reuse by extending data and functions
\item Subtyping $A < B$ allows the complete substitution of $A$ for whenever a $B$ is needed. \emph{All methods defined on $B$ are defined on $A$}
\end{itemize}
\pause
\begin{center}
\Large How to generalize to a functional setting?
\end{center}
\end{frame}
\begin{frame}{Transporting Functions Across Ornaments}
Notice the similarity:
\begin{block}{$\NN + \NN : \NN$}
$\{Z,\bullet\} + m \mapsto m\\
\{Suc, n\} + m \mapsto \{Suc,\lambda \bullet.m(\bullet) + n(\bullet)\}$
\end{block}
\begin{block}{$List~t \doubleplus List~t : List~t$}
$\{Nil_t,\bullet\} \doubleplus ys \mapsto ys\\
\{\Cons~(a :: t), xs\} \doubleplus ys \mapsto \{Cons~(a :: t),\lambda \bullet.xs(\bullet) \doubleplus ys(\bullet)\}$
\end{block}
\pause
Look at what happens to the trees.
\end{frame}

\begin{frame}[fragile]{Indexed Transport}
\begin{lstlisting}
data HList (ts :: [*]) where
    HNil :: HList []
    HCons :: t -> HList ts -> HList (t:ts)

reverse :: List a -> List a
reverse Nil = Nil
reverse (Cons a as) = reverse as ++ (Cons a Nil) 

hReverse :: HList xs -> HList (reverse xs)
hReverse HNil = HNil
hReverse (HCons a as) = hReverse as ++ (HCons a HNil)

\end{lstlisting}

\end{frame}

\begin{frame}[fragile]{Coherence Concerns}

\begin{lstlisting}
(<) :: $\NN$ -> $\NN$ -> Bool
n < Z = False
Z < S m = True
S n < m = n < m
lookup :: $\NN$ -> ListA -> MaybeA
lookup n Nil = Nothing
lookup Z (Cons a xs) = Just a
lookup (S n) xs = lookup n xs
\end{lstlisting}
\pause
Coherence: \lstinline+isJust . lookup n == (n <) . length+
\pause
\begin{lstlisting}
-- The optimized predicate MaybeA $\otimes$ Singleton$_{Bool}$
data IMaybeA :: Bool -> * where
    INothing :: IMaybeA False
    IJust :: A -> IMaybeA True
\end{lstlisting}

Lift lookup to opimized predicates VecA and IMaybeA, with (<) on indicies. Coherence for free!
\end{frame}
\begin{frame}{Recap}
\begin{itemize}
\item Polynomials allow first class data representation with nice algebraic properties
\item Ornaments let us build more complex types from simpler ones, and allows \emph{ad-hoc} extension
\item Transport of functions across ornaments allow inheritance
\item Coherent liftings allow subtypeing
\end{itemize}

\end{frame}
\begin{frame}
\begin{center}
\Huge Questions?
\end{center}

\end{frame}
\begin{frame}{Categories}
Categories capture the essence of composition and modularity.
\pause
\begin{definition}[Category]
A category $C$ has:
\begin{itemize}
\item A collection of objects $c : C$
\item A collection of  morphisms (arrows) between (indexed by) pairs of objects $c \xrightarrow{f} c'$
\item Arrows compose: For every pair of arrows $a \xrightarrow{f} b \xrightarrow{g} c$, their composition $a \xrightarrow{g \circ f} c$
\item Every object $a$ has an identity arrow $a \xrightarrow{1_a} a$
\end{itemize}
\end{definition}
\end{frame}

\begin{frame}[plain,c]
\begin{center}
\Huge Why Categories?
\end{center}
\end{frame}

\begin{frame}{Universal Constructions}
Universal objects are the "most general" of its kind, and are "Unique up to unique isomorphism"
The action of any other object is determined by factoring through the universal one.
\pause
\begin{example}[(Co)Universal Constructions]
\begin{itemize}
\item Products
\pause
\item Coproducts (Sums)
\pause
\item Pullbacks (Fiber Products)
\pause
\item Initial/Terminal Objects
\end{itemize}
\end{example}
\pause
Universal properties allow \alert{encapsulation}: Even if the object construction is messy (or unknown), its interaction is completely determined by the universal property.
They are a \alert{bridge} between abstract interfaces and concrete representations.
% It's always easier to work with concrete representations instead of interface indirection. So instead provide a view to the universal object.
\end{frame}

\begin{frame}{Functors}
\begin{itemize}
\item Functors are arrows between categories.
\item $A \xrightarrow{F} B$ sends objects $a : A$ to objects $b : B$, and arrows $a\to a'$ to arrows $F(a) \to F(a')$
\item ``Functors'' in Haskell are actually functors {\bf Hask} $\to$ {\bf Hask}
\end{itemize}
\pause
\begin{block}{Example}
 \lstinline+data FunBox a = F a deriving (Functor)+
\begin{itemize}
\item The constructor \lstinline+(F :: a -> Funbox a)+ is the object component of the functor
\item \lstinline+fmap :: (a -> b) -> (Funbox a -> Funbox b)+ is the arrow component of the functor
\end{itemize}
\end{block}
\end{frame}

\begin{frame}{(Co)Limits}
\begin{definition}[Diagrams]
A \emph{$J$-shaped diagram} in a category $C$ is any functor $J \xrightarrow{F} C$\\
\end{definition}
We draw them as collection of objects and arrows in $C$, leaving $J$ implicit, because only the shape matters.
\pause
\begin{definition}[(Co)Limit]
The Limit of a diagram (functor) in $C$ is a universal object $\operatorname{Lim} F : C$ with a unique arrow to every object in the diagram.
\end{definition}
The interaction of the composition law and universality forces path equivalence
\end{frame}
 
 

\begin{frame}{Encoding Polynomials Categorically}
$\mbox{Packed}_a \cong \mbox{Array}_a + ByteString$\\
$\Type * \NN \xleftarrow{} B \to A \xrightarrow{} \Type * \NN$

\pause

\[\Set / I \xrightarrow{\Delta_s} \Set / B \xrightarrow{\Pi_f} \Set / A \xrightarrow{\Sigma_t} \Set / J\]
\[\hat I \xrightarrow{\Delta_s} \hat B \xrightarrow{\Pi_f} \hat A \xrightarrow{\Sigma_t} \hat J\]
\[
 \xymatrix{
 & B \ar[ddrr]_{X \circ s} \ar[ddl]_{s} \ar[rrrr]^{f} & & & & A \ar[ddll]_{\operatorname{Rex}_f (X \circ s)} \ar[ddr]^{t} & \\
 & & \ar@{=>}[rr] & & & &  \\
 I \ar[rrr]_{X} & & & \Set & & & J \ar[lll]^{\operatorname{Lex}_t (\operatorname{Rex}_f (X \circ s))}  }
 \]
 
Three interpretations:
\begin{itemize}
\item $I,J$ are the type indicies, variable subscripts/letters, or incoming/outgoing branch labels
\item $A$ are the constructor names, sum subscript, or outgoing edges.
\item $B$ are the recursive positions, product subscript, or incoming edges.
\pause
\item $s$ gives the type index of a recursive position, the variable subscript, or labels each incoming edge.
\item $t$ gives the type index of a constructor, indexes a family of polynomials, or labels each outgoing edge.
\item $f$ describes the shape of a constructor, the components of each product, or the shape of each fork.
\end{itemize}
\end{frame}





\begin{frame}[fragile]{Example: Rank-2 Maybe}
\lstinline+data Maybe2 a (f :: * -> *) = Z | S (f a)+
\pause
\begin{columns}
\column{0.33\textwidth}
\begin{block}{$\Type \xrightarrow{Shape} \Set$}
$a \mapsto \{\mbox{Z},\mbox{S}\}$
\end{block}

\column{0.33\textwidth}
\begin{block}{$\int Shape \xrightarrow{Pos} \Set$}
$(a, Z) \mapsto \emptyset\\
(a, S) \mapsto \{\bullet\}$
\end{block}

\column{0.33\textwidth}
\begin{block}{$\int Pos \xrightarrow{next} \Type$}
$(a,S,\bullet) \mapsto a$
\end{block}
\end{columns}
\\~\\
\pause
 \[\xymatrix{
 X \ar[d]^{x} \ar@{=}[r] & X \ar[d]^{x} \dlpullback & \Type + X \ar[d]_{Id + x} \ar[dr]^{Id \nabla x} & \\
 \Type & \Type \ar@{=}[l] \ar[r]^{inR} & \Type * 2 \ar[r]^{Id \nabla Id} & \Type}\]
\pause
 
  $\Pi_{inR} X \equiv \\
  (a,b) : \Type * \mbox{Bool} \vdash i : \operatorname{inL^{-1}} (a,b) \to X(a)\\
  \cong Type + X$

\end{frame}

\begin{frame}[fragile]{Example: Monomorphic Lists}
\lstinline+data AList_ x = Z | $SA_1$ x | $SA_2$ x | ...+ $\cong$ \lstinline+data AList_ x = Z | S A x+
\pause
\begin{columns}
\column{0.33\textwidth}
\begin{block}{$1 \xrightarrow{Shape} \Set$}
$\bullet \mapsto \{\mbox{Z},\mbox{S}\}$
\end{block}

\column{0.33\textwidth}
\begin{block}{$\int Shape \xrightarrow{Pos} \Set$}
$(\bullet, Z) \mapsto \emptyset\\
(\bullet, S a) \mapsto \{\bullet\}$
\end{block}

\column{0.33\textwidth}
\begin{block}{$\int Pos \xrightarrow{next} 1$}
$(\bullet,S a,\bullet) \mapsto a$
\end{block}
\end{columns}
\\~\\
\pause
 \[\xymatrix{
 X \ar[d]^{x} \ar@{=}[r] & X \ar[d]^{x} \dlpullback & 1 + X \ar[d]_{Id + x} \ar[dr]^{Id \nabla x} & \\
 1 & 1 \ar@{=}[l] \ar[r]^{inR} & 2 \ar[r]^{!} & 1}\]
\pause
 
  $\Pi_{inL} X \equiv \\
  b : \mbox{Bool} \vdash (i : \operatorname{inL^{-1}} b) \to X\\
  \cong b : \mbox{Bool} \vdash i : (b==true) \to X \\
  \cong 1 + X$

\end{frame}





\end{document}