[Haskell-cafe] Re: deconstruction of the list/backtracking applicative functor?

[apfelmus]

Conal Elliott wrote:
> Thanks for the reply.  Here's the decomposition I had in mind.  Start with
> 
>     type List a = Maybe (a, List a)
> 
> Rewrite a bit
> 
>     type List a = Maybe (Id a, List a)
> 
> Then make the type *constructor* pairing explicit
> 
>     type List a = Maybe ((Id :*: List) a)
> 
> where
> 
>     newtype (f :*: g) a = Prod { unProd :: (f a, g a) }
> 
> Then make the type-constructor composition explicit
> 
>     type List = Maybe :. (Id :*: List)
> 
> (which isn't legal Haskell, due to the type synonym cycle).  From there use
> the Functor and Applicative instances for composition and pairing of type
> constructors and for Id.  I think the result is equivalent to ZipList.

Ah, I didn't think of feeding  a  to both  f  and  g  in the product  f 
:* g  . Your argument cheats a bit because of its circularity: assuming 
  List  is an applicative functor, you deduce that  List  is an 
applicative functor. But in this case, the recursion is (co-)inductive, 
so things work out. Here's the formalization:

       -- higher-order functors  g :: (* -> *) -> (* -> *)
       -- (not sure how to do these classes directly in Haskell,
       --  but you know what I want to do here)
   class Functor2 g where
       forall f . Functor f => Functor (g f)
   class Applicative2 g where
       forall f . Applicative f => Applicative (g f)

       -- higher-order composition
   type (f :.. g) h = f :. (g :. h)

       -- fixed points for higher-order functors
   newtype Mu g a = In { out :: g (Mu g) a }

   type List a = Mu ((Maybe :.) :.. (Id :*)) a


   instance Applicative2 g => Applicative (Mu g) where
      pure x = In (pure x)
      (In f) <*> (In x) = In (f <*> g)

This last class instance looks ridiculous of course, but does nothing 
more than use the assertion  Applicative (Mu g)  in its own definition. 
But fortunately, this definition terminates.

>>> Is there some construction simpler than lists
>>> (non-recursive) that introduces cross products?
>
> To clarify my "cross products" question, I mean fs <*> xs = [f x | f <- fs,
> x <- xs], as with lists.

I'm not sure how to decouple the notion of cross products from lists. 
Maybe the other characterization of applicative functors sheds some 
light on it: applicative functors  f  can also be defined with the 
following two primitive operations

   pure  :: a -> f a
   cross :: (f a, f b) -> f (a,b)

   f <*> x = fmap eval (cross (f,x))
       where eval (f,x) = f x

Then, the choice

   pure x = repeat x
   [1,2] `cross` [3,4] = [(1,3), (2,4)]

yields zip lists whereas the choice

   pure x = [x]
   [1,2] `cross` [3,4] = [(1,3), (1,4), (2,3), (2,4)]

yields backtracking lists. I'm not sure whether other choices are 
possible too, they probably violate the laws mentioned in chapter 7 of 
the applicative functor paper.


Regards,
apfelmus