bft-hyperfunction-presentation.markdown

---

title: Hyperfunctions, Breadth-First Traversals, and Search author: Oisín Kidney patat: theme: codeBlock: [vividBlack] code: [vividBlack] incrementalLists: true eval: ruby: command: irb --noecho --noverbose fragment: true replace: false

...

Hyperfunctions

Hyperfunctions

newtype a -&> b = Hyp { invoke :: (b -&> a) -> b }

• First defined in:

  Launchbury, John, Sava Krstic, and Timothy E. Sauerwein. ‘Zip Fusion with Hyperfunctions’, 2000. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.4961.

• Although similar types have shown up before then:

  Hofmann, Martin. Letter to types@uk.ac.gla.dcs. ‘Non Strictly Positive Datatypes in System F’, 15 February 1993. https://www.seas.upenn.edu/~sweirich/types/archive/1993/msg00027.html.

• Not a huge amount of literature on them.

Expanding out the type

type a -&> b = (b -&> a) -> b

Expanding out the type

type a -&> b = (b -&> a) -> b
             = ((a -&> b) -> a) -> b

Expanding out the type

type a -&> b = (b -&> a) -> b
             = ((a -&> b) -> a) -> b
             = (((b -&> a) -> b) -> a) -> b

Expanding out the type

type a -&> b = (b -&> a) -> b
             = ((a -&> b) -> a) -> b
             = (((b -&> a) -> b) -> a) -> b
             = ((((a -&> b) -> a) -> b) -> a) -> b

• Infinitely left-nested function.

• All a is always negative, b is always positive.

Fusing Zip

zip []     ys     = []
zip (x:xs) []     = []
zip (x:xs) (y:ys) = (x,y) : zip xs ys

Fusing Zip

zip = foldr f b
  where
    b      ys     = []
    f x xs []     = []
    f x xs (y:ys) = (x,y) : xs ys

Fusing Zip

zip xs ys = foldr xf xb xs (foldr yf yb ys)
  where
    xb      _  = []
    xf x xk yk = yk x xk
    
    yb      _ _  = []
    yf y yk x xk = (x,y) : xk yk

Fusing Zip

zip xs ys = xr xs (yr ys)
  where
    xr = foldr xf xb
    xb      _  = []
    xf x xk yk = yk x xk

    yr = foldr yf yb
    yb      _ _  = []
    yf y yk x xk = (x,y) : xk yk

>>> zip [1,2] [3,4]

Fusing Zip

zip xs ys = xr xs (yr ys)
  where
    xr = foldr xf xb
    xb      _  = []
    xf x xk yk = yk x xk

    yr = foldr yf yb
    yb      _ _  = []
    yf y yk x xk = (x,y) : xk yk

>>> xr [1,2] (yr [3,4])

Fusing Zip

zip xs ys = xr xs (yr ys)
  where
    xr = foldr xf xb
    xb      _  = []
    xf x xk yk = yk x xk

    yr = foldr yf yb
    yb      _ _  = []
    yf y yk x xk = (x,y) : xk yk

>>> xf 1 (xr [2]) (yr [3,4])

Fusing Zip

zip xs ys = xr xs (yr ys)
  where
    xr = foldr xf xb
    xb      _  = []
    xf x xk yk = yk x xk

    yr = foldr yf yb
    yb      _ _  = []
    yf y yk x xk = (x,y) : xk yk

>>> yr [3,4] 1 (xr [2])

Fusing Zip

zip xs ys = xr xs (yr ys)
  where
    xr = foldr xf xb
    xb      _  = []
    xf x xk yk = yk x xk

    yr = foldr yf yb
    yb      _ _  = []
    yf y yk x xk = (x,y) : xk yk

>>> yf 3 (yr [4]) 1 (xr [2])

Fusing Zip

zip xs ys = xr xs (yr ys)
  where
    xr = foldr xf xb
    xb      _  = []
    xf x xk yk = yk x xk

    yr = foldr yf yb
    yb      _ _  = []
    yf y yk x xk = (x,y) : xk yk

>>> (1,3) : xr [2] (yr [4])

Fusing Zip

• There is a type error:

• Occurs check: cannot construct the infinite type:
    t0 ~ a -> (t0 -> [(a, b)]) -> [(a, b)]

• This error gives us the signature of the newtype we need:

newtype Zip a b = 
  Zip { runZip :: a -> (Zip a b -> [(a,b)]) -> [(a,b)] }

