Talk.tex

\documentclass[tikz, 12pt]{beamer}

% for themes, etc.
\mode<presentation>
{ \usetheme{Copenhagen}
  \usecolortheme{seahorse}{}
  \usefonttheme{professionalfonts}
}
\setbeamertemplate{itemize items}[default]
\setbeamertemplate{enumerate items}[default]
\setbeamertemplate{navigation symbols}{}
\setbeamertemplate{headline}{}
\setbeamertemplate{footline}{}

\usepackage{times}  % fonts are up to you
\usepackage{proof}
\usepackage{listings}
\usepackage{courier}
\usepackage{graphicx}
\usepackage{stmaryrd}

\usepackage{tikz}
\usetikzlibrary{positioning}

\newcommand*\circled[1]{\tikz[baseline=(char.base)]{
            \node[shape=circle,draw,double,inner sep=1pt] (char) {#1};}}

\DeclareMathOperator*{\Wtype}{\textrm{\LARGE W}}
\DeclareMathOperator*{\Mtype}{\textrm{\LARGE M}}
\DeclareMathAlphabet{\mathbfsf}{\encodingdefault}{\sfdefault}{sb}{n}
\def\Type{\mathbfsf{Type}}


\lstset{columns=fullflexible}
\lstset{
  literate={->}{$\to$ }{1}
           {(->)}{$(\to)$ }{1}
           {=>}{$\Rightarrow$ }{1}
           {<-:}{$\Mapsfrom$ }{1}
           {(<-:)}{($\Mapsfrom$)}{1}
           {:E}{$\in$ }{1}
           {:<}{$\subseteq$ }{1}
           {forall}{$\forall$}{1}
           {(<+>)}{($\oplus$) }{1}
           {<+>}{$\oplus$ }{1}
           {<<*>>}{$\circled{$\star$}$ }{1}
           {<<map>>}{$\circled{\$}$ }{1}
           {(<<map>>)}{($\circled{\$}$) }{1}
           {(<<*>>)}{($\circled{$\star$}$) }{1}
           {Nat}{$\mathbb{N}$}{1}
           {Int}{$\mathbb{Z}$}{1},
  escapeinside=~~,
  moredelim=**[is][\color{red}]{@}{@},
}
\lstset{language=Haskell}

% these will be used later in the title page
\title{Vinyl: Records in Haskell \\ and Type Theory}
\author{Jon Sterling\\
  jonmsterling.com
}

\begin{document}

% this prints title, author etc. info from above
\begin{frame}
\titlepage
\end{frame}

\section{Extensible Records and Row Polymorphism}

\begin{frame}[fragile]
  \frametitle{Records in GHC 7.8}\pause
  \begin{itemize}
    \item Haskell records are nominally typed\pause
    \item They may not share field names
  \end{itemize}
  \pause
  \begin{lstlisting}
data R = R { x :: X } ~\pause~
data R' = R' { x :: X } -- ^ Error
  \end{lstlisting}
\end{frame}

\begin{frame}
  \frametitle{Structural typing}\pause
  \begin{itemize}
    \item Sharing field names and accessors\pause
    \item Record types may be characterized \emph{structurally}
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Row polymorphism}\pause
  How do we express the type of a function which adds a field to a record?\pause
  \only<3>{
    \[
      \infer{ f(x) : \{foo:A, bar:B\} }{ x : \{foo:A\} }
    \]
  }
  \only<4>{
    \[
      \infer{ f(x) : \{foo:A, bar:B; \vec{rs}\} }{ x : \{foo:A; \vec{rs}\} }
    \]
  }
\end{frame}

\begin{frame}[fragile]
  \frametitle{Roll your own in Haskell}\pause
  \begin{lstlisting}
data (s :: Symbol) ::: (t :: *) = Field ~\pause~

data Rec :: [*] -> * where ~\pause~
  RNil :: Rec '[] ~\pause~
  (:&) :: !t -> !(Rec rs) -> Rec ((s ::: t) ': rs)

~\pause~
class s :E (rs :: [*])~\pause~
class ss :< (rs :: [*]) where
  cast :: Rec rs -> Rec ss~\pause~
(=:) : s ::: t -> t -> Rec '[s ::: t]~\pause~
(<+>) : Rec ss -> Rec ts -> Rec (ss ++ ts)~\pause~
lens : s ::: t :E rs => s ::: t -> Lens' (Rec rs) t
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Roll your own in Haskell}\pause
  \begin{lstlisting}
f :: Rec ("foo" ::: A ': rs)
  -> Rec ("bar" ::: B ': "foo" ::: A ': rs)
  \end{lstlisting}
\end{frame}

\begin{frame}
  \frametitle{Why be stringly typed?}\pause
  \begin{itemize}
    \item Let's generalize our key space
  \end{itemize}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Old}
  We relied on a single representation for keys as pairs of strings and types.
  \begin{lstlisting}
data Rec :: [*] -> * where
  RNil :: Rec '[]
  (:&) :: !t -> !(Rec rs) -> Rec ((s ::: t) ': rs)
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Proposed}
  We put the keys in an arbitrary type (kind) and describe their semantics with a function \lstinline{el} (for \emph{elements}).
  \begin{lstlisting}
data Rec :: [*] -> * where
  RNil :: Rec '[]
  (:&) :: !t -> !(Rec rs) -> Rec ((s ::: t) ': rs)
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Proposed}
  We put the keys in an arbitrary type (kind) and describe their semantics with a function \lstinline{el} (for \emph{elements}).
  \begin{lstlisting}
data Rec :: (el :: k -> *) -> (rs :: [k]) -> * where
  RNil :: Rec el '[]
  (:&) :: forall (r :: k) (rs':: [k]). !(el r) -> !(Rec el rs) -> Rec (r ': rs')
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Proposed}
  We put the keys in an arbitrary type (kind) and describe their semantics with a function \lstinline{el} (for \emph{elements}).
  \begin{lstlisting}
data Rec :: (k -> *) -> [k] -> * where
  RNil :: Rec el '[]
  (:&) :: !(el r) -> !(Rec el rs) -> Rec (r ': rs)
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Actual}
  Type families are \emph{not} functions, but in many cases can simulate them using Richard Eisenberg's technique outlined in \emph{Defunctionalization for the win}.
  \begin{lstlisting}
data TyFun :: * -> * -> *~\pause~
type family (f :: TyFun k l -> *) $ (x :: k) :: l~\pause~

data Rec :: (TyFun k * -> *) -> [k] -> * where
  RNil :: Rec el '[]
  (:&) :: !(el $ r) -> !(Rec el rs) -> Rec el (r ': rs)
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Example}
  \begin{lstlisting}
data Label = Home | Work
data AddrKeys = Name | Phone Label | Email Label~\pause~

data SLabel :: Label -> * where
  SHome :: SLabel Home
  SWork :: SLabel Work
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Example}
  \begin{lstlisting}
data Label = Home | Work
data AddrKeys = Name | Phone Label | Email Label

data SLabel :: Label -> *~\pause~
data SAddrKeys :: AddrKeys -> * where
  SName :: SAddrKeys Name
  SPhone :: SLabel l -> SAddrKeys (Phone l)
  SEmail :: SLabel l -> SAddrKeys (Email l)
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Example}
  \begin{lstlisting}
