[Haskell-cafe] Chuch encoding of data structures in Haskell

[Dan Doel]

On Thursday 27 May 2010 7:15:15 pm Brandon S. Allbery KF8NH wrote:
> On May 27, 2010, at 19:07 , Brandon S. Allbery KF8NH wrote:
> > reordered_cons  :: (t -> (t1 -> t2)) -> t -> (t1 -> t2)
> > churchedNumeral :: (t -> t         ) -> t -> t
> > 
> > t unifies with (t1 -> t2), giving us a Church numeral made up of
> > (t1,t2).  (I think.)
> 
> Which also explains why that record representation isn't used:  it's
> as inefficient as Peano numbers are.

Church encoding has additional efficiency problems, too. If we look at Peano 
numerals for instance, the Church encoding is:

  forall r. r -> (r -> r) -> r

This means that our only method of computation with them is the structurally 
recursive fold. So, suppose we want to implement a predecessor operation. With 
Haskell-like data, we do:

  pred :: Nat -> Nat
  pred Zero    = Zero
  pred (Suc n) = n

This operation is expected to be O(1). What if we want to write this using 
only fold? Well, we have to do tricks (this same trick works to define tail 
with foldr):

  pred n = snd $ fold (Zero, Zero) (\ ~(m, _) -> (Suc m, m))

So, we've done it, but if you look closely, you'll see that we've actually 
rebuilt the entire 'tail' of the number. So this definition is O(n) (at least, 
if it all gets evaluated). So, Church encodings are less efficient than a 
direct implementation is capable of being.

There is a dual problem with codata. You can encode the extended natural 
numbers as:

  exists s. (s, s -> Either () s)

but this only gives you the anamorphism. So, if you want to write the 
successor operation, it's:

  succ n = (Nothing, step)
   where
   step Nothing  = Right (Just n)
   step (Just m) = case observe m of
     Left ()  -> Left ()
     Right m' -> Right (Just m')

so we end up re-unfolding the entire number.

Taking the paramorphism/apomorphism as a primitive operation fixes this, I 
believe, but you cannot, to my knowledge, encode types that way in, say, 
System F, because it would involve:

  Nat = forall r. r -> (Nat -> r -> r) -> r

which is still a recursive equation.

-- Dan