From oleg-at-okmij.org Thu Jul 21 20:30:38 2005 cc: haskell-cafe@haskell.org In-Reply-To: <200507171849.j6HInPv4004993@localhost.localdomain> Subject: Re: [Haskell-cafe] Re: Lists vs. Monads Message-ID: <20050722023038.4A81DAC5E@Adric.metnet.navy.mil> Date: Thu, 21 Jul 2005 19:30:38 -0700 (PDT) Status: OR 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 [or higher-rank] 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 [but higher-rank!]. 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 discussed in ../Haskell/car-fstream.lhs. As we see, the problem is not so trivial.