Fusing Zip

newtype Zip a b = 
  Zip { runZip :: a -> (Zip a b -> [(a,b)]) -> [(a,b)] }

zip :: forall a b. [a] -> [b] -> [(a,b)]
zip xs ys = xz yz
  where
    xz :: Zip a b -> [(a,b)]
    xz = foldr f b xs
      where    
        f x xk yk = runZip yk x xk
        b _ = []
    
    yz :: Zip a b
    yz = foldr f b ys
      where
        f y yk = Zip (\x xk -> (x,y) : xk yk)
        b = Zip (\_ _ -> [])

Fusing Zip

Zip is of course a hyperfunction:

. . .

zip :: forall a b. [a] -> [b] -> [(a,b)]
zip xs ys = invoke xz yz
  where
    xz :: (a -> [(a,b)]) -&> [(a,b)]
    xz = foldr f b xs
      where
        f x xk = Hyp (\yk -> invoke yk xk x)
        b = Hyp (\_ -> [])
    
    yz :: [(a,b)] -&> (a -> [(a,b)]) 
    yz = foldr f b ys
      where
        f y yk = Hyp (\xk x -> (x,y) : invoke xk yk)
        b = Hyp (\_ _ -> [])

Breadth-First Tree Traversal

data Tree a = a :& [Tree a]

bfe :: Tree a -> [a]
bfe t = q [t]
  where
    q ((x :& xs):ts) = x : q (ts ++ xs)
    q [] = []

Breadth-First Tree Traversal

data Tree a = a :& [Tree a]

bfe :: Tree a -> [a]
bfe t = foldr f b [t]
  where
    f (x :& xs) ts = x : foldr f b (ts ++ xs)
    b = []

Breadth-First Tree Traversal

data Tree a = a :& [Tree a]

bfe :: Tree a -> [a]
bfe t = f t b
  where
    f (x :& xs) ts = x : foldr f b (ts ++ xs)
    b = []

Breadth-First Tree Traversal

data Tree a = a :& [Tree a]

bfe :: Tree a -> [a]
bfe t = f t b []
  where
    f (x :& xs) fw bw = x : fw (bw ++ xs)

    b [] = []
    b qs = foldr f b qs []

Breadth-First Tree Traversal

data Tree a = a :& [Tree a]

bfe :: Tree a -> [a]
bfe t = f t b []
  where
    f (x :& xs) fw bw = x : fw (bw ++ xs)

    -- b [] = []
    b qs = foldr f b qs []

Breadth-First Tree Traversal

data Tree a = a :& [Tree a]

bfe :: Tree a -> [a]
bfe t = f t b []
  where
    f (x :& xs) fw bw = x : fw (bw ++ xs)

    b qs = foldr f b qs []

Breadth-First Tree Traversal

foldr :: (a -> b -> b) -> b -> [a] -> b

. . .

type Cayley a = a -> a

. . .

cayley :: (a -> Cayley b) -> [a] -> Cayley b
cayley f xs b = foldr f b xs

. . .

cayley f (xs ++ ys) = cayley f xs . cayley f ys
cayley f []         = id

Breadth-First Tree Traversal

data Tree a = a :& [Tree a]

bfe :: Tree a -> [a]
bfe t = f t b []
  where
    f (x :& xs) fw bw = x : fw (bw ++ xs)

    b qs = foldr f b qs []

Breadth-First Tree Traversal

data Tree a = a :& [Tree a]

bfe :: Tree a -> [a]
bfe t = f t b []
  where
    f (x :& xs) fw bw = x : fw (bw ++ xs)

    b qs = cayley f qs b []

Breadth-First Tree Traversal

data Tree a = a :& [Tree a]

bfe :: Tree a -> [a]
bfe t = f t b b
  where
    f (x :& xs) fw bw = x : fw (bw . cayley f xs)

    b qs = qs b

Breadth-First Tree Traversal

data Tree a = a :& [Tree a]

bfe :: Tree a -> [a]
bfe t = f t b b
  where
    f (x :& xs) fw bw = x : fw (bw . cayley f xs) -- Error

    b qs = qs b

• Occurs check: cannot construct the infinite type:
    a2 ~ (a2 -> c) -> [a1]

Breadth-First Tree Traversal

data Tree a = a :& [Tree a]

bfe :: Tree a -> [a]
bfe t = f t b b
  where
    f (x :& xs) fw bw = x : fw (bw . cayley f xs)

    b qs = qs b -- Error

