\documentclass{beamer}

%include lhs2TeX.fmt
%include polycode.fmt

\usetheme{uucs}
\usepackage{tikz}
\usepackage{textpos}

\usetikzlibrary{trees,arrows,decorations,shapes,fit,backgrounds}

\pgfdeclarelayer{background}
\pgfsetlayers{background,main}

\author{Arie Middelkoop}
\title{Breadth-first Evaluation of Catamorphisms}

\institute{%
  Dept.\ of Information and Computing Sciences, Utrecht University\\%
  P.O.\ Box 80.089, 3508 TB Utrecht, The Netherlands\\%
  Web pages: \url{http://www.cs.uu.nl/wiki/Center}}
\date{HUG Sept '10}

%format tau = "\tau"
%format tau1
%format tau2
%format tau3
%format tau4
%format tau5

%format <|> = "<\!\!|\!\!>"
%format <#> = "<\!\!|\!\!>"
%format <*> = "<\!\!\!*\!\!\!>"
%format <$> = "<\!\!\$\!\!>"
%format <=> = "\Longleftrightarrow"
%format forall = "\forall"

\begin{document}

\frontmatter

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

\mainmatter

\begin{frame}
  \frametitle{Introduction}

  \begin{itemize}
  \item Computations over data types with alternatives
  \item Lazy evaluation
  \item Breadth-first evaluation
  \item @http://www.cs.uu.nl/~ariem/Labyrinth.hs@
  \end{itemize}
  
  \begin{center}
  \begin{tikzpicture}
    [ attr/.style={rectangle, minimum size=1mm, node distance=5mm, very thick, top color=uuxred, bottom color=uuxred,font=\tiny} ]
    \node(A){A}
      child {
        node(B){B}
          child {
            node(C){C}
          }
          child {
            node(D){D}
              child {
                node(E){E}
              }
              child {
                node(F){F}
              }
          }
      }
      child {
        node(G){G}
      };
      \pause
      \node[attr,right of=A](A1){};
      \node[attr,right of=B]{};
      \node[attr,right of=C]{};
      \node[attr,right of=D]{};
      \node[attr,right of=E]{};
      \node[attr,right of=F]{};
      \node[attr,right of=G]{};
      \pause
      \node[right of=A1, xshift=10mm](A2){|Inh N -> Syn N|};
      \pause
      \node[below of=A2, xshift=4mm, yshift=5mm]{|(tau1, tau2) -> (tau3, tau4, tau5)|};
      \pause
      \node[below of=A, yshift=3mm]{or};
      \node[below of=D, yshift=3mm]{or};
  \end{tikzpicture}
  \end{center}
\end{frame}


\section*{Breadth-first evaluation via a monad with non-deterministic choice}

\begin{frame}
  \frametitle{Stuck In A Labyrinth}
  
  \includegraphics{maze}
  \includegraphics{lostprofessors}
\end{frame}

\begin{frame}
  \frametitle{Compute A Route To The Exit}
  
  \begin{center}
  \begin{code}
  findRoute :: Labyrinth -> Path
  findRoute = ... -- to be implemented
  
  data Path  = Forward Dir Path | End
  data Dir   = North | East | South | West deriving Enum
  \end{code}
  \end{center}
  \pause
  Assuming we restrict ourselves to simple paths (i.e. no loops), can we already
  return portions of the path before we reach the exit?
\end{frame}

\begin{frame}
  \frametitle{Non-deterministic Monad With State On Top}
  
  \begin{code}
  type Lab a = NonT (State LabState) a
  data LabState
    = LS  { ls_lab    :: Array Pos Bool    -- ``labyrinth grid''
          , ls_end    :: Pos               -- goal position
          , ls_cur    :: Pos               -- current position
          , ls_trail  :: Set Pos           -- previous positions
          , ls_path   :: (Path -> Path)    -- path so far
         }
  \end{code}

  \begin{code}
  run :: Lab () -> Path
  run m = ls_path sFin End
    where  sIn = LS  { ls_lab   = ... ,       ls_cur   = (0,0)
                     , ls_end   = (100,100),  ls_trail = empty
                     , ls_path  = id }
           sFin = execState (evalNonT m) sIn
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Search Strategy}
  
  \begin{code}
  search :: Lab ()
  search  =    finished
          <|>  non  [ do  move d
                          search
                    | d <- [North .. West] ]
  
  finished :: Lab ()
  finished = do  p <- gets ls_cur
                 e <- gets ls_end
                 if p == e
                   then return ()
                   else fail "not at the end yet"

  non :: [Lab a] -> Lab a
  non []      = empty
  non (x:xs)  = x <|> non xs
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Moving A Step}

  \begin{code}
  move :: Dir -> Lab ()
  move d = do
    p  <- gets ls_cur
    let p' = forward d p
    a  <- gets ls_lab
    if a ! p'
      then do
        ps <- gets ls_trail
        if p' `member` ps
          then fail "already been there"
          else modify (\s -> s  {
               ls_cur   = p'
            ,  ls_trail = insert p' (ls_trail s)
            ,  ls_path  = Forward d . ls_path s })
      else fail "hit against the wall"
  \end{code}
\end{frame}

\section*{Implementation: the monad as catamorphism}

\begin{frame}
  \frametitle{Data-type Representing The Monad}
  
  \begin{code}
  data NonM a where
    Return  :: a -> NonM a
    Bind    :: NonM b -> (b -> NonM a) -> NonM a
    Alt     :: NonM a -> NonM a -> NonM a
    Fail    :: String -> NonM a
    Work    :: NonM a -> NonM a
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Algebra For The Data-type}
  
  \begin{code}
  data NonAlg c a = NonAlg
      { alg_return  ::  a -> Sem Info (Non c a)
      , alg_bind    ::  forall b . Sem Info (Non c b) ->
                        (b -> Sem Info (Non c a)) ->
                        Sem Info (Non c a)
      , alg_alt     ::  Sem Info (Non c a) ->
                        Sem Info (Non c a) ->
                        Sem Info (Non c a)
      , alg_fail    ::  String -> Sem Info (Non c a)
      , alg_work    ::  Sem Info (Non c a) -> 
                        Sem Info (Non c a) }
  \end{code}
  \begin{code}
  type Sem i n   = Inh n -> Comp i n
  type Comp i n  = Syn n  -- for now
  data Info      = SomeWork | Failed String
  \end{code}