data Label = Home | Work
data AddrKeys = Name | Phone Label | Email Label

data SLabel :: Label -> *
data SAddrKeys :: AddrKeys -> *~\pause~

data ElAddr :: (TyFun AddrKeys *) -> * where
  ElAddr :: ElAddr el ~\pause~

type instance ElAddr $ Name = String
type instance ElAddr $ (Phone l) = [Nat]
type instance ElAddr $ (Email l) = String

type AddrRec rs = Rec ElAddr rs
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Sugared example}
  \begin{lstlisting}
import Data.Singletons as S~\pause~

data Label = Home | Work
data AddrKeys = Name | Phone Label | Email Label
S.genSingletons [ ''Label, ''AddrKeys ]~\pause~

makeUniverse ''AddrKeys "ElAddr"~\pause~

type instance ElAddr $ Name = String
type instance ElAddr $ (Phone l) = [Nat]
type instance ElAddr $ (Email l) = String

type AddrRec rs = Rec ElAddr rs
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Example records}
  \begin{lstlisting}
bob :: AddrRec [Name, Email Work]
bob = SName =: "Robert W. Harper"
    <+> SEmail SWork =: "rwh@cs.cmu.edu"~\pause~

jon :: AddrRec [Name, Email Work, Email Home]
jon = SName =: "Jon M. Sterling"
   <+> SEmail SWork =: "jon@fobo.net"
   <+> SEmail SHome =: "jon@jonmsterling.com"
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Recovering HList}\pause
  \begin{lstlisting}