• Occurs check: cannot construct the infinite type:
    a2 ~ (a2 -> c) -> [a1]

• Occurs check: cannot construct the infinite type:
    t ~ (t -> t0) -> t0

Breadth-First Tree Traversal

data Tree a = a :& [Tree a]

bfe :: Tree a -> [a]
bfe t = f t b b
  where
    f (x :& xs) fw bw = x : fw (bw . cayley f xs)

    b qs = qs b

• Occurs check: cannot construct the infinite type:
    a2 ~ (a2 -> c) -> [a1]

• Occurs check: cannot construct the infinite type:
    t ~ (t -> t0) -> t0

newtype Q a = Q { q :: (Q a -> [a]) -> [a] }

Breadth-First Tree Traversal

data Tree a = a :& [Tree a]

bfe :: Tree a -> [a]
bfe t = q (f t b) e
  where
    f (x :& xs) fw = Q (\bw -> x : q fw (bw . cayley f xs))

    b :: Q a
    b = Q (\k -> k b)
    
    e :: Q a -> [a]
    e (Q q) = q e

newtype Q a = Q { q :: (Q a -> [a]) -> [a] }

Breadth-First Tree Traversal

data Tree a = a :& [Tree a]

bfe :: Tree a -> [a]
bfe t = q (f t b) e
  where
    f (x :& xs) fw = Q (\bw -> x : q fw (bw . cayley f xs))
    
    b :: Q a
    b = Q (\k -> k b)
    
    e :: Q a -> [a]
    e (Q q) = q e







newtype Q a = Q { q :: (Q a -> [a]) -> [a] } -- Fix (Cont [a])

Breadth-First Tree Traversal

data Tree a = a :& [Tree a]

bfe :: Tree a -> [a]
bfe t = q (f t b) e
  where
    f (x :& xs) fw = Q (\bw -> x : q fw (bw . cayley f xs))
    
    b :: Q a
    b = Q (\k -> k b)  -- b k = k b
    
    e :: Q a -> [a]
    e (Q q) = q e      -- e q = q e







newtype Q a = Q { q :: (Q a -> [a]) -> [a] }

Breadth-First Tree Traversal

data Tree a = a :& [Tree a]

bfe :: Tree a -> [a]
bfe t = invoke (f t b) b
  where
    f (x :& xs) fw = Hyp (\bw -> x : invoke fw 
                         (Hyp (invoke bw . cayley f xs)))
    
    b :: Q a
    b = Hyp (\qs -> invoke qs b)









type Q a = [a] -&> [a]

Breadth-First Tree Traversal

These traversals don't terminate; to fix that we can pass in a counter.

. . .

bfe :: Tree a -> [a]
bfe t = invoke (f t e) b 0
  where
    f (x :& xs) fw = Hyp (\bw n -> x : invoke fw 
                                         (Hyp (invoke bw . cayley f xs)) 
                                         (n+1))
    
    b = Hyp (\h -> invoke h b)

    e = Hyp (\h n -> if n == 0 then [] else invoke h e (n-1))

type Q a = (Int -> [a]) -&> (Int -> [a])

. . .

Similar trick in:

Smith, Leon P. ‘Lloyd Allison’s Corecursive Queues: Why Continuations Matter’. The Monad.Reader, 29 July 2009. https://meldingmonads.files.wordpress.com/2009/06/corecqueues.pdf.

Hyperfunctions Aren't Sets

Clear cardinality problems:

$a ↬ b = ((((a ↬ b) → a) → b) → a) → b$

Hyperfunctions Are Not Always Types

. . .

We aren't allowed to define the type in Agda:

. . .

record _↬_ (A : Type) (B : Type) : Type where
  field invoke : (B ↬ A) → B

-- Error: not strictly positive

. . .

And for good reason:

. . .

yes? : ⊥ ↬ ⊥
yes? .invoke h = h .invoke h

no! : (⊥ ↬ ⊥) → ⊥
no! h = h .invoke h

boom : ⊥
boom = no! yes?

Curry's paradox, stackoverflow.com/a/51253757

They're Only Sometimes Types

. . .

A very similar definition prevents the encoding of the paradox:

record _↬_ (A : Type) (B : Type) : Type where
  field invoke : ((A ↬ B) → A) → B

Although this isn't allowed in Agda it perhaps should be:

$vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/$

