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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