data Id :: (TyFun k k) -> * where
type instance Id $ x = x~\pause~

type HList rs = Rec Id rs~\pause~

ex :: HList [Int, Bool, String]
ex = 34 :& True :& "vinyl" :& RNil
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Validating records}
  \begin{lstlisting}
validateName :: String -> Either Error String
validateEmail :: String -> Either Error String
validatePhone :: [Nat] -> Either Error [Nat]
  \end{lstlisting}
  \pause
  \centerline{\textit{*unnnnnhhh...*}}
  \pause
  \begin{lstlisting}
validateContact
  :: AddrRec [Name, Email Work]
  -> Either Error (AddrRec [Name, Email Work])
  \end{lstlisting}
\end{frame}

\begin{frame}
  \centerline{\textbf{Welp.}}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Effects inside records}
  \begin{lstlisting}
data Rec :: (TyFun k * -> *) -> [k] -> * where
  RNil :: Rec el '[]
  (:&) :: !(el $ r) -> !(Rec el rs) -> Rec el (r ': rs)
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Effects inside records}
  \begin{lstlisting}
data Rec :: (TyFun k * -> *) -> (* -> *) -> [k] -> * where
  RNil :: Rec el f '[]
  (:&) :: !(f (el $ r)) -> !(Rec el f rs) -> Rec el f (r ': rs)
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Effects inside records}
  \begin{lstlisting}
data Rec :: (TyFun k * -> *) -> (* -> *) -> [k] -> * where
  RNil :: Rec el f '[]
  (:&) :: !(f (el $ r)) -> !(Rec el f rs) -> Rec el f (r ': rs)~\pause~

(=:) : Applicative f => sing r -> el $ r -> Rec el f '[r]
k =: x = pure x :& RNil~\pause~

(<-:) : sing r -> f (el $ r) -> Rec el f '[r]
k <-: x = x :& RNil
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Compositional validation}
  \begin{lstlisting}
type Validator a = a -> Either Error a
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Compositional validation}
  \begin{lstlisting}
newtype Lift o f g x = Lift { runLift :: f x `o` g x }
type Validator = Lift (->) Identity (Either Error)
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Compositional validation}
  \begin{lstlisting}
newtype Lift o f g x = Lift { runLift :: f x `o` g x }
type Validator = Lift (->) Identity (Either Error)~\pause~

validateName :: AddrRec Validator '[Name]
validatePhone :: forall l. AddrRec Validator '[Phone l]
validateEmail :: forall l. AddrRec Validator '[Email l]~\pause~

type TotalContact =
  [ Name, Email Home, Email Work
  , Phone Home, Phone Work ]~\pause~

validateContact :: AddrRec Validator TotalContact
validateContact = validateName
                <+> validateEmail <+> validateEmail
                <+> validatePhone <+> validatePhone
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Record effect operators}\pause
  \begin{lstlisting}