What can Hyperfunctions do?

. . .

i.e. what instances do they have.

. . .

All these from Edward Kmett's library (hackage.haskell.org/package/hyperfunctions)

And the 2013 paper:

Launchbury, J., S. Krstic, and T. E. Sauerwein. ‘Coroutining Folds with Hyperfunctions’. Electronic Proceedings in Theoretical Computer Science 129 (19 September 2013): 121–35. https://doi.org/10.4204/EPTCS.129.9.

They're A Category

instance Category (-&>) where
  id :: a -&> a
  id = Hyp (\k -> invoke k id)
  
  (.) :: (b -&> c) -> (a -&> b) -> a -&> c
  f . g = Hyp (\k -> invoke f (g . k))

They're a Profunctor

instance Profunctor (-&>) where
  lmap :: (a -> b) -> (b -&> c) -> a -&> c
  lmap f h = Hyp (invoke h . rmap f)
  
  rmap :: (b -> c) -> a -&> b -> a -&> c
  rmap f h = Hyp (f . invoke h . lmap f)

They're a Monad

instance Monad ((-&>) a) where
  m >>= f = Hyp (\k -> invoke (f (invoke m (Hyp (invoke k . (>>=f))))) k)

They Kind of Act Like Streams

. . .

We have the following cons:

push :: (a -> b) -> a -&> b -> a -&> b
push f q = Hyp (\k -> f (invoke k q))

. . .

push f fs . push g gs = push (f . g) (fs . gs)

. . .

And we can run the stream:

run :: a -&> a -> a
run f = invoke f id

BFE Again

bfe :: Tree a -> [a]
bfe = run . f
  where
    f (x :& xs) = push (x:) (foldr ((.) . f) id xs)

. . .

bfe t = run (f t . e) 0
  where
    f (x :& xs) =
      push (\k n -> x : k (n+1)) 
      (foldr ((.) . f) id xs)
      
    e = Hyp (\h n -> if n == 0 then [] else invoke h e (n-1))

HypM

. . .

newtype HypM m a b = HypM { invokeM :: m ((HypM m a b -> a) -> b) }

. . .

bfe t = r (f t e)
  where
    f (x :& xs) fw = 
      HypM (Just (\bw -> x : fromMaybe (\k -> k e) (invokeM fw) 
                 (bw . flip (foldr f) xs)))
    e = HypM Nothing
    r = maybe [] (\k -> k r) . invokeM

Coroutines

. . .

type Producer a b = (a -> b) -&> b
type Consumer a b = b -&> (a -> b)

. . .

type Handlers m i o r = Producer i (m r) -> Consumer o (m r) -> m r

newtype Coroutine i o r m a
  = Co { route :: (a -> Handlers m i o r) -> Handlers m i o r }

Coroutines

yield :: o -> Coroutine i o r m ()
yield x = Co (\k p c -> invoke c (Hyp (\h -> k () p h)) x)

await ::Coroutine i o r m i
await = Co (\k p c -> invoke p (Hyp (\p' x -> k x p' c)))

halt :: m r -> Coroutine i o r m x
halt x = Co (\_ _ _ -> x)

merge :: Coroutine i x r m Void 
      -> Coroutine x o r m Void 
      -> Coroutine i o r m a
merge ix xo = Co (\_ -> route xo absurd . Hyp . route ix absurd)

run :: Coroutine () () r m () -> m r
run xs = route xs (\_ p c -> invoke p c) p c
  where
    p = Hyp (\h -> invoke h p ())
    c = Hyp (\h _ -> invoke h c)

Coroutines

lhs :: Coroutine () Int () IO Void
lhs = do
  putStrLn "L 1"
  putStrLn "L 2"
  yield 1
  putStrLn "L 3"
  yield 2
  putStrLn "L 4"
  halt (pure ())
  
rhs :: Coroutine Int () () IO Void
rhs = do
  putStrLn "R 1"
  x <- await
  putStr "Got : "
  print x
  putStrLn "R 2"
  y <- await
  putStr "Got : "
  print y
  halt (pure ())

Coroutines

lhs :: Coroutine () Int () IO Void    -- >> run (merge lhs rhs)
lhs = do                              -- R 1
  putStrLn "L 1"                      -- L 1
  putStrLn "L 2"                      -- L 2
  yield 1                             -- Got : 1
  putStrLn "L 3"                      -- R 2
  yield 2                             -- L 3
  putStrLn "L 4"                      -- Got : 2
  halt (pure ())

