Skip to content

Instantly share code, notes, and snippets.

@michaeljklein
Last active November 6, 2017 18:22
Show Gist options
  • Select an option

  • Save michaeljklein/0a502fed28b5f7b57cfdf115b9d24107 to your computer and use it in GitHub Desktop.

Select an option

Save michaeljklein/0a502fed28b5f7b57cfdf115b9d24107 to your computer and use it in GitHub Desktop.

Introduction

We want the following function:

pushThrough :: (Functor f, Functor g) => f (g a) -> f (g (f a))

To ensure that something actually gets pushed through, we require that:

pushThrough = pushOver . partition
partition :: (Functor f, Functor g) => f (g a) -> f (f (g a))
pushOver  :: (Functor f, Functor g) => f (f (g a)) -> f (g (f a))

To ensure that everything that can possibly get pushed through does, we require pushThrough to be "idempotent":

Pointed f
pushThrough . pushThrough = fmap (fmap point) . pushThrough

Common push-throughs

We find that when pushing through Either a b, we get that pushThrough must be of the form:

pushThrough :: f (Either a b) -> Either (CycleCofree f (f a) (f b)) (CycleCofree f (f b) (f a))
  where
    newtype CycleCofree f a b = CycleCofree (b, f (CycleCofree f b a))

We find that when pushing through (a, b), we get that pushThrough must be of the form:

pushThrough :: f (a, b) -> Free f (f a, f b)
  where
    newtype Free f a = Either a (f (Free f a))

Pushing through compositions

It appears that either pushing (Functor f, Functor g) => Compose f g through Functor h => h or Functor f => f through (Functor g, Functor h) => Compose g h requires inverted pushing to "clean up the leftovers" To see this, consider pushOver for the second case:

pushOver :: f (f (Compose g h a)) -> f (Compose g h (f a))
-- we unwrap the Compose newtype
pushOver :: f (f (g (h a))) -> f (g (h (f a)))
-- we push f over g
pushOver :: f (g (f (h a))) -> f (g (h (f a)))
-- we partition and push f over h
pushOver :: f (g (f (h (f a)))) -> f (g (h (f a)))

Assuming we've pushed through all of f that we can through Compose g h and it must be of the above form, we have to withdraw the leftovers of the partition back (left):

f (g (f t)) -> f (g t)

This is exactly the form of an inverted pushThrough.

Haskell implementation

Here are example implementations of push, pull-throughs as Haskell type-classes:

class (Functor f, Functor g) => Push f g where
  -- | Partition the `f`
  part :: f (g a) -> f (f (g a))

  -- | Push the inner `f` through the `g`
  pver :: f (f (g a)) -> f (g (f a))

  push :: f (g a) -> f (g (f a))
  push = pver . part

class (Functor f, Functor g) => Qush f g where
  -- | Join the partitioned `f`
  qart :: f (f (g a)) -> f (g a)

  -- | Pull the inner `f` through the `g`
  qver :: f (g (f a)) -> f (f (g a))

  qush :: f (g (f a)) -> f (g a)
  qush = qart . qver

class (Functor f, Functor g) => Pull f g where
  -- | Parition the `g`
  draw :: f (g a) -> f (g (g a))

  -- | Pull the outer `g` through the `f`
  plvr :: f (g (g a)) -> g (f (g a))

  pull :: f (g a) -> g (f (g a))
  pull = plver . draw

class (Functor f, Functor g) => Qull f g where
  -- | Join the partitioned `g`
  braw :: f (g (g a)) -> f (g a)

  -- | Push the outer `g` through the `f`
  qlvr :: g (f (g a)) -> f (g (g a))

  qull :: g (f (g a)) -> f (g a)
  qull = braw . qlvr

Examples

Push the list structure through a Maybe:

instance Push [] Maybe where
  part :: [Maybe a] -> [[Maybe a]]
  part = groupBy ((==) `on` isJust)

  pver :: [[Maybe a]] -> [Maybe [a]]
  pver = fmap $ liftM2 (>>) (join . listToMaybe) (Just . fmap fromJust)

Push the list structure of ListT m through a MaybeT m:

instance Monad m => Push (ListT m) (MaybeT m) where
  part :: ListT m (MaybeT m a) -> ListT m (ListT m (MaybeT m a))
  part = partWrap . part' . partUnwrap
    where
      partWrap :: Functor m => m [m [m (Maybe a)]] -> ListT m (ListT m (MaybeT m a))
      partWrap = fmap (fmap MaybeT) . fmap ListT . ListT

      part' :: Monad m => m [m (Maybe a)] -> m [m [m (Maybe a)]]
      part' = fmap (fmap (return . fmap return)) . (>>= fmap (groupBy ((==) `on` isJust)) . sequence)

      partUnwrap :: Functor m => ListT m (MaybeT m a) -> m [m (Maybe a)]
      partUnwrap = runListT . fmap runMaybeT

  pver :: ListT m (ListT m (MaybeT m a)) -> ListT m (MaybeT m (ListT m a))
  pver = pverWrap . fmap (fmap pver') . pverUnwrap
    where
      pverWrap :: Functor m => m [m (Maybe (m [a]))] -> ListT m (MaybeT m (ListT m a))
      pverWrap = fmap (fmap ListT) . fmap MaybeT . ListT

      pver' :: Monad m => m [m (Maybe a)] -> m (Maybe (m [a]))
      pver' xs = do
        xs' <- fmap (fmap fromJust) <$> xs
        if null xs'
           then return Nothing
           else return (Just (sequence xs'))

      pverUnwrap :: Functor m => ListT m (ListT m (MaybeT m a)) -> m [m [m (Maybe a)]]
      pverUnwrap = runListT . fmap runListT . fmap (fmap runMaybeT)

Abstract applications:

Dependent information flow

Push-throughs can be used to model the flow of information through dependent contexts.

  • We encode contexts using functors
  • We encode context dependency using: "context f depends on context g" -> g . f
  • We encode the transfer of information from a context to a dependent context as a push-through
  • We encode the transfer of information from a context to a depended context as a pull-through

Information bottlenecks

This model can easily express the "information bottleneck" model of neural networks, found in this preprint.

We encode the neural network as:

outer_context . neural_network

We encode the training of the neural network as a push-through from the outer context to the context of the neural network:

push :: outer_context (neural_network a) -> outer_context (neural_network (outer_context a))

We model utilizing the resulting predictions of the neural network as a pull through from the context of the neural network to the outer context (i.e. updating the information we have about the outer context based on the information contained within neural network's context):

pull :: outer_context (neural_network (outer_context a)) -> outer_context (neural_network a)

Since the neural network context is finite, only a finite amount of the outer context can be pushed through.

This is the "information bottleneck" described in the paper.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment