Why do we use folds to encode datatypes as functions?

Question

Or to be specific, why do we use foldr to encode lists and iteration to encode numbers?

Sorry for the longwinded introduction, but I don't really know how to name the things I want to ask about so I'll need to give some exposition first. This draws heavily from this C.A.McCann post that just not quite satisfies my curiosity and I'll also be handwaving the issues with rank-n-types and infinite lazy things.

---

One way to encode datatypes as functions is to create a "pattern matching" function that receives one argument for each case, each argument being a function that receives the values corresponding to that constructor and all arguments returning a same result type.

This all works out as expected for non-recursive types

--encoding data Bool = true | False
type Bool r = r -> r -> r

true :: Bool r
true = \ct cf -> ct

false :: Bool r
false = \ct cf -> cf

--encoding data Either a b = Left a | Right b
type Either a b r = (a -> r) -> (b -> r) -> r

left :: a -> Either a b r
left x = \cl cr -> cl x

right :: b -> Either a b r
right y = \cl cr -> cr y

However, the nice analogy with pattern matching breaks down with recursive types. We might be tempted to do something like

--encoding data Nat = Z | S Nat
type RecNat r = r -> (RecNat -> r) -> r
zero = \cz cs -> cz
succ n = \cz cs -> cs n

-- encoding data List a = Nil | Cons a (List a)
type RecListType a r = r -> (a -> RecListType -> r) -> r
nil = \cnil ccons -> cnil
cons x xs = \cnil ccons -> ccons x xs

but we can't write those recursive type definitions in Haskell! The usual solution is to force the callback of the cons/succ case to be applied to all levels of recursion instead of just the first one (ie, writing a fold/iterator). In this version we use the return type r where the recursive type would be:

--encoding data Nat = Z | S Nat
type Nat r = r -> (r -> r) -> r
zero = \cz cf -> cz
succ n = \cz cf -> cf (n cz cf)

-- encoding data List a = Nil | Cons a (List a)
type recListType a r = r -> (a -> r -> r) -> r
nil = \z f -> z
cons x xs = \z f -> f x (xs z f)

While this version works, it makes defining some functions much harder. For example, writing a "tail" function for lists or a "predecessor" function for numbers is trivial if you can use pattern matching but gets tricky if you need to use the folds instead.

So onto my real questions:

1. How can we be sure that the encoding using folds is as powerful as the hypothetical "pattern matching encoding"? Is there a way to take an arbitrary function definition via pattern matching and mechanically convert it to one using only folds instead? (If so, this would also help make tricky definitions such as tail or foldl in terms of foldr as less magical)

2. Why doesn't the Haskell type system allow for the recursive types needed in the "pattern matching" encoding?. Is there a reason for only allowing recursive types in datatypes defined via data? Is pattern matching the only way to consume recursive algebraic datatypes directly? Does it have to do with the type inferencing algorithm?

Ibanez

I'll just leave this here: haskell.org/pipermail/haskell-cafe/2010-November/085897.html – Tantalize

@melpomene: Hmm, that looks like it asnwers questions #2 - you can do that in Haskel but you need to use newtypes to get access to the recursivity. Now I only need to see if those papers you linked also answer qustion #1 :) (btw, your link was copy pasted weird) – Ibanez