rhs :: Coroutine Int () () IO Void
rhs = do
  putStrLn "R 1"
  x <- await
  putStr "Got : "
  print x
  putStrLn "R 2"
  y <- await
  putStr "Got : "
  print y
  halt (pure ())

Coroutines

• Shivers, Olin, and Matthew Might. ‘Continuations and Transducer Composition’. ACM SIGPLAN Notices 41, no. 6 (11 June 2006): 295–307. https://doi.org/10.1145/1133255.1134016.

• Spivey, Michael. ‘Faster Coroutine Pipelines’. Proceedings of the ACM on Programming Languages 1, no. ICFP (29 August 2017): 5:1-5:23. https://doi.org/10.1145/3110249.

• Pieters, Ruben P., and Tom Schrijvers. ‘Faster Coroutine Pipelines: A Reconstruction’. In Practical Aspects of Declarative Languages, 133–49. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2019. https://doi.org/10.1007/978-3-030-05998-9_9.

Breadth-First Traversals

Level-Order Breadth-First Search

. . .

levels :: Tree a -> [[a]]
levels t = map (map root)
         . takeWhile (not . null) 
         . iterate (concatMap children)
         $ [t]

Level-Order Breadth-First Search

levels :: Tree a -> [[a]]
levels t = map (map root)
         . takeWhile (not . null) 
         . iterate (concatMap children)
         $ [t]

tree =
    1 :&                     --      ┌8
      [ 2 :&                 --    ┌4┤ 
          [ 4 :&             --    │ └9
              [ 8 :& []      --  ┌2┤ 
              , 9 :& []]     --  │ └5
          , 5 :& []]         -- 1┤
      , 3 :&                 --  │   ┌10
          [ 6 :&             --  │ ┌6┤
              [ 10 :& []     --  │ │ └11 
              , 11 :& []]    --  └3┤
          , 7 :& []]]        --    └7

Level-Order Breadth-First Search

levels :: Tree a -> [[a]]
levels t = map (map root)
         . takeWhile (not . null) 
         . iterate (concatMap children)
         $ [t]

tree =
    1 :&                     --      ┌8
      [ 2 :&                 --    ┌4┤ 
          [ 4 :&             --    │ └9
              [ 8 :& []      --  ┌2┤ 
              , 9 :& []]     --  │ └5
          , 5 :& []]         -- 1┤
      , 3 :&                 --  │   ┌10
          [ 6 :&             --  │ ┌6┤
              [ 10 :& []     --  │ │ └11 
              , 11 :& []]    --  └3┤
          , 7 :& []]]        --    └7

>>> levels tree
[[1],[2,3],[4,5,6,7],[8,9,10,11]]

Deriving a Level-Order Breadth-First Search

levels t = map (map root)
         . takeWhile (not . null) 
         . iterate (concatMap children)
         $ [t]

. . .

Step 1: fuse the multiple maps by turning it into an unfold.

map r . takeWhile p . iterate f = unfoldr (\x -> (r x, f x) <$ guard (p x))

Deriving a Level-Order Breadth-First Search

levels :: Tree a -> [[a]]
levels t = unfoldr (\x -> (map root x, concatMap children x) 
                       <$ guard (not (null x)))
         $ [t]

. . .

Step 2: Make the lambda its own function

Deriving a Level-Order Breadth-First Search

levels t = unfoldr alg [t]
  where
    alg x = (map root x, concatMap children x) <$ guard (not (null x))

. . .

Step 3: Inline guard and <$

Deriving a Level-Order Breadth-First Search

levels t = unfoldr alg [t]
  where
    alg [] = Nothing
    alg xs = Just (map root xs, concatMap children xs)

. . .

Step 4: concatMap = concat . map{.haskell}

Deriving a Level-Order Breadth-First Search

levels t = unfoldr alg [t]
  where
    alg [] = Nothing
    alg xs = Just (map root xs, concat (map children xs))

. . .

Step 5: Use second

second :: (a -> b) -> (e, a) -> (e, b)
second f (x, y) = (x, f y)

Deriving a Level-Order Breadth-First Search

levels t = unfoldr alg [t]
  where
    alg [] = Nothing
    alg xs = Just (second concat (map root xs, map children xs))

. . .

Step 6: Hey, there's an unzip!

 (map f xs, map g xs) = unzipWith (f &&& g) xs

(&&&) :: (a -> b) -> (a -> c) -> a -> (b, c)
(f &&& g) x = (f x, g x)

Deriving a Level-Order Breadth-First Search

levels t = unfoldr alg [t]
  where
    alg [] = Nothing
    alg xs = Just (second concat (unzipWith (root &&& children) xs))

. . .

Step 7: Inline unzipWith

unzipWith :: (a -> (b,c)) -> [a] -> ([b],[c])
unzipWith z = foldr f ([],[])
  where
    f x (ys,zs) = (y:ys,z:zs)
      where
        (y,z) = z x

Deriving a Level-Order Breadth-First Search

levels t = unfoldr alg [t]
  where
  alg []  = Nothing
  alg ts  = Just (x, concat xs)
    where
      (x,xs) = foldr f ([],[]) ts

  f (x :& xs) (l, ls) = (x:l, xs:ls)

. . .

Step 8: Inline unfoldr

Deriving a Level-Order Breadth-First Search

levels t = go [t]
  where
  go []  = []
  go ts  = x : go (concat xs)
    where
      (x,xs) = foldr f ([],[]) ts

  f (x :& xs) (l, ls) = (x:l, xs:ls)

. . .

Step 9: Split up go

Deriving a Level-Order Breadth-First Search

levels t = go [t]
  where
    go [] = []
    go ts = b (foldr f ([],[]) ts)

    b (x,xs) = x : go (concat xs)

    f (x :& xs) (l, ls) = (x:l, xs:ls)

. . .

Step 10: Remove go

Deriving a Level-Order Breadth-First Search

levels t = b (f t ([],[]))
  where
    b ([], _) = []
    b (x ,xs) = x : b (foldr f ([],[]) (concat xs))

    f (x :& xs) (l, ls) = (x:l, xs:ls)

. . .

Step 11: Fusion to remove the concat

Deriving a Level-Order Breadth-First Search

levels t = b (f t ([],[]))
  where
    b ([], _) = []
    b (x ,xs) = x : b (foldr (flip (foldr f)) ([],[]) xs)

    f (x :& xs) (l, ls) = (x:l, xs:ls)
--

. . .

Step 12: Fuse away... the pair?

Deriving a Level-Order Breadth-First Search

levels t = b (f t ([],[]))
  where
    b ([], _) = []
    b (x ,xs) = x : b (foldr (flip (foldr f)) ([],[]) xs)
--                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    f (x :& xs) (l, ls) = (x:l, xs:ls)
--                              ^^^^^

Step 12: Fuse away... the pair?

Deriving a Level-Order Breadth-First Search

levels t = b (f t ([],[]))
  where
    b ([], _) = []
    b (x ,xs) = x : b xs
--                    ^^
    f (x :& xs) (l, ls) = (x:l, foldr f ls xs)
--                              ^^^^^^^^^^^^^

Step 12: Fuse away... the pair?

Deriving a Level-Order Breadth-First Search

levels t = b (f t ([],[]))
  where
    b ([], _) = []
    b (x ,xs) = x : b xs
--                    ^^
    f (x :& xs) (l, ls) = (x:l, foldr f ls xs)
--                              ^^^^^^^^^^^^^

. . .

Occurs check: cannot construct the infinite type: b ~ ([a], b)

Deriving a Level-Order Breadth-First Search

Occurs check: cannot construct the infinite type: b ~ ([a], b)

. . .

data Stream a = a :< Stream a

Deriving a Level-Order Breadth-First Search

levels t = b (f t ([],[]))
  where
    b ([], _) = []
    b (x ,xs) = x : b xs

    f (x :& xs) (l, ls) = (x:l, foldr f ls xs)

Deriving a Level-Order Breadth-First Search

levels t = b (f t e)
  where
    b ([] :< _ ) = []
    b (x  :< xs) = x : b xs

    f (x :& xs) (l :< ls) = (x:l) :< foldr f ls xs

    e = [] :< e

. . .

It's possible to write this with lists and library functions

Deriving a Level-Order Breadth-First Search

levels t = takeWhile (not . null) (f t (repeat []))
  where
    f (x :& xs) (l : ls) = (x:l) : foldr f ls xs

. . .

And it's possible to write it entirely inductively (i.e. structurally recursive, Agda won't complain)

Deriving a Level-Order Breadth-First Search