\end{frame}

\begin{frame}
   \frametitle{Fold For The Data-type}
   
   \begin{code}
   foldNon :: (forall b d . NonAlg d b)  -> Non c a
                                         -> Sem Info (Non c a)
   foldNon alg (Return x)  = alg_return alg x
   foldNon alg (Bind m f)  = alg_bind alg  (foldNon alg m)
                                           (foldNon alg . f)
   foldNon alg (Alt l r)   = alg_alt alg   (foldNon alg l)
                                           (foldNon alg r)
   foldNon alg (Fail s)    = alg_fail alg s
   foldNon alg (Work m)    = alg_work alg (foldNon alg m)

   nonAlg :: NonAlg c a
   nonAlg = NonAlg  sem_Return sem_Bind
                    sem_Alt sem_Fail sem_Work
   \end{code}
\end{frame}

\begin{frame}
  \frametitle{Direct Construction of Semantic Functions}
  
  \begin{code}
  newtype N c a = N (Sem Info (Non c a))

  instance Monad (N c) where
    return       = N . sem_Return
    (N m) >>= f  = N (sem_Bind m ((\(N m') -> m') . f))
    fail         = N . sem_Fail

  instance Applicative (N c) where
    pure x   = return x
    p <*> q  = p >>= \f -> (q >>= (return . f))

  instance Alternative (N c) where
    empty            = N (sem_Fail "empty")
    (N l) <|> (N r)  = N (sem_Alt l r)
  
  instance Functor (N c) ...
  \end{code}
\end{frame}

\section*{Implementation: the semantic functions}

\begin{frame}
  \frametitle{Inputs and Outputs: Attributes}
  
  \begin{code}
  type Sem i n  = Inh n -> Comp i n
  type Comp i n = Syn n  -- for now

  data instance Inh (Non c a) = Inh { cont :: Rem a c }
  data instance Syn (Non c a) = Syn { res :: c }
  \end{code}
  
  \begin{code}
  -- represents what follows |p| in: |((p >>= q) >>= r) >>= s|
  -- takes an |a|, after evaluation produces a |b|
  data Rem a b where
    Done ::  Rem a a
    More ::  (a -> Sem Info (Non b c))
             -> Rem c b -> Rem a b
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Lazy Evaluation of the Catamorphism}
  
  \begin{code}
  evalNon :: N a a -> a
  evalNon (N m) = res syn
    where  inh = Inh { cont = Done }
           sem = invoke m inh
           syn = lazyEval sem
  \end{code}
  
  \begin{code}
  invoke (Sem f) = f
  lazyEval = id -- for now
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{At The Leafs: Apply Remaining Tasks}
  
  \begin{code}
  sem_Leaf :: Sem Info (Non a a) -> Sem Info (Non c a)
  sem_Leaf = ... -- omitted
  \end{code}
  
  \begin{code}
  sem_Fail s    = sem_Leaf (sem_Fail' s)
  sem_Return x  = sem_Leaf (sem_Return' x)
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{The |return| Combinator}
  
  \begin{code}
  sem_Return v =
    sem_Leaf $ Sem $ \inh -> Syn { res = v }
  \end{code}
  
  Given:
  \begin{code}
  final :: Syn n -> Comp i n
  final = id
  \end{code}
  
  Rewrite to:
  \begin{code}
  sem_Return v = sem_Leaf $ Sem $ \inh ->
    final $ Syn { res = v }
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{The |fail| Combinator}
  
  \begin{code}
  sem_Fail s =
    sem_Leaf $ Sem $ \inh ->
      Syn { res = error ("error: " ++ s) }
  \end{code}
  
  \begin{code}
  inject :: i -> Comp i n
  inject = undefined
  
  resume :: Comp i n -> (Syn n -> Comp i m) -> Comp i m
  resume x f = f x
  \end{code}
  
  \begin{code}
  sem_Fail s =
    sem_Leaf $ Sem $ \inh ->
      resume (inject $ Failed s) $ \_ ->
          final $ Syn { res = error ("error: " ++ s) }
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{The Bind Combinator}
  
  \begin{code}
  sem_Bind :: Sem Info (Non c b)
    -> (b -> Sem Info (Non c a)) -> Sem Info (Non c a)
  sem_Bind (Sem m) f = Sem $ \inh ->
        let  mInh  = Inh { cont = More f (cont inh) }
             mSyn  = m mInh
        in Syn { res = res mSyn }
  \end{code}
  
  \begin{code}
  invoke :: Sem i n -> Inh n -> Comp i n
  invoke (Sem f) = f

  sem_Bind m f
    = Sem $ \inh ->
        let  mInh  = Inh { cont = More f (cont inh) }
             mComp = invoke m mInh
        in resume mComp $ \mSyn ->
             final $ Syn { res = res mSyn }
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{The |work| Combinator}
  
  Another example of a combinator that injects an |Info|:
  \begin{code}
  sem_Work k
    = Sem $ \inh ->
        resume (inject SomeWork) $ \_ ->
          let  kInh = Inh { cont = cont inh }
               kComp = invoke k kInh
          in resume kComp $ \kSyn ->
               final $ Syn { res = res kSyn }
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{The Or Combinator}
  
  \begin{code}
  sem_Alt (Sem l) (Sem r) = Sem $ \inh ->
    let  lInh  = Inh { cont = cont inh }
         lSyn  = l lInh 
        
         rInh  = Inh { cont = cont inh }
         rSyn  = r rInh
         
         kSyn  = best lSyn rSyn
    in Syn { res = res kSyn }
  \end{code}
  
  
  \begin{code}
  sem_Alt l r = Sem $ \inh ->
    let  lInh  = Inh { cont = cont inh }
         lComp = invoke l lInh

         rInh  = Inh { cont = cont inh }
         rComp = invoke r rInh

         kComp = best lComp rComp
    in resume kComp $ \kSyn -> 
         final $ Syn { res = res kSyn }
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{The |best| Dilemma}
  
  \begin{code}
  best :: Comp i n -> Comp i n -> Comp i n
  best l r = l -- or rather r??
  \end{code}
\end{frame}


\section*{Evaluation Strategies}

\begin{frame}
  \frametitle{Recap}
  
  \begin{code}
  newtype Sem i n = Sem (Inh n -> Comp i n)
  type Comp i n = Syn n  -- for now
  data family Inh n
  data family Syn n
  \end{code}
  
  \begin{code}
  invoke  :: Sem i n -> Inh n -> Comp n
  resume  :: Comp i n -> (Syn n -> Comp i m) -> Comp i m
  final   :: Syn n -> Comp i n
  inject  :: i -> Comp i n
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Depth-first Evaluation}
  
  \begin{code}
  data Comp i n
    =  Final (Syn n)
    |  Info i
  \end{code}
  
  \begin{code}
  invoke (Sem f) inh = seq inh (f inh)
  
  resume (Final syn) f  = seq syn (f syn)
  resume (Info _) f     = f undefined
  
  inject i = Info i
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Illustration}
  
  \begin{center}
  \begin{tikzpicture}
    [ attr/.style={rectangle, minimum size=1mm, node distance=5mm, very thick, top color=uuxred, bottom color=uuxred,font=\tiny} ]
    \node(A){A}
      child {
        node(B){B}
          child {
            node(C){C}
          }
          child {
            node(D){D}
              child {
                node(E){E}
              }
              child {
                node(F){F}
              }
          }
      }
      child {
        node(G){G}
      };
      \node[attr,right of=A](A1){};
      \node[attr,right of=B]{};
      \node[attr,right of=C]{};
      \node[attr,right of=D]{};
      \node[attr,right of=E]{};
      \node[attr,right of=F]{};
      \node[attr,right of=G]{};
  \end{tikzpicture}
  \end{center}
