[Haskell-cafe] Re: Lists vs. Monads

[oleg at pobox.com]

Jonathan Cast wrote:
] > You can't  define most  initial models  without  recursive (or
] > inductive) data types in general, because initial models are defined
] > inductively.
] > You can't define head, tail,  or foldr using the MonadPlus
] > signature
] OK.  Right.  I forgot about the Church encoding.

I'm afraid just using Church encoding in the typed setting without any
recursive datatypes whatsoever may be problematic.

Indeed, let us consider the standard Church encoding of pairs

> {-# OPTIONS -fglasgow-exts #-}
> module Foo where
>
> cons x y p = p x y
> car p = p true
> cdr p = p false
>
> true x y = x
> false x y = y

from which we can build the encoding of lists. For simplicity, we
assume in this example lists of non-negative numbers, so that we can
encode nil simply as

> nil = cons 0 0
> isnil l = car l == 0

We can build a simple list

> l1 = cons 1 (cons 2 (cons 3 nil))

we can find the second element of the list

> cadr = car . cdr
> t11 = cadr l1

but we can't write any generic function on lists, e.g., finding out
the n-th element of a list, let alone fold over the list:

> nth 0 l = car l
> -- nth n l = nth (n-1) (cdr l)

-- fldr f z l = if (isnil l) then z else f (car l) (fldr f z (cdr l))

If we uncomment either line, we get an error

    Occurs check: cannot construct the infinite type: t = (t1 -> t1 -> t1) -> t
      Expected type: (t1 -> t1 -> t1) -> (t1 -> t1 -> t1) -> t
      Inferred type: (t1 -> t1 -> t1) -> t
    In the first argument of `cdr', namely `l'
    In the second argument of `nth', namely `(cdr l)'


indeed, the type of cdr is
	cdr :: ((t1 -> t2 -> t2) -> t) -> t
If we wish to say that (cdr l) has the same type as l (and so the same
operations apply to (cdr l) as those that apply to l), we need to
unify ((t1 -> t2 -> t2) -> t) and t -- which is impossible without
recursive types.

The same problem exists for a different variation of the Church
encoding: representing [1,2,3] as (1,(2,(3,()))). Again, we can find
the first or the second element of the latter list -- but we can't
express finding the n-th element without recursive types.

Because in these encodings the type of the list reflects the structure
of the list, and in the absence of the type-level recursion types are
well-founded, these encodings cannot represent infinite lists.

One may say that we don't have to require that (cdr lst) have the same
type as lst itself -- so long as the same operations apply to (cdr
lst) as those that apply to lst. The operations in questions are `car',
`cdr', and `null' -- which can be represented by only one operation,
`dons', the deconstructor. So, we define

> class L l where
>     cdons :: l a -> (forall l'. L l' => a -> l' a -> w) -> w -> w
>
> data Nil a = Nil
> data Cons t a = Cons a (t a)
>
> instance L Nil where
>     cdons _ oncons onnil = onnil
>
> instance L b => L (Cons b) where
>     cdons (Cons h t) oncons onnil = oncons h t


We could have quantified over 't' in `Cons a (t a)' to make a
homogeneous list:

> class TL l where
>     tdons :: l a -> (forall l'. TL l' => a -> l' a -> w) -> w -> w
>
> data DL a = TNil | forall l. TL l => TCons a (l a)
>
> instance TL DL where
>     tdons TNil oncons onnil = onnil
>     tdons (TCons h t) oncons onnil = oncons h t

we can write

> l2 = Cons 1 (Cons 2 (Cons 3 Nil))

> cnth :: L l => Int -> l a -> a
> cnth 0 l = cdons l (\h t -> h) undefined
> cnth n l = cdons l (\h t -> (cnth (n-1) t)) undefined
>
> t21 = cnth 2 l2 
>
> cfoldr :: L l => (a->b->b) -> b -> l a -> b
> cfoldr f z l = cdons l (\h t -> f h (cfoldr f z t)) z
>
> t22 = cfoldr (+) 0 l2

Or, in the homogeneous case,

> l3 = TCons 1 (TCons 2 (TCons 3 TNil))
>
> tnth :: TL l => Int -> l a -> a
> tnth 0 l = tdons l (\h t -> h) undefined
> tnth n l = tdons l (\h t -> (tnth (n-1) t)) undefined
>
> t51 = tnth 2 l3

The latter encoding supports infinite lists:

> l3i = TCons 1 (TCons 2 (TCons 3 l3i))
> t52 = tnth 42 l3i

Neither Cons nor DL are recursive types. Problems solved? Well, the
type class is a sugared dictionary passing. Let us remove the sweetener.

Instances `L Nil' and `L b => L (Cons b)' translate to dictionary
declarations (ref Hall et al.)

> dict'nil = ((), \Nil oncons onnil -> onnil)
> dict'cons = \dict -> ((), \ (Cons h t) oncons onnil -> oncons dict h t)

We use the structure for dictionaries as described in Hall et al. We
define a class method projection function

> dons'm (_,x) = x

The dictionary for the list l2 has the form

> l2'd = dict'cons $ dict'cons $ dict'cons $ dict'nil

We can define

> cadr'd dict l = dons'm dict l (\dict h t -> 
> 	            dons'm dict t (\_ h _ -> h) undefined) undefined
> t31 = cadr'd l2'd l2

We can attempt to define

> cnth'd dict 0 l = dons'm dict l (\dict h t -> h) undefined
> -- cnth'd dict n l = dons'm dict l (\dict h t -> (cnth'd dict (n-1) t)) 
> --			undefined

If we uncomment the latter lines, we get the dreaded

    Occurs check: cannot construct the infinite type:
      t = (a, t3 -> (t -> t1 -> t2 -> t1) -> a1 -> t1)
      Expected type: (a, t3 -> (t -> t1 -> t2 -> t1) -> a1 -> t1)
      Inferred type: t
    In the first argument of `cnth'd', namely `dict'
    In a lambda abstraction: \ dict h t -> (cnth'd dict (n - 1) t)

error. Indeed, the dictionary that is passed along to the recursive
invocation of cnth'd must have the same `structure' as the dictionary
cnth'd received. There is no way to express that fact without
recursion. BTW, the class L is not actually allowed in Hall et
al. system, because their target language had no recursive types. If
we have iso-recursive types, we can realize the dictionaries as

> newtype LDict l a = LDict (forall w. l a -> 
> 			(forall l'. LDict l' a -> a -> l' a -> w) -> w -> w)
>
>
> ldict'nil = LDict (\Nil oncons onnil -> onnil)
> ldict'cons = \dict -> LDict (\ (Cons h t) oncons onnil -> oncons dict h t)
>
> ldons'm :: LDict l a -> 
> 	   l a -> (forall l'. LDict l' a -> a -> l' a -> w) -> w -> w
> ldons'm (LDict x)  = x
>
> cnth'ld :: LDict l a -> Int -> l a -> a
> cnth'ld dict 0 l = ldons'm dict l (\dict h t -> h) undefined
> cnth'ld dict n l = ldons'm dict l (\dict h t -> (cnth'ld dict (n-1) t)) 
> 			undefined
>
> l2'ld = ldict'cons $ ldict'cons $ ldict'cons $ ldict'nil
> t42 = cnth'ld l2'ld 2 l2


but if we had recursive types, we wouldn't have gone into trouble to
implement the list in this way...


There is the third way: represent a list as a fold:

> type ListAsFoldR a = forall b. (a -> b -> b) -> b -> b
>
> lfnil f z = z
> lfcons a l = \f z -> f a (l f z)
>
> l4 = lfcons 1 $ lfcons 2 $ lfcons 3 $ lfnil
> l4i = lfcons 1 $ lfcons 2 $ lfcons 3 $ l4i

The type ListAsFoldR is obviously not recursive. We can similarly
define ListAsFoldL. The stream data type

> newtype FStream a = SFK (forall ans. SK a ans -> FK ans -> ans)
> type FK ans = () -> ans            -- failure continuation
> type SK a ans = a -> FK ans -> ans -- success continuation
> unSFK (SFK a) = a

is of similar nature. The three latter encodings support infinite
lists.

If we try to define nth, we see a problem:

> lflength :: ListAsFoldR a  -> Int
> lflength l = l (const (+ 1)) 0
>
> lfnth :: Int -> ListAsFoldR a -> a
> lfnth n l = snd $ lfnth' ((lflength l) - n - 1) l 
>     where
>     lfnth' n l = l (\a (c,e) -> if c == n then (c+1,a) else (c+1,e)) 
> 		   (0,undefined)
>
> t61 = lfnth 2 l4


This works -- but only for finite lists. Obviously, computing the
length of an infinite list will take time. To select the n-th element
of a list, we need to propagate the counter as part of the state
threaded through the fold. Alas, the threading starts from the right
end -- which does not exist in an infinite list. The representation
ListAsFoldL has the same problem: the left fold gives the answer only
when it finished scanning the whole list, so we can apply it to finite
lists only.

But ListAsFoldR and FStream have a bigger problem: how to take the
tail? The reason these types are not recursive is because the success
continuation (aka the fold function) receives as its second argument
something of the type `b' rather than of the type of the list. So, how
to find the tail of FStream, which is itself of the type FStream,
without resorting to recursive types? We thus get to the problem that
was answered in car-fstream.lhs. As we see, the problem is not so
trivial.