levels t = f t []
  where
    f (x :& xs) (l : ls) = (x:l) : foldr f ls xs
    f (x :& xs) []       = [x]   : foldr f [] xs

. . .

Although getting this version to have the right laziness properties is a bit of a pain:

Deriving a Level-Order Breadth-First Search

levels t = f t []
  where
    f (x :& xs) (l :~ ls) = (x:l) : foldr f ls xs 

. . .

uncons []     = ([], [])
uncons (x:xs) = (x , xs)

pattern (:~) x xs <- (uncons -> ~(x, xs))

Deriving a Level-Order Breadth-First Search

. . .

The stream here is representing the same thing as the hyperfunction.

. . .

In fact streams are a "model" for hyperfunctions.

Polynomials

. . .

$x³ + 2x + 3$

[3,2,0,1]

. . .

[]      + ys      = ys
xs      + []      = xs
(x:xs)  + (y:ys)  = (x + y) : (xs + ys)

[]      * ys  = []
(x:xs)  * ys  = map (x *) ys + (0 : (xs * ys))

. . .

xs * ys = foldr f [] xs where
  f x zs = foldr (g x) id ys ([] : zs)
  g y k (z : zs) = (x * y + z) : k zs

Levels

newtype Levels a = Levels [⟅a⟆]

. . .

instance Applicative Levels where
  pure x = Levels [⟅x⟆]
  Levels xs <*> Levels ys = Levels (foldr f [] xs) where
      f x zs = foldr (g x) id ys (⟅⟆ : zs)
      g x y k (z:zs) = (x <*> y <|> z) : k zs
      g x y k []     = (x <*> y)       : k []

. . .

instance Alternative Levels where
  empty = Levels []
  Levels xs <|> Levels ys = Levels (zipL xs ys) where
      zipL [] ys = ys
      zipL xs [] = xs
      zipL (x:xs) (y:ys) = (x <|> y) : zipL xs ys

. . .

instance Monad Levels where
  Levels xs >>= k = foldr f empty xs where
      f x (Levels ys) = foldr ((<|>) . k) (Levels (⟅⟆ : ys)) x

Levels

pyth = do
  let nats = Levels [ ⟅n⟆ | n <- [1..] ]
  x <- nats
  y <- nats
  z <- nats
  guard (x*x + y*y == z*z)
  pure (x,y,z)

Levels

pyth = do                                     -- >>> mapM_ print pyth
  let nats = Levels [ ⟅n⟆ | n <- [1..] ]      -- (3,4,5)
  x <- nats                                   -- (4,3,5)
  y <- nats                                   -- (6,8,10)
  z <- nats                                   -- (8,6,10)
  guard (x*x + y*y == z*z)                    -- (5,12,13)
  pure (x,y,z)                                -- ...

LogicT

• The transformer version of the Levels type actually implements LogicT, from

  Kiselyov, Oleg, Chung-chieh Shan, Daniel P. Friedman, and Amr Sabry. ‘Backtracking, Interleaving, and Terminating Monad Transformers: (Functional Pearl)’. ICFP ’05. 2005. https://doi.org/10.1145/1086365.1086390.

• Although the implementation of >>= is fairer and lazier.

• And we can use the HypM type to implement a church-encoded version.

Search

The Free Semimodule

• A semimodule is a commutative monoid that can be "conditioned" by a semiring.

  _∪_ : 𝑀 → 𝑀 → 𝑀
  ε   : 𝑀
  _+_ : 𝑅 → 𝑅 → 𝑅
  _∗_ : 𝑅 → 𝑅 → 𝑅
  1 0 : 𝑅
  _⋊_ : 𝑅 → 𝑀 → 𝑀

• We can implement this type in Cubical Agda, using quotients.

  data W (A : Type) : Type where
    []    : W A
    _&_∷_ : (p : 𝑅) → (x : A) → W A → W A
    dup : ∀ p q x xs → p & x ∷ q & x ∷ xs ≡ p + q & x ∷ xs
    com : ∀ p x q y xs → p & x ∷ q & y ∷ xs ≡ q & y ∷ p & x ∷ xs
    del : ∀ x xs → 0# & x ∷ xs ≡ xs
    trunc : isSet (W A)

The Free Semimodule

• The type can represent the probability monad for discrete, finite distributions.

• Or, alternatively it can be used to represent search.

• 1 = empty path; 0 = infinite path; + = min; * = concat.

The Free Semimodule

