Wed 29 Apr 2015

## Domains, Sets, Traversals and Applicatives

Posted by Dan Doel under Category Theory , Comonads , Data Structures , Haskell , Mathematics , Monads[70] Comments

Last time I looked at free monoids, and noticed that in Haskell lists don't really cut it. This is a consequence of laziness and general recursion. To model a language with those properties, one needs to use domains and monotone, continuous maps, rather than sets and total functions (a call-by-value language with general recursion would use domains and strict maps instead).

This time I'd like to talk about some other examples of this, and point out how doing so can (perhaps) resolve some disagreements that people have about the specific cases.

The first example is not one that I came up with: induction. It's sometimes said that Haskell does not have inductive types at all, or that we cannot reason about functions on its data types by induction. However, I think this is (techincally) inaccurate. What's true is that we cannot simply pretend that that our types are sets and use the induction principles for sets to reason about Haskell programs. Instead, one has to figure out what inductive domains would be, and what their proof principles are.

Fortunately, there are some papers about doing this. The most recent (that I'm aware of) is Generic Fibrational Induction. I won't get too into the details, but it shows how one can talk about induction in a general setting, where one has a category that roughly corresponds to the type theory/programming language, and a second category of proofs that is 'indexed' by the first category's objects. Importantly, it is not required that the second category is somehow 'part of' the type theory being reasoned about, as is often the case with dependent types, although that is also a special case of their construction.

One of the results of the paper is that this framework can be used to talk about induction principles for types that don't make sense as sets. Specifically:

newtype Hyp = Hyp ((Hyp -> Int) -> Int)

the type of "hyperfunctions". Instead of interpreting this type as a set, where it would effectively require a set that is isomorphic to the power set of its power set, they interpret it in the category of domains and strict functions mentioned earlier. They then construct the proof category in a similar way as one would for sets, except instead of talking about predicates as sub*sets*, we talk about sub-*domains* instead. Once this is done, their framework gives a notion of induction for this type.

This example is suitable for ML (and suchlike), due to the strict functions, and sort of breaks the idea that we can really get away with only thinking about sets, even there. Sets are good enough for some simple examples (like flat domains where we don't care about ⊥), but in general we have to generalize induction itself to apply to all types in the 'good' language.

While I haven't worked out how the generic induction would work out for Haskell, I have little doubt that it would, because ML actually contains all of Haskell's data types (and vice versa). So the fact that the framework gives meaning to induction for ML implies that it does so for Haskell. If one wants to know what induction for Haskell's 'lazy naturals' looks like, they can study the ML analogue of:

data LNat = Zero | Succ (() -> LNat)

because function spaces lift their codomain, and make things 'lazy'.

----

The other example I'd like to talk about hearkens back to the previous article. I explained how `foldMap`

is the proper fundamental method of the `Foldable`

class, because it can be massaged to look like:

foldMap :: Foldable f => f a -> FreeMonoid a

and lists are not the free monoid, because they do not work properly for various infinite cases.

I also mentioned that `foldMap`

looks a lot like `traverse`

:

foldMap :: (Foldable t , Monoid m) => (a -> m) -> t a -> m traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)

And of course, we have `Monoid m => Applicative (Const m)`

, and the functions are expected to agree in this way when applicable.

Now, people like to get in arguments about whether traversals are allowed to be infinite. I know Ed Kmett likes to argue that they can be, because he has lots of examples. But, not everyone agrees, and especially people who have papers proving things about traversals tend to side with the finite-only side. I've heard this includes one of the inventors of `Traversable`

, Conor McBride.

In my opinion, the above disagreement is just another example of a situation where we have a generic notion instantiated in two different ways, and intuition about one does not quite transfer to the other. If you are working in a language like Agda or Coq (for proving), you will be thinking about traversals in the context of sets and total functions. And there, traversals are finite. But in Haskell, there are infinitary cases to consider, and they should work out all right when thinking about domains instead of sets. But I should probably put forward some argument for this position (and even if I don't need to, it leads somewhere else interesting).

One example that people like to give about finitary traversals is that they can be done via lists. Given a finite traversal, we can traverse to get the elements (using `Const [a]`

), traverse the list, then put them back where we got them by traversing again (using `State [a]`

). Usually when you see this, though, there's some subtle cheating in relying on the list to be exactly the right length for the second traversal. It will be, because we got it from a traversal of the same structure, but I would expect that proving the function is actually total to be a lot of work. Thus, I'll use this as an excuse to do my own cheating later.

Now, the above uses lists, but why are we using lists when we're in Haskell? We know they're deficient in certain ways. It turns out that we can give a lot of the same relevant structure to the better free monoid type:

newtype FM a = FM (forall m. Monoid m => (a -> m) -> m) deriving (Functor) instance Applicative FM where pure x = FM ($ x) FM ef < *> FM ex = FM $ \k -> ef $ \f -> ex $ \x -> k (f x) instance Monoid (FM a) where mempty = FM $ \_ -> mempty mappend (FM l) (FM r) = FM $ \k -> l k <> r k instance Foldable FM where foldMap f (FM e) = e f newtype Ap f b = Ap { unAp :: f b } instance (Applicative f, Monoid b) => Monoid (Ap f b) where mempty = Ap $ pure mempty mappend (Ap l) (Ap r) = Ap $ (<>) < $> l < *> r instance Traversable FM where traverse f (FM e) = unAp . e $ Ap . fmap pure . f

So, free monoids are `Monoids`

(of course), `Foldable`

, and even `Traversable`

. At least, we can define something with the right type that wouldn't bother anyone if it were written in a total language with the right features, but in Haskell it happens to allow various infinite things that people don't like.

Now it's time to cheat. First, let's define a function that can take any `Traversable`

to our free monoid:

toFreeMonoid :: Traversable t => t a -> FM a toFreeMonoid f = FM $ \k -> getConst $ traverse (Const . k) f

Now let's define a `Monoid`

that's not a monoid:

data Cheat a = Empty | Single a | Append (Cheat a) (Cheat a) instance Monoid (Cheat a) where mempty = Empty mappend = Append

You may recognize this as the data version of the free monoid from the previous article, where we get the real free monoid by taking a quotient. using this, we can define an `Applicative`

that's not valid:

newtype Cheating b a = Cheating { prosper :: Cheat b -> a } deriving (Functor) instance Applicative (Cheating b) where pure x = Cheating $ \_ -> x Cheating f < *> Cheating x = Cheating $ \c -> case c of Append l r -> f l (x r)

Given these building blocks, we can define a function to relabel a traversable using a free monoid:

relabel :: Traversable t => t a -> FM b -> t b relabel t (FM m) = propser (traverse (const hope) t) (m Single) where hope = Cheating $ \c -> case c of Single x -> x

And we can implement any traversal by taking a trip through the free monoid:

slowTraverse :: (Applicative f, Traversable t) => (a -> f b) -> t a -> f (t b) slowTraverse f t = fmap (relabel t) . traverse f . toFreeMonoid $ t

And since we got our free monoid via traversing, all the partiality I hid in the above won't blow up in practice, rather like the case with lists and finite traversals.

Arguably, this is worse cheating. It relies on the exact association structure to work out, rather than just number of elements. The reason is that for infinitary cases, you cannot flatten things out, and there's really no way to detect when you have something infinitary. The finitary traversals have the luxury of being able to reassociate everything to a canonical form, while the infinite cases force us to not do any reassociating at all. So this might be somewhat unsatisfying.

But, what if we didn't have to cheat at all? We can get the free monoid by tweaking `foldMap`

, and it looks like `traverse`

, so what happens if we do the same manipulation to the latter?

It turns out that lens has a type for this purpose, a slight specialization of which is:

newtype Bazaar a b t = Bazaar { runBazaar :: forall f. Applicative f => (a -> f b) -> f t }

Using this type, we can reorder `traverse`

to get:

howBizarre :: Traversable t => t a -> Bazaar a b (t b) howBizarre t = Bazaar $ \k -> traverse k t

But now, what do we do with this? And what even is it? [1]

If we continue drawing on intuition from `Foldable`

, we know that `foldMap`

is related to the free monoid. `Traversable`

has more indexing, and instead of `Monoid`

uses `Applicative`

. But the latter are actually related to the former; `Applicative`

s are monoidal (closed) functors. And it turns out, `Bazaar`

has to do with free `Applicative`

s.

If we want to construct free `Applicative`

s, we can use our universal property encoding trick:

newtype Free p f a = Free { gratis :: forall g. p g => (forall x. f x -> g x) -> g a }

This is a higher-order version of the free `p`

, where we parameterize over the constraint we want to use to represent structures. So `Free Applicative f`

is the free `Applicative`

over a type constructor `f`

. I'll leave the instances as an exercise.

Since free monoid is a monad, we'd expect `Free p`

to be a monad, too. In this case, it is a McBride style indexed monad, as seen in The Kleisli Arrows of Outrageous Fortune.

type f ~> g = forall x. f x -> g x embed :: f ~> Free p f embed fx = Free $ \k -> k fx translate :: (f ~> g) -> Free p f ~> Free p g translate tr (Free e) = Free $ \k -> e (k . tr) collapse :: Free p (Free p f) ~> Free p f collapse (Free e) = Free $ \k -> e $ \(Free e') -> e' k

That paper explains how these are related to Atkey style indexed monads:

data At key i j where At :: key -> At key i i type Atkey m i j a = m (At a j) i ireturn :: IMonad m => a -> Atkey m i i a ireturn = ... ibind :: IMonad m => Atkey m i j a -> (a -> Atkey m j k b) -> Atkey m i k b ibind = ...

It turns out, `Bazaar`

is exactly the Atkey indexed monad derived from the `Free Applicative`

indexed monad (with some arguments shuffled) [2]:

hence :: Bazaar a b t -> Atkey (Free Applicative) t b a hence bz = Free $ \tr -> runBazaar bz $ tr . At forth :: Atkey (Free Applicative) t b a -> Bazaar a b t forth fa = Bazaar $ \g -> gratis fa $ \(At a) -> g a imap :: (a -> b) -> Bazaar a i j -> Bazaar b i j imap f (Bazaar e) = Bazaar $ \k -> e (k . f) ipure :: a -> Bazaar a i i ipure x = Bazaar ($ x) (>>>=) :: Bazaar a j i -> (a -> Bazaar b k j) -> Bazaar b k i Bazaar e >>>= f = Bazaar $ \k -> e $ \x -> runBazaar (f x) k (>==>) :: (s -> Bazaar i o t) -> (i -> Bazaar a b o) -> s -> Bazaar a b t (f >==> g) x = f x >>>= g

As an aside, `Bazaar`

is also an (Atkey) indexed comonad, and the one that characterizes traversals, similar to how indexed store characterizes lenses. A `Lens s t a b`

is equivalent to a coalgebra `s -> Store a b t`

. A traversal is a similar `Bazaar`

coalgebra:

s -> Bazaar a b t ~ s -> forall f. Applicative f => (a -> f b) -> f t ~ forall f. Applicative f => (a -> f b) -> s -> f t

It so happens that Kleisli composition of the Atkey indexed monad above `(>==>)`

is traversal composition.

Anyhow, `Bazaar`

also inherits `Applicative`

structure from `Free Applicative`

:

instance Functor (Bazaar a b) where fmap f (Bazaar e) = Bazaar $ \k -> fmap f (e k) instance Applicative (Bazaar a b) where pure x = Bazaar $ \_ -> pure x Bazaar ef < *> Bazaar ex = Bazaar $ \k -> ef k < *> ex k

This is actually analogous to the `Monoid`

instance for the free monoid; we just delegate to the underlying structure.

The more exciting thing is that we can fold and traverse over the first argument of `Bazaar`

, just like we can with the free monoid:

bfoldMap :: Monoid m => (a -> m) -> Bazaar a b t -> m bfoldMap f (Bazaar e) = getConst $ e (Const . f) newtype Comp g f a = Comp { getComp :: g (f a) } deriving (Functor) instance (Applicative f, Applicative g) => Applicative (Comp g f) where pure = Comp . pure . pure Comp f < *> Comp x = Comp $ liftA2 (< *>) f x btraverse :: (Applicative f) => (a -> f a') -> Bazaar a b t -> Bazaar a' b t btraverse f (Bazaar e) = getComp $ e (c . fmap ipure . f)

This is again analogous to the free monoid code. `Comp`

is the analogue of `Ap`

, and we use `ipure`

in `traverse`

. I mentioned that `Bazaar`

is a comonad:

extract :: Bazaar b b t -> t extract (Bazaar e) = runIdentity $ e Identity

And now we are finally prepared to not cheat:

honestTraverse :: (Applicative f, Traversable t) => (a -> f b) -> t a -> f (t b) honestTraverse f = fmap extract . btraverse f . howBizarre

So, we can traverse by first turning out `Traversable`

into some structure that's kind of like the free monoid, except having to do with `Applicative`

, traverse that, and then pull a result back out. `Bazaar`

retains the information that we're eventually building back the same type of structure, so we don't need any cheating.

To pull this back around to domains, there's nothing about this code to object to if done in a total language. But, if we think about our free `Applicative`

-ish structure, in Haskell, it will naturally allow infinitary expressions composed of the `Applicative`

operations, just like the free monoid will allow infinitary monoid expressions. And this is okay, because *some* `Applicative`

s can make sense of those, so throwing them away would make the type not free, in the same way that even finite lists are not the free monoid in Haskell. And this, I think, is compelling enough to say that infinite traversals are right for Haskell, just as they are wrong for Agda.

For those who wish to see executable code for all this, I've put a files here and here. The latter also contains some extra goodies at the end that I may talk about in further installments.

[1] Truth be told, I'm not exactly sure.

[2] It turns out, you can generalize `Bazaar`

to have a correspondence for every choice of `p`

newtype Bizarre p a b t = Bizarre { bizarre :: forall f. p f => (a -> f b) -> f t }

`hence`

and `forth`

above go through with the more general types. This can be seen here.

September 22nd, 2022 at 6:47 am

forex…The Comonad.Reader » Domains, Sets, Traversals and Applicatives…

September 23rd, 2022 at 6:11 am

5 mg viagra coupon printable https://500px.com/p/skulogovid/?view=groups...Really tons of helpful material….

September 23rd, 2022 at 10:09 am

Viagra generika https://500px.com/p/bersavahi/?view=groups...You expressed this fantastically….

September 23rd, 2022 at 10:46 pm

Football Betting…blog topic…

September 24th, 2022 at 3:19 am

Viagra from canada https://reallygoodemails.com/canadianpharmaceuticalsonlineusa...Wow plenty of wonderful knowledge….

September 24th, 2022 at 6:51 am

Viagra kaufen https://www.provenexpert.com/canadian-pharmaceuticals-online-usa/...Whoa a good deal of beneficial tips….

September 24th, 2022 at 11:56 am

Buy generic viagra https://sanangelolive.com/members/pharmaceuticals...Appreciate it! Plenty of write ups!

…

September 24th, 2022 at 10:50 pm

binary options…blog topic…

September 25th, 2022 at 1:48 am

http://www.majorcabritish.Com/groups/sunbet-online-betting-more-get-sa-s-best-bonuses-1141656856...blog topic…

September 26th, 2022 at 1:52 am

paket usaha printing…blog topic…

September 26th, 2022 at 5:42 am

SEO to the Point…blog topic…

September 26th, 2022 at 11:00 am

canadian pharmaceuticals https://melaninterest.com/user/canadian-pharmaceuticals-online/?view=likes...You said it perfectly…..

September 26th, 2022 at 2:59 pm

canadian rx https://haikudeck.com/canadian-pharmaceuticals-online-personal-presentation-827506e003...Reliable postings. Thanks a lot!…

September 26th, 2022 at 6:31 pm

dedicated server for rent…The Comonad.Reader » Domains, Sets, Traversals and Applicatives…

September 26th, 2022 at 7:06 pm

Viagra generique https://buyersguide.americanbar.org/profile/420642/0...Effectively spoken of course! ….

September 27th, 2022 at 2:47 am

Viagra prices https://experiment.com/users/canadianpharmacy...You mentioned it superbly!…

September 27th, 2022 at 8:44 am

drugs for sale https://slides.com/canadianpharmaceuticalsonline...Nicely put, Kudos….

September 27th, 2022 at 12:27 pm

Tadalafil 5mg https://challonge.com/esapenti...Valuable info. Thanks a lot!…

September 27th, 2022 at 4:52 pm

Online viagra https://challonge.com/gotsembpertvil...With thanks! I like this!…

September 27th, 2022 at 8:31 pm

مرجان وظائف دبي…The Comonad.Reader » Domains, Sets, Traversals and Applicatives…

September 28th, 2022 at 6:32 am

Viagra generika https://challonge.com/citlitigolf...Useful posts. Thanks….

September 28th, 2022 at 10:06 am

stromectol treatment scabies https://order-stromectol-over-the-counter.estranky.cz/clanky/order-stromectol-over-the-counter.html...Thanks! I appreciate it….

September 28th, 2022 at 4:32 pm

Viagra levitra https://soncheebarxu.estranky.cz/clanky/stromectol-for-head-lice.html...Thank you. Good information!…

September 29th, 2022 at 1:26 am

Situs Slot Gacor Terpercaya 2022…blog topic…

September 29th, 2022 at 6:03 am

dose for stromectol https://lehyriwor.estranky.sk/clanky/stromectol-cream.html...Wow quite a lot of fantastic information….

September 29th, 2022 at 9:50 am

Viagra purchasing https://dsdgbvda.zombeek.cz/...You definitely made the point….

September 29th, 2022 at 4:20 pm

stromectol buy https://inflavnena.zombeek.cz/...Useful advice. Regards!…

September 30th, 2022 at 4:19 am

wwwi.odnoklassniki-film.ru…wwwi.odnoklassniki-film.ru…

September 30th, 2022 at 6:44 am

site…site…

September 30th, 2022 at 10:32 am

Generic for viagra https://www.myscrsdirectory.com/profile/421708/0...Effectively expressed indeed! ….

September 30th, 2022 at 5:47 pm

Canadian Pharmacies Shipping to USA https://supplier.ihrsa.org/profile/421717/0...Wonderful info. Thanks a lot….

October 1st, 2022 at 12:10 am

daftar ngamenjitu…blog topic…

October 1st, 2022 at 8:06 am

Viagra reviews https://wefbuyersguide.wef.org/profile/421914/0...Amazing lots of fantastic information….

October 1st, 2022 at 12:10 pm

Canadian viagra https://legalmarketplace.alanet.org/profile/421920/0...You actually explained that fantastically….

October 1st, 2022 at 3:30 pm

t.me…The Comonad.Reader » Domains, Sets, Traversals and Applicatives…

October 1st, 2022 at 6:37 pm

Latex fashion…The Comonad.Reader » Domains, Sets, Traversals and Applicatives…

October 2nd, 2022 at 5:45 am

Viagra daily https://moaamein.nacda.com/profile/422018/0...Helpful postings. Appreciate it!…

October 2nd, 2022 at 10:09 am

Viagra from canada https://www.audiologysolutionsnetwork.org/profile/422019/0...You actually said it adequately!…

October 2nd, 2022 at 1:26 pm

Online viagra https://network.myscrs.org/profile/422020/0...Nicely put. Regards….

October 2nd, 2022 at 2:12 pm

The London Info…The Comonad.Reader » Domains, Sets, Traversals and Applicatives…

October 3rd, 2022 at 7:12 am

canadian drugstore https://sanangelolive.com/members/canadianpharmaceuticalsonlineusa...Regards! Plenty of content.

…

October 3rd, 2022 at 10:43 am

stromectol nz https://sanangelolive.com/members/girsagerea...Very good tips. Regards….

October 4th, 2022 at 9:36 am

Cheap viagra https://www.ecosia.org/search?q=“My Canadian Pharmacy – Extensive Assortment of Medications – 2022″…You said that superbly!…

October 4th, 2022 at 1:51 pm

Buy generic viagra https://www.mojomarketplace.com/user/Canadianpharmaceuticalsonline-EkugcJDMYH...Amazing quite a lot of excellent facts….

October 4th, 2022 at 5:43 pm

Viagra lowest price https://seedandspark.com/user/canadian-pharmaceuticals-online...Regards! Loads of facts!

…

October 5th, 2022 at 2:37 am

เว็บบาคาร่า…blog topic…

October 5th, 2022 at 10:47 am

Viagra or viagra https://www.giantbomb.com/profile/canadapharmacy/blog/canadian-pharmaceuticals-online/265652/...This is nicely put! !…

October 5th, 2022 at 2:41 pm

buy viagra now https://feeds.feedburner.com/bing/Canadian-pharmaceuticals-online...You actually stated that terrifically….

October 5th, 2022 at 7:22 pm

Discount viagra https://search.gmx.com/web/result?q=“My Canadian Pharmacy – Extensive Assortment of Medications – 2022″…Effectively spoken of course. ….

October 5th, 2022 at 7:31 pm

rftrip.ru…rftrip.ru…

October 6th, 2022 at 4:27 am

prescriptions from canada without https://search.seznam.cz/?q=“My Canadian Pharmacy – Extensive Assortment of Medications – 2022″…This is nicely said. !…

October 6th, 2022 at 8:12 am

Viagra dosage https://sanangelolive.com/members/unsafiri...Many thanks! I value this!…

October 6th, 2022 at 12:23 pm

viagra canada …You actually mentioned it exceptionally well….

October 7th, 2022 at 5:55 am

canada drug https://www.dogpile.com/serp?q=“My Canadian Pharmacy – Extensive Assortment of Medications – 2022″…You said it adequately.!…

October 7th, 2022 at 1:05 pm

Buy viagra online …Wow a lot of wonderful information!…

October 8th, 2022 at 8:57 am

Buy generic viagra https://search.givewater.com/serp?q=“My Canadian Pharmacy – Extensive Assortment of Medications – 2022″…Thank you, Excellent information….

October 8th, 2022 at 10:05 am

boys fendi hat…blog topic…

October 8th, 2022 at 2:25 pm

canadian online pharmacies https://www.bakespace.com/members/profile/Сanadian pharmaceuticals for usa sales/1541108/…Cheers! I value this….

October 9th, 2022 at 7:34 am

Viagra 5mg …You reported it superbly….

October 9th, 2022 at 12:42 pm

Tadalafil tablets https://results.excite.com/serp?q=“My Canadian Pharmacy – Extensive Assortment of Medications – 2022″…Amazing quite a lot of beneficial knowledge!…

October 9th, 2022 at 5:14 pm

Viagra 20mg https://www.infospace.com/serp?q=“My Canadian Pharmacy – Extensive Assortment of Medications – 2022″…Many thanks. Valuable stuff!…

October 9th, 2022 at 10:15 pm

terbinafine 250 mg buy online…The Comonad.Reader » Domains, Sets, Traversals and Applicatives…

October 10th, 2022 at 12:45 am

dolpsy.ru…dolpsy.ru…

October 10th, 2022 at 9:30 am

Viagra tablets australia https://headwayapp.co/canadianppharmacy-changelog...Thanks. An abundance of content!

…

October 11th, 2022 at 7:32 am

Viagra from canada https://results.excite.com/serp?q=“My Canadian Pharmacy – Extensive Assortment of Medications – 2022″…Superb information. With thanks!…

October 11th, 2022 at 12:56 pm

Viagra uk https://canadianpharmaceuticalsonline.as.me/schedule.php...Many thanks. Quite a lot of postings!

…

October 11th, 2022 at 8:14 pm

slot online jackpot terbesar…blog topic…

October 14th, 2022 at 12:59 am

factoring company austin…blog topic…

October 14th, 2022 at 5:23 am

situs Slot gacor dan terpercaya…blog topic…

October 14th, 2022 at 7:09 am

Viagra alternative https://reallygoodemails.com/orderstromectoloverthecounterusa...Wonderful info, Regards!…