\end{frame}

\section*{Breadth-first Implementation}

\begin{frame}
  \frametitle{The Real |Comp| Data-type}
  
  \begin{code}
  data Comp i n where
    Pending  :: Parents i m n -> Comp i m -> Comp i n
    Final    :: Syn n -> Comp i n
    Info     :: i -> Comp i n -> Comp i n
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Illustration}
  
  \begin{center}
  \begin{tikzpicture}
    [ attr/.style={rectangle, minimum size=1mm, node distance=5mm, very thick, top color=uuxred, bottom color=uuxred,font=\tiny} ]
    \node(A){A}
      child {
        node(B){B}
          child {
            node(C){C}
          }
          child {
            node(D){}
          }
      }
      child {
        node(G){}
      };
      \node[attr,right of=A]{};
      \node[attr,right of=B]{};
      \node[attr,right of=C]{};
  \end{tikzpicture}
  \end{center}
\end{frame}

\begin{frame}
  \frametitle{Parents Of The Currently Evaluating Node}
  
  \begin{code}
  data Parents i m n where
    Cont :: Node i m k -> Parents i k n -> Parents i m n
    Root :: Parents i n n
  \end{code}
  
  \begin{code}
  newtype Node i m n = Node (Syn m -> Comp i n)
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Lazy Evaluation}
  
  \begin{code}
  lazyEval :: Comp i a -> Syn a
  lazyEval (Pending stack r)  = evalParents stack
                                  (lazyEval r)
  lazyEval (Final v)          = v
  lazyEval (Info _ r)         = lazyEval r
  \end{code}

  \begin{code}
  evalParents :: Parents i m n -> Syn m -> Syn n
  evalParents Root v = v
  evalParents (Cont (Node f) c) v = evalParents c
                                      (lazyEval (f v))
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Step-wise Evaluation}
  
  \begin{code}
  data Outcome i a
    =  Fin  (Syn a)
    |  Step i (Comp i a)
  \end{code}
  
  \begin{code}
  oneStep :: Comp i a -> Outcome i a
  oneStep (Pending stack r)
    = case oneStep r of
        Fin v     -> oneStep (reduceParent stack v)
        Step i r' -> Step i (Pending stack r')
  oneStep (Final v)  = Fin v
  oneStep (Info i r) = Step i r

  reduceParent :: Parents i m n -> Syn m -> Comp i n
  reduceParent Root v = Final v
  reduceParent (Cont (Node f) c) v = Pending c (f v)
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Info-step Injection}
  
  \begin{code}
  data instance Syn Inject = Syn_Inject {}
  
  inject :: i -> Comp i Inject
  inject i = info i $ final $ Syn_Inject {}
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{The |best| function}
  
  \begin{code}
  best l r = best' (oneStep l) (oneStep r)
    where
      best' (Fin synL) _  = final synL
      best' _ (Fin synR)  = final synR
      best' (Step infoL remL) (Step infoR remR)
        = case infoR of
            Failed _ ->  info infoL remL
            SomeWork ->  case infoL of
              Failed _ ->  info infoR remR
              SomeWork ->  info SomeWork
                (best remL remR)
  \end{code}
\end{frame}

\section*{Conclusion}

\begin{frame}
  \frametitle{Wrapping-Up}
  
  \begin{itemize}
  \item Relatively easy to add breadth-first computation to your programs
  \item Interesting combination between strict and lazy evaluation
  \item Grouping of contents in |resume|-blocks can be done automatically
        for ordered attribute grammars
  \end{itemize}
  
  \begin{itemize}
  \item Queston: What are good use-cases?
  \item ... that also require `online' results?
  \end{itemize}
  
  \begin{itemize}
  \item If we forget about lazy evaluation. What about a monadic
        evaluation, such that we can think about sharing.
  \end{itemize}
  
\end{frame}

\end{document}