class Semiring s where
  one, zer :: s
  (<+>), (<.>) :: s -> s -> s

newtype W w a  = W { runW :: [(a, w)] }

cond :: Semiring w => w -> W w a -> W w a
cond w xs = W [ (x, w <.> wx) | (x, wx) <- runW xs ]

instance Semiring w => Monad (W w) where
  return x = W [(x, one)]
  xs >>= k = foldMap (\(x,wx) -> cond wx (k x)) (runW xs)
  
compress :: (Semiring w, Ord a) => W w a -> W w a
compress = W . Map.toList . Map.fromListWith (<+>) . runW

The Heap Monad

data Root a b = a :< Heap a b

type Node a b = Either b (Root a b)

newtype Heap a b = Heap { runHeap :: [Node a b] }

. . .

• We can derive this monad as the free monad plus transformer with the writer monad as the functor.

  data FreeF f a = Pure a | Free (f (FreeT f a))
  
  newtype FreeT f a = { runFreeT :: [FreeF f a] }

• Alternatively, we can derive it as an instance of the "smart datatype" optimisation, where we optimise away the expensive conditioning operator.

  Jaskelioff, Mauro, and Exequiel Rivas. ‘Functional Pearl: A Smart View on Datatypes’. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 355–61. ICFP 2015. New York, NY, USA: ACM, 2015. https://doi.org/10.1145/2784731.2784743.

The Heap Monad

data Root a b = a :< Heap a b

type Node a b = Either b (Root a b)

newtype Heap a b = Heap { runHeap :: [Node a b] }

. . .

• The Node type coincides with the type of pairing heaps.

  Fredman, Michael L., Robert Sedgewick, Daniel D. Sleator, and Robert E. Tarjan. ‘The Pairing Heap: A New Form of Self-Adjusting Heap’. Algorithmica 1, no. 1–4 (January 1986): 111–29. https://doi.org/10.1007/BF01840439.

• This means we can efficiently implement heap operations on the monad.

Monus

class (Ord a, Monoid a) => Monus a where
  (|-|) :: a -> a -> a

. . .

x <= x <> y
x <= y ==> x <> (x |-| y) = y

. . .

instance Monus Natural where
  x |-| y
    | y <= x    = x - y
    | otherwise = y - x

Monus

newtype Prob = Prob { runProb :: Rational }

instance Ord Prob where
  Prob x <= Prob y = y <= x
  
instance Monoid Prob where
  mempty = 1
  (<>) = (*)

instance Monus Prob where
  Prob x |-| Prob y
    | x >= y    = Prob (y / x)
    | otherwise = Prob (x / y)

Heap

popMin :: Monus w => Heap w a -> ([a], Maybe (Root w a))
popMin = second sift . partitionEithers . runHeap

sift :: Monus w => [Root w a] -> Maybe (Root w a)
sift [] = Nothing
sift (x : xs) = Just (sift1 x xs)
  where
    sift1 x  []         = x
    sift1 x1 [x2]       = x1 <> x2
    sift1 x1 (x2:x3:xs) = (x1 <> x2) <> sift1 x3 xs

instance Monus w => Semigroup (Root w a) where
  (xw :< Heap xs) <> (yw :< Heap ys)
    | xw <= yw  = xw :< Heap (Right (xw |-| yw :< Heap ys) : xs)
    | otherwise = yw :< Heap (Right (xw |-| yw :< Heap xs) : ys)

Sampling

choose :: [a] -> IO a

sample :: Heap Prob a -> IO a
sample xs = case popMin xs of
  (y,Nothing) -> choose y
  (y,Just (n % d, ys)) -> do
    s <- randomRIO (1, d)
    if s > n
      then choose y
      else sample ys

Dijkstra

newtype HeapT w m a 
  = HeapT { runHeapT :: ListT m (Either a (w, HeapT w m a)) }

unique :: (MonadState (Set a) m, Alternative m, Ord a) => a -> m ()
unique x = do seen <- get
              guard (Set.notMember x seen)
              put (Set.insert x seen)

dijkstra :: Ord a => Graph a -> Graph a
dijkstra g s = evalState (searchT (explore s)) Set.empty
  where
    explore s = do unique s
                   star (asum . map node . g) s

    node (w, x) = do tell w
                     unique x
                     pure x

star :: MonadPlus m => (a -> m a) -> a -> m a
star f x = pure x <|> (f x >>= star f)

type Graph a = a -> [(Natural, a)]