Although predecessor for the Nat is hard, adding is O(1) (I think that's even more efficient than the binary version computers usually use.) – Benzol

Answer 1

The Wikipedia page on Scott encoding has some useful insights. The short version is, what you're referring to is the Church encoding, and your "hypothetical pattern-match encoding" is the Scott encoding. Both are sensible ways of doing things, but the Church encoding requires lighter type machinery to use (in particular, it does not require recursive types).

The proof that the two are equivalent uses the following idea:

churchfold :: (a -> b -> b) -> b -> [a] -> b
churchfold _ z [] = z
churchfold f z (x:xs) = f x (churchfold f z xs)

scottfold :: (a -> [a] -> b) -> b -> [a] -> b
scottfold _ z [] = z
scottfold f _ (x:xs) = f x xs

scottFromChurch :: (a -> [a] -> b) -> b -> [a] -> b
scottFromChurch f z xs = fst (churchfold g (z, []) xs)
 where
  g x ~(_, xs) = (f x xs, x : xs)

The idea is that since churchfold (:) [] is the identity on lists, we can use a Church fold that produces the list argument it is given as well as the result it is supposed to produce. Then in the chain x1 `f` (x2 `f` (... `f` xn) ... ) the outermost f receives a pair (y, x2 : ... : xn : []) (for some y we don't care about), so returns f x1 (x2 : ... : xn : []). Of course, it also has to return x1 : ... : xn : [] so that any more applications of f could also work.

(This is actually a little similar to the proof of the mathematical principle of strong (or complete) induction, from the "weak" or usual principle of induction).

By the way, your Bool r type is a bit too big for real Church booleans – e.g. (+) :: Bool Integer, but (+) isn't really a Church boolean. If you enable RankNTypes then you can use a more precise type: type Bool = forall r. r -> r -> r. Now it is forced to be polymorphic, so genuinely only contains two (ignoring seq and bottom) inhabitants – \t _ -> t and \_ f -> f. Similar ideas apply to your other Church types, too.

Sogdian

Answer 2

Given some inductive data type

data Nat = Succ Nat | Zero

we can consider how we pattern match on this data

case n of
  Succ n' -> f n'
  Zero    -> g

it should be obvious that every function of type Nat -> a can be defined by giving an appropriate f and g and that the only ways to make a Nat (baring bottom) is using one of the two constructors.

---

EDIT: Think about f for a moment. If we are defining a function foo :: Nat -> a by giving the appropriate f and g such that f recursively calls foo than we can redefine f as f' n' (foo n') such that f' is not recursive. If the type a = (a',Nat) than we can instead write f' (foo n). So, without loss of generality

foo n = h $ case n
                 Succ n' -> f (foo n)
                 Zero    -> g

this is the formulation that makes the rest of my post make sense:

---

So, we can thus think about the case statement as applying a "destructor dictionary"

data NatDict a = NatDict {
   onSucc :: a -> a,
   onZero :: a
}

now our case statement from before can become

h $ case n of
      Succ n' -> onSucc (NatDict f g) n'
      Zero    -> onZero (NatDict f g)

given this we can derive

newtype NatBB = NatBB {cataNat :: forall a. NatDict a -> a}

we can then define two functions

fromBB :: NatBB -> Nat
fromBB n = cataNat n (NatDict Succ Zero)

and

toBB :: Nat -> NatBB
toBB Zero = Nat $ \dict -> onZero dict
toBB (Succ n) = Nat $ \dict -> onSucc dict (cataNat (toBB n) dict)

we can prove these two functions are witness to an isomorphism (up to fast and lose reasoning) and thus show that

newtype NatAsFold = NatByFold (forall a. (a -> a) -> a -> a)

(which is just the same as NatBB) is isomorphic to Nat

We can use the same construction with other types, and prove that the resulting function types are what we want just by proving that the underlying types are isomorphic with algebraic reasoning (and induction).

As to your second question, Haskell's type system is based on iso-recursive not equi-recursive types. This is probably becuase the theory and type inference is easier to work out with iso-recursive types, and they have all the power they just impose a little more work on the programmers part. I like to claim that you can get your iso-recursive types without any overhead

newtype RecListType a r = RecListType (r -> (a -> RecListType -> r) -> r)

but apparently GHCs optimizer chokes on those sometimes :(.

Forum

Wait, why is the onSucc case of the NatDict (a -> a)? Wouldn't it have to receive a natdict as the first argument instead of an a for the pattern matching parallel to hold? (The bit I still don t get is why we can be sure that the fold is just as powerful as the pattern matching in this situation) – Ibanez

onSucc is correct, but my later exposition is lacking...give me a moment – Forum