Jonathan Cast wrote:

...

If you had a version of Haskell without recursive data types you wouldn't be at a loss, because you could always use monads to recreate lists. Maybe "bind" would replace the job of "cons" and "return" would replace "head" or somesuch.

No. 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 (how would you define them for e.g. a backtracking parser?), which is why you do need recursive types for []

However surprising might it seem, you _can_ define head, tail, and foldr for an implementation of a backtracking transformer that it is not a list and uses no recursive (or inductive) types. In fact, it is possible to define list final algebra (complete with head and tail) in a language without recursive datatypes, only with the higher-rank one. The msplit contraption of the LogicT paper was `null', `head', and `tail' all in one. The paper specifically made a point that msplit can be defined without help from recursive data types. The brief summary of that derivation is a note `How to take a TAIL of a functional stream' http://pobox.com/~oleg/ftp/Computation/Continuations.html#cdr-fstream The higher-rank type is needed only to express the polymorphic answertype.

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.