(<<*>>) :: Rec el (Lift (->) f g) rs -> Rec el f rs -> Rec el g rs~\pause~

rtraverse :: Applicative h =>
  (forall x. f x -> h (g x)) ->
  Rec el f rs -> h (Rec el g rs)~\pause~

rdist :: Applicative f => Rec el f rs -> f (Rec el Identity rs)
rdist = rtraverse (fmap Identity)
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Compositional validation}
  \begin{lstlisting}
bob :: AddrRec [Name, Email Work]
validateContact :: AddrRec Validator TotalContact~\pause~

bobValid :: AddrRec (Either Error) [Name, Email Work]
bobValid = cast validateContact <<*>> bob~\pause~

validBob :: Either Error (AddrRec Identity [Name, Email Work])
validBob = rdist bobValid
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Laziness as an effect}\pause

  \begin{lstlisting}
newtype Identity a = Identity { runIdentity :: a }
data Thunk a = Thunk { unThunk :: a }~\pause~

type PlainRec el rs = Rec el Identity rs~\pause~
type LazyRec el rs = Rec el Thunk rs
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Concurrent records with Async}\pause

  \begin{lstlisting}
fetchName :: AddrRec IO '[Name]
fetchName = SName <-: runDB nameQuery ~\pause~

fetchWorkEmail :: AddrRec IO '[Email Work]
fetchWorkEmail = SEmail SWork <-: runDB emailQuery ~\pause~

fetchBob :: AddrRec IO [Name, Email Work]
fetchBob = fetchName <+> fetchWorkEmail
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Concurrent records with Async}\pause

  \begin{lstlisting}
newtype Concurrently a
  = Concurrently { runConcurrently :: IO a }~\pause~

(<<map>>) :: (forall a. f a -> g a) -> Rec el f rs -> Rec el g rs~\pause~

bobConcurrently :: Rec el Concurrently [Name, Email Work]
bobConcurrently = Concurrently <<map>> fetchBob~\pause~

concurrentBob :: IO (PlainRec el [Name, Email Work])
concurrentBob = runConcurrently (rdist bobConcurrently)
  \end{lstlisting}
\end{frame}

\begin{frame}[fragile]
  \centerline{Type Theoretic Semantics for Records}
\end{frame}

\begin{frame}
  \frametitle{Universes \`a la Tarski}\pause
  \begin{itemize}
    \item A type $\mathcal{U}$ of \textbf{codes} for types.
      \pause
    \item Function $El_\mathcal{U} : \mathcal{U}\to\Type$.
      \pause
      \[
        \infer{
          \Gamma\vdash El_\mathcal{U}(s) : \Type
        }{
          \Gamma\vdash s : \mathcal{U}
        }
      \]
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Universes \`a la Tarski}
  \begin{center}
    \includegraphics[width=2.8in]{universe-empty.pdf}
  \end{center}
\end{frame}

\begin{frame}
  \frametitle{Universes \`a la Tarski}
  \begin{center}
    \includegraphics[width=2.8in]{universe-embedded.pdf}
  \end{center}
\end{frame}

\begin{frame}
  \frametitle{Universes \`a la Tarski}
  \begin{center}
    \includegraphics[width=2.8in]{universe-populated.pdf}
  \end{center}
\end{frame}

\begin{frame}
  \frametitle{Universes \`a la Tarski}
  \begin{center}
    \includegraphics[width=2.8in]{universe-interpretation.pdf}
  \end{center}
\end{frame}

\begin{frame}
  \frametitle{Records as products}
  \pause
  \only<2>{
    Records: the product of the image of $El_\mathcal{U}$ in $\Type$ restricted to a subset of $\mathcal{U}$.
  }
  \only<3>{
    \begin{center}
      \includegraphics[width=2.8in]{universe-interpretation.pdf}
    \end{center}
  }
  \only<4>{
    \begin{center}
      \includegraphics[width=2.8in]{universe-product.pdf}
    \end{center}
  }
\end{frame}

\def\container{\mathsf{container}}
\newcommand\mkcon[2]{#1\triangleleft#2}

\begin{frame}
  \frametitle{Vinyl: beyond records?}\pause
  Records and corecords are finite products and sums respectively.\pause
  \[
    \begin{aligned}
      \mathsf{Rec}(El_\mathcal{U}; F; rs)
      &:\equiv \prod_{\mathcal{U}|_{rs}}F\circ El_\mathcal{U}\\\pause
      \mathsf{CoRec}(El_\mathcal{U}; F; rs)
      &:\equiv \sum_{\mathcal{U}|_{rs}}F\circ El_\mathcal{U}\\\pause
      \mathsf{Data}(El_\mathcal{U}; F; rs)
      &:\equiv \Wtype_{\mathcal{U}|_{rs}}F\circ El_\mathcal{U}\\\pause
      \mathsf{Codata}(El_\mathcal{U}; F; rs)
      &:\equiv \Mtype_{\mathcal{U}|_{rs}}F\circ El_\mathcal{U}
    \end{aligned}
  \]
\end{frame}

\begin{frame}
  \frametitle{Vinyl: beyond records?}
  \only<1>{
    \[ \mkcon{\left(\mathcal{U}|_{rs}\right)}{\left(F\circ El_\mathcal{U}\right)} \]
  }
  \only<2>{
    \[ \left\llbracket\mkcon{\left(\mathcal{U}|_{rs}\right)}{\left(F\circ El_\mathcal{U}\right)}\right\rrbracket_\Pi \]
  }
  \only<3>{
    \[ \left\llbracket\mkcon{\left(\mathcal{U}|_{rs}\right)}{\left(F\circ El_\mathcal{U}\right)}\right\rrbracket_\text{W} \]
  }
  \only<4>{
    \[ \left\llbracket\mkcon{\left(\mathcal{U}|_{rs}\right)}{\left(F\circ El_\mathcal{U}\right)}\right\rrbracket_\text{M} \]
  }
\end{frame}

\begin{frame}
  \frametitle{Presheaves}\pause

  A presheaf on some space $X$ is a functor
  $\mathcal{O}(X)^{\mathrm{op}}\to\mathbf{Type}$, where $\mathcal{O}$ is the
  category of open sets of $X$ for whatever topology you have chosen.
\end{frame}

\begin{frame}
  \frametitle{Topologies on some space $X$}\pause

  \begin{itemize}
    \item What are the open sets on $X$?\pause
    \item The empty set and $X$ are open sets\pause
    \item The union of open sets is open\pause
    \item Finite intersections of open sets are open
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Records are presheaves}\pause

  \begin{itemize}
    \item Let $\mathcal{O} = \mathcal{P}$, the discrete topology\pause
    \item Then records on a universe $X$ give rise to a presheaf $\mathcal{R}$: subset inclusions are taken to casts from larger to smaller records
  \end{itemize}
  \pause

  \[
    \begin{aligned}
      \text{for } U\in\mathcal{P}(X)\quad \mathcal{R}(U) &:\equiv \prod_U El_X|_U : \mathbf{Type}\\ \pause
      \text{for } i : V\hookrightarrow U\quad \mathcal{R}(i) &:\equiv \mathsf{cast} : \mathcal{R}(U)\to\mathcal{R}(V)
    \end{aligned}
  \]
\end{frame}

\begin{frame}[fragile]
  \frametitle{Records are sheaves}\pause

  For a cover $U = \bigcup_i U_i$ on $X$, then:\\
  \medskip

  \only<2>{
    \begin{tikzpicture}[node distance=3.5cm, auto]
      \node (FU) {$\mathcal{R}(U)$};
      \node (PFUi) [right of=FU] {$\prod_i\mathcal{R}(U_i)$};
      \node (PFUij) [right of=PFUi] {$\prod_{i,j}\mathcal{R}(U_i\cap U_j)$};

      \draw[->] (FU) to node {$e$} (PFUi);
      \draw[transform canvas={yshift=1mm}][->] (PFUi) to node {$p$} (PFUij);
      \draw[transform canvas={yshift=-1mm}][->] (PFUi) to node [swap] {$q$} (PFUij);
    \end{tikzpicture}\\
    is an equalizer, where
  }
  \only<3>{
    \begin{tikzpicture}[node distance=3.5cm, auto]
      \node (FU) {$\mathcal{R}(U)$};
      \node (PFUi) [right of=FU] {$\prod_i\mathcal{R}(U_i)$};
      \node (PFUij) [right of=PFUi] {$\prod_{i,j}\mathcal{R}(U_i\cap U_j)$};
      \node (G) [below of=PFUi] {$\Gamma$};

      \draw[->] (FU) to node {$e$} (PFUi);
      \draw[->] (G) to node [swap] {$m$} (PFUi);
      \draw[->, dashed] (G) to node {$!u$} (FU);
      \draw[transform canvas={yshift=1mm}][->] (PFUi) to node {$p$} (PFUij);
      \draw[transform canvas={yshift=-1mm}][->] (PFUi) to node [swap] {$q$} (PFUij);
    \end{tikzpicture}\\
    where
  }

  \[
    \begin{aligned}
      e &= \lambda r. \lambda i.\ \mathsf{cast}_{U_i}(r)\\
      p &= \lambda f. \lambda i. \lambda j.\ \mathsf{cast}_{U_i\cap U_j}(f(i))\\
      q &= \lambda f. \lambda i. \lambda j.\ \mathsf{cast}_{U_i\cap U_j}(f(j))\\
    \end{aligned}
  \]
\end{frame}

\begin{frame}
  \frametitle{Records with non-trivial topology}\pause
  \[
    \begin{aligned}
      \mathsf{NameType} &:\equiv \{ F, M, L \}\\\pause
      \mathcal{A} &:\equiv \{ \mathsf{Name}[t] \mid t\in\mathsf{NameType}\}
        \cup
        \{ \mathsf{Phone}[\ell] \mid \ell\in\mathsf{Label} \}\\\pause
      El_\mathcal{A} &:\equiv \lambda\_. \mathbf{String}\\\pause
      T &:\equiv \{ U\in\mathcal{P}(\mathcal{A}) \mid \mathsf{Name}[M]\in U\\&\hspace{90pt}\Rightarrow \{\mathsf{Name}[F],\mathsf{Name}[L]\}\subseteq U\}\\\pause
      ex &: \mathcal{R}_T(\{\mathsf{Name}[t]\mid t\in\mathsf{NameType}\})\\
      ex &:\equiv
        \{\mathsf{Name}[F]\mapsto \text{"Robert"};\\
          &\qquad \mathsf{Name}[M]\mapsto\text{"W"};\\
          &\qquad \mathsf{Name}[L]\mapsto\text{"Harper"}\}\\\pause
      \color{red}{nope} &: \color{red}{\mathcal{R}_T(\{\mathsf{Name}[M],\mathsf{Phone}[Work]\})}\\
      \color{red}{nope} &:\equiv\color{red}{\{\mathsf{Name}[M]\mapsto\text{"W"};}\\
          &\qquad \color{red}{\mathsf{Phone}[Work]\mapsto\text{"5555555555"}\}}
    \end{aligned}
  \]
\end{frame}

\begin{frame}
  \frametitle{Future work}\pause
  \begin{itemize}
    \item Complete: formalization of records with topologies as presheaves in Coq\pause
    \item In Progress: formalization of records as sheaves\pause
    \item Future: extension to \emph{dependent} records using extensional type theory and realizability (Nuprl, MetaPRL)
  \end{itemize}
\end{frame}

\begin{frame}
  \centerline{\textbf{Questions}}
\end{frame}

\end{document}