talk.tex

\documentclass
  [hyperref={colorlinks = true,linkcolor = blue, 
             citecolor = blue, urlcolor = blue}
  ]{beamer}

\setbeamertemplate{navigation symbols}{}
\setbeamertemplate{footline}[frame number]
 
\usepackage[utf8]{inputenc}

\usepackage[newfloat]{minted}

\usepackage{pgf}
\usepackage{tikz}
\usepackage{upquote}
\usepackage{natbib}
\usepackage[export]{adjustbox}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{trfrac}

\usetikzlibrary{arrows,automata,fit, shapes.geometric}

\bibliographystyle{abbrvnat}

\newenvironment{code}{\captionsetup{type=listing}}{}
\SetupFloatingEnvironment{listing}{name=Listing}

\setbeamertemplate{items}[square]

\renewcommand{\thempfootnote}{\arabic{mpfootnote}}

\title{Why is so much of FP about Types instead of Functions?}
\author{Donovan Crichton}
  
\date{October 2023}

\begin{document}
 
\frame{\titlepage}

\begin{frame}[fragile]
  \frametitle{Preliminaries}
  \begin{itemize}
  \item Slides and Examples available at:
    \href{https://github.com/donovancrichton/Talks}
         {https://github.com/donovancrichton/Talks}
  \item This talk: BFPG/WhyIsFPAboutTypes
  \end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{About Me}
\begin{minipage}[t]{\linewidth}
\noindent
  \begin{minipage}{0.5\linewidth}
    \begin{figure}[h]
       \includegraphics[width=\linewidth]
         {Images/ANU.png}
    \end{figure}
  \end{minipage}
  \hfill
  \begin{minipage}{0.45\linewidth}
    \begin{itemize}
      \item 
        \href{https://cecc.anu.edu.au/people/donovan-crichton}
             {PhD Candidate}
      \item 
        \href{https://comp.anu.edu.au/research/clusters/computing-foundations/}
             {Computing Foundations}
      \item 
        \href{https://comp.anu.edu.au/}
             {School of Computing}
    \end{itemize}
  \end{minipage}
\end{minipage}
\hrule
  \begin{minipage}{0.5\linewidth}
    \begin{figure}[h]
      \includegraphics[scale=0.5,width=\linewidth]
        {Images/GriffithLogo.png}
    \end{figure}
  \end{minipage}
  \hfill
  \begin{minipage}{0.45\linewidth}
  \begin{itemize}
    \item Visiting Scholar
    \item Trusted Systems Lab
    \item \href{https://www.griffith.edu.au/institute-integrated-intelligent-systems}{IIIS}
  \end{itemize}
  \end{minipage}
\hrule
  \begin{minipage}{0.5\linewidth}
    \begin{figure}[h]
      \includegraphics[width=\linewidth]
        {Images/asd-logo.png}
    \end{figure}
  \end{minipage}
  \hfill
  \begin{minipage}{0.45\linewidth}
  \begin{itemize}
    \item ASD 
      \href{https://www.asd.gov.au/about/asd-anu-co-lab}{Co-Lab} 
      Scholar
  \end{itemize}
  \end{minipage}
\end{frame}

\begin{frame}[fragile]
\frametitle{What is a Function?}
\begin{minipage}{0.8\linewidth}
  \begin{figure}[h]
  \includegraphics
    [scale=0.3, width=0.6\linewidth]
    {Images/Function_machine.png}
  \caption[A "black-box" depiction of a function.]{A
  "black-box" depiction of a function\protect\footnote[1]{Source \protect\url{https://en.wikipedia.org/wiki/Function_(mathematics)\#/media/File:Function_machine2.svg}}}
  \end{figure}
\end{minipage}
\end{frame}

\begin{frame}[fragile]
\frametitle{What can we do with a function?}
  \begin{itemize}[<+->]
    \item Give it its argument.
    \item Look at its result.
    \item ...
    \item ...
    \item Maybe we need to think about this some more...
  \end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{What is a function, Georg Cantor?}
\begin{minipage}{0.8\linewidth}
  \begin{figure}[h]
  \includegraphics
    [scale=0.1, width=0.5\linewidth]
    {Images/Georg_Cantor.jpg}
  \caption[Georg Cantor (1845 - 1918)]{Georg Cantor (1845 -
  1918)\protect\footnote[1]{Source
  \protect\url{https://en.wikipedia.org/wiki/Georg_Cantor\#/media/File:Georg_Cantor_(Portr\%C3\%A4t).jpg}}}
  \end{figure}
\end{minipage}
\end{frame}

\begin{frame}[fragile]
\frametitle{Sets}
  \begin{itemize}[<+->]
    \item Sets are concerned with collections of discrete
          mathematical objects. \\
          e.g $A = \{1, 2, 3, ...\}$.
    \item The order of elements does not matter.
    \item Each element my appear only once.
    \item Given an set $X$ and an index $i$ we may 
          chose $x_i \in X$. Think of this like a function
          $f : (Set(X), \mathbb{N}) \rightarrow X$. \\
          e.g $f(A,2) = 2$.
    \item See \citep{halmos1960naive} for more!
  \end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{Relations}
\begin{itemize}
  \item <1-> A relation is a set of pairs and specifically
        is useful for denoting a one-to-many relationship. 
  \item<2-> i.e $1 < 2$, $1 < 3$, $1 < 4$ and so on.
  \item<3-> To the WHITEBOARD\footnote<3->{I sadly did not have
  time to typeset this diagram for tonight's talk, but I will
  upload the completed diagram to GitHub before the end of
  the week.} for a demo.
\end{itemize}

\setbeamercolor{block title}{fg=white,bg=orange!75!black}
\setbeamercolor{block body}{fg=white,bg=orange!25!black}
\begin{block}{Question for the pub!}<4->
Why are functions the default 'building-blocks' in most
programming languages? Why not relations? All
functions are relations, but not all relations are functions.
\end{block}

\end{frame}

\begin{frame}[fragile]
\frametitle{Functions}
  \begin{itemize}
    \item<1-> Functions can have a one-to-one, or many-to-one
          relationship, but never one-to-many.
    \item<2-> There are special classes of \textit{injective}
          functions, where every input gives only one
          output, and all outputs are distinct from
          one-another.
    \item<3-> There are special classes of \textit{surjective}
          functions, where the entire output set can be
          reached through one-or-more inputs.
    \item<4-> Functions that are surjective and injective are
          said to be \textit{bijective}.
    \item<5-> To the WHITEBOARD\footnote<5->{As before, I will
    typeset the accompanying diagrams and upload online.} for
    a demo.
  \end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{What can we do with set-theoretic functions?}
  \begin{itemize}
    \item<1-> We can now easily model \textit{composition}.
    \item<2-> Let's see this on the
    WHITEBOARD\footnote<2->{actual diagrams coming soon to the 
    online version, I promise!}.
    \item<3-> ...
    \item<4-> ...
    \item<5-> Isn't this just giving a function it's argument
              and checking the result though?
    \item<6-> Let's ask someone else...
  \end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{What can we do with functions, Alonzo Church?}
\begin{minipage}{0.8\linewidth}
  \begin{figure}[h]
  \includegraphics
    [scale=0.3, width=0.5\linewidth]
    {Images/Alonzo_Church.jpg}
  \caption[Alonzo Church (1903 - 1995)]{Alonzo Church (1903 -
  1995)\protect\footnote[1]{Source \protect\url{https://en.wikipedia.org/wiki/Alonzo_Church\#/media/File:Alonzo_Church.jpg}}}
  \end{figure}
\end{minipage}
\end{frame}

\begin{frame}[fragile]
\frametitle{The Untyped Lambda Calculus}  
  \setbeamercolor{block title}{fg=white,bg=purple!75!black}
  \setbeamercolor{block body}{fg=black,bg=white!80!gray}
  \begin{block}{The Grammar for LC.}
  \begin{align*}
    M, N ::= & \; x, y, z, ...  &\text{Variables.} \\
             &| \; \lambda x.N  &\text{Abstraction.} \\
             &| \; M \; N       &\text{Application}
  \end{align*}  
  \end{block}
  \setbeamercolor{block title}{fg=white,bg=purple!75!black}
  \setbeamercolor{block body}{fg=black,bg=white!80!gray}
  \begin{block}{An Idris Example (some liberties with types) 
  \\ $\lambda x.\lnot x \; \text{True}$}
  \inputminted{idris}{../Code/src/Lambda.idr}
\end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Functions are limited.}
  \setbeamercolor{block title}{fg=black,bg=green!95!black}
  \setbeamercolor{block body}{fg=white,bg=green!25!black}
  \begin{block}{Can we apply any function to any argument?}
  Clearly we cannot, saying $(3 < 7) + 12$ does not make
  sense, nor does $ (-4) \lor 7$. 
  \\ Operations are often defined as being closed under 
  a particular set. \\
  Closures are really speaking about the type of operations.
  \end{block}
  \setbeamercolor{block title}{fg=black,bg=green!95!black}
  \setbeamercolor{block body}{fg=white,bg=green!25!black}
  \begin{block}{Are there other ways we can categorise
    functions besides the type of their input and output?}
  We can also classify functions based on properties of their
  behaviour. Sometimes we don't care what specific types
  a function operates on, so long as there is some valid
  operation defined for those types.
  \end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Typed vs Untyped composition}
See WHITEBOARD.
\end{frame}

\begin{frame}[fragile]
\frametitle{Types as a class of behaviour}
See WHITEBOARD.
\end{frame}

\begin{frame}[fragile]
\frametitle{To functional programming}
\setbeamercolor{block title}{fg=black,bg=green!95!black}
\setbeamercolor{block body}{fg=white,bg=green!25!black}
\begin{block}{Is everything really a function? (Really?)}
The argument goes that a pure functional language is just
an elaboration of some variant of a typed lambda calculus.
Let's briefly investigate this.
\end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Values as functions.}
  \setbeamercolor{block title}{fg=white,bg=purple!75!black}
  \setbeamercolor{block body}{fg=black,bg=white!80!gray}
  \begin{block}{Are these functions the same?}<1->
  \inputminted{idris}{../Code/src/Values.idr}
  \end{block}

  \setbeamercolor{block title}{fg=black,bg=green!95!black}
  \setbeamercolor{block body}{fg=white,bg=green!25!black}
  \begin{block}{The humble unit type.}<2->
  The unit type is special.
  Denoted \mintinline{idris}{()} or $\top$, the unit type is
  defined as having only one single element, also
  \mintinline{idris}{()}, or sometimes $\ast$.
  The unit element can \textit{always} be constructed.
  This implies that \mintinline{idris}{seven} is the same as
  \mintinline{idris}{seven'} as we can always construct the 
  argument to \mintinline{idris}{seven'}.
  \end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Data types as functions.}
  \setbeamercolor{block title}{fg=black,bg=green!95!black}
  \setbeamercolor{block body}{fg=black,bg=white!80!gray}
  \begin{block}{Can we do the same with data types?}<1->
    We can see this with church encoding, and have a
    small example below, interested readers should see
    \cite[p. 58-68]{pierce2002types}.
  \end{block}

  \setbeamercolor{block title}{fg=white,bg=purple!75!black}
  \setbeamercolor{block body}{fg=black,bg=white!80!gray}
  \begin{block}{Church encoding of the Boolean type}<2->
    \inputminted{idris}{../Code/src/ChurchBools.idr}
  \end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Sum Types}
  \setbeamercolor{block title}{fg=white,bg=purple!75!black}
  \setbeamercolor{block body}{fg=black,bg=white!80!gray}
  \begin{block}{The canonical sum type: Either}
  \inputminted{idris}{../Code/src/Sum.idr}
  \end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Product Types}
  \setbeamercolor{block title}{fg=white,bg=purple!75!black}
  \setbeamercolor{block body}{fg=black,bg=white!80!gray}
  \begin{block}{The canonical product type: Pair}
  \inputminted{idris}{../Code/src/Product.idr}
  \end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Algebraic Data Types}
  \setbeamercolor{block title}{fg=white,bg=purple!75!black}
  \setbeamercolor{block body}{fg=black,bg=white!80!gray}
  \begin{block}{A higher-kinded, parametrically polymorphic,
  sum of product type: List}
  \inputminted{idris}{../Code/src/List.idr}
  \end{block}
\end{frame}

\begin{frame}[fragile]
\frametitle{Dependent Types and Type-classes}
See actual Idris demo on verified functor and verified
applicative.
\end{frame}

\begin{frame}[fragile]
  \frametitle{Is compositionality important, John Hughes?}
\begin{minipage}{0.8\linewidth}
  \begin{figure}[h]
  \includegraphics
    [scale=0.3, width=0.5\linewidth]
    {Images/John_Hughes.jpg}
  \caption[John Hughes]{John
  Hughes\protect\footnote[1]{Source
  \protect\url{https://en.wikipedia.org/wiki/John_Hughes_(computer_scientist)\#/media/File:John_Hughes_(computer_scientist).jpg}}}
  \end{figure}
\end{minipage}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Why Functional Programming Matters
    \cite{hughes1989functional}}
  \setbeamercolor{block title}{fg=black,bg=green!95!black}
  \setbeamercolor{block body}{fg=black,bg=white!80!gray}
  \begin{block}{Modularity through HOF and composition}
    John wrote a seminal paper in 1989 on the benefits of 
    functional programming. He argues that modularity and
    compositionality lead to reusable, readable, debugable
    code. 
  \end{block}

\end{frame}

\begin{frame}[fragile]
\frametitle{Conclusion}

  \setbeamercolor{block title}{fg=black,bg=green!95!black}
  \setbeamercolor{block body}{fg=white,bg=green!25!black}
  \begin{block}{FP is about types}<1->
    Types allow us to talk about well-behaved
    compositionality and talk about functions
    when defined by properties on sets. \\
    In very expressive type systems we can even
    prove those properties.
  \end{block}
  \begin{block}{Functions are boring in general, but
  interesting in specific}<2->
    At the most general view, all a function can do produce
    an output given an input. Functions become interesting
    once you restrict this view to
    functions-with-particular-properties.
  \end{block}
\setbeamercolor{block title}{fg=white,bg=orange!75!black}
\setbeamercolor{block body}{fg=white,bg=orange!25!black}
\begin{block}{Closing comment for the pub}<3->
  I hypothesise that the more expressive a type system
  becomes, the less compositional it becomes, but the
  guarantees of behaviour become stronger. \\
  Is this something we can objectively measure? \\
  Is there a sweet spot for type systems for programming?
\end{block}

\end{frame}

\begin{frame}[fragile]
\frametitle{References}
\bibliography{references}{}
\end{frame}




\end{document}