listhaskellcategory-theory

Relation between `DList` and `[]` with Codensity


I've been experimenting with Codensity lately which is supposed to relate DList with [] among other things. Anyway, I've never found code that states this relation. After some experiments I ended up with this:

{-# LANGUAGE RankNTypes #-}
module Codensity where

newtype Codensity f a = Codensity
  { runCodensity :: forall b. (a -> f b) -> f b }

type DList a = Codensity [] [a]

nil :: DList a
nil = Codensity ($ [])

infixr 5 `cons`
cons :: a -> DList a -> DList a
cons x (Codensity xs) = Codensity ($ (xs (x:)))

append :: DList a -> DList a -> DList a
append (Codensity xs) ys = Codensity ($ (xs (++ toList ys)))

toList :: DList a -> [a]
toList xs = runCodensity xs id

fromList :: [a] -> DList a
fromList xs = Codensity (\k -> k xs)

However, the definition of DList feels a bit icky in my example. Is there a different way to state this relation? Is this even the right way to do this?


Solution

  • One view could be that DList is a way for reordering monoid operations, just as Codensity is a way for reordering monad operations.

    [] is a free monoid on a, so let's represent lists using a free writer monad, that is Free ((,) a):

    module Codensity where
    
    import Control.Monad
    import Control.Monad.Free
    import Control.Monad.Codensity
    import Control.Monad.Trans (lift)
    
    type DList a = Free ((,) a) ()
    

    Now we can define the standard list operations:

    nil :: DList a
    nil = return ()
    
    singleton :: a -> DList a
    singleton x = liftF (x, ())
    
    append :: DList a -> DList a -> DList a
    append = (>>)
    
    infixr 5 `snoc`
    snoc :: DList a -> a -> DList a
    snoc xs x = xs >> singleton x
    
    exec :: Free ((,) a) () -> [a]
    exec (Free (x, xs)) = x : exec xs
    exec (Pure _) = []
    
    fromList :: [a] -> DList a
    fromList = mapM_ singleton
    
    toList :: DList a -> [a]
    toList = exec
    

    This representation has the same drawbacks as list when it comes to snoc. We can verify that

    last . toList . foldl snoc nil $ [1..10000]
    

    takes a significant (quadratic) amount of time. However, just as every free monad, it can be improved using Codensity. We just replace the definition with

    type DList a = Codensity (Free ((,) a)) ()
    

    and toList with

    toList = exec . lowerCodensity
    

    Now the same expression is executed instantly, as Codensity reorders the operations, just like the original difference lists.