Tue 13 May 2008

## Towards Formal Power Series for Functors

Posted by Edward Kmett under Category Theory , Haskell , Mathematics , Type Theory[12] Comments

Tue 13 May 2008

[12] Comments

Wed 7 May 2008

I did some digging and found the universal operations mentioned in the last couple of posts: unzip, unbizip and counzip were referenced as abide, abide and coabide -- actually, I was looking for something else, and this fell into my lap.

They were apparently named for a notion defined by Richard Bird back in:

R.S. Bird. Lecture notes on constructive functional programming. In M. Broy, editor, Constructive Methods in Computing Science. International Summer School directed by F.L. Bauer [et al.], Springer Verlag, 1989. NATO Advanced Science Institute Series (Series F: Computer and System Sciences Vol. 55).

The notion can be summed up by defining that two binary operations and **abide** if for all a, b, c, d:

.

There is a cute pictorial explanation of this idea in Maarten Fokkinga's remarkably readable Ph.D dissertation on p. 20.

The idea appears again on p.88 as part of the famous 'banana split' theorem, and then later on p90 the above names above are given along with the laws:

fmap f &&& fmap g = unfzip . fmap (f &&& g) bimap f g &&& bimap h j = unbizip . bimap (f &&& h) (g &&& j) fmap f ||| fmap g = fmap (f ||| g) . counfzip

That said the cases when the inverse operations exist do not appear to be mentioned in these sources.

Mon 5 May 2008

Twan van Laarhoven pointed out that fzip from the other day is a close cousin of applicative chosen to be an inverse of the universal construction 'unfzip'.

During that post I also put off talking about the dual of zipping, so I figured I'd bring up the notion of choosing a notion of 'cozipping' by defining it as an inverse to a universally definable notion of 'counzipping'.

Sun 4 May 2008

Kefer asked a question in the comments of my post about (co)monadic (co)strength about Uustalu and Vene's ComonadZip class from p157 of The Essence of Dataflow Programming. The class in question is:

class Comonad w => ComonadZip w where czip :: f a -> f b -> f (a, b)

In response I added Control.Functor.Zip [Source] to my nascent rebundled version of category-extras, which was posted up to hackage earlier today.

Wed 30 Apr 2008

[8] Comments

{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-} import Control.Monad import Control.Monad.Identity import Control.Arrow ((&&&), (***),(+++), (|||))

I want to talk about duality briefly. I don't want to go all the way to Filinski-style or Haskell is Not Not ML-style value/continuation duality, but I do want to poke a bit at the variant/record duality explified by the extensible cases used to handle variants in MLPolyR.

The need for extensible cases to handle open variants is part of the expression problem as stated by Wadler:

The goal is to define a data type by cases, where one can add new cases to the data type and new functions over the data type, without recompiling existing code, and while retaining static type safety.

One obvious trick is to use an extensible record of functions as a 'case' statement, with each field corresponding to one of the variants. To index into records you can use an extensible variant of functions to represent a field selection. In a purer form ala the Filinski or the Haskell is Not Not ML approach mentioned above, you can replace the word 'function' with continuation and everything works out.

Sweirstra recently tackled the extensible variant side of the equation with in Data types a la carte using the free monad coproduct to handle the 'variant' side of things, leaving the handling of cases to typeclasses, but we can see if we can go one better and just exploit the variant/record duality directly.

Wed 30 Apr 2008

[9] Comments

No, this isn't some uplifting piece about deriving courage from sloth in the face of adversity.

What I want to talk about is **monadic** strength.

Transcribing the definition from category theory into Haskell we find that a strong monad is a functor such that there exists a morphism:

with a couple of conditions on it that I'll get to later.

Currying that to get something that feels more natural to a Haskell programmer we get:

mstrength :: Monad m => m a -> b -> m (a,b)

Pardo provided us with a nice definition for that in Towards merging recursion and comonads:

Sat 26 Apr 2008

[2] Comments

In case it wasn't obvious, I thought I should mention that Kabanov and Vene's dynamorphisms which optimize histomorphisms for dynamic programming can be expressed readily as chronomorphisms; they just use an anamorphism instead of a futumorphism.

Sat 26 Apr 2008

1 Comment

Back in the days of HYLO, it was common to write hylomorphisms with an additional natural transformation in them. Well, I was still coding in evil imperative languages back then, but I have it on reliable, er.. well supposition, that this is probably the case, or at least that they liked to do it back in the HYLO papers anyways.

Transcoding the category theory mumbo-jumbo into Haskell, so I can have a larger audience, we get the following 'frat combinator' -- you can blame Jules Bean from #haskell for that.

hyloEta :: Functor f => (g b -> b) -> (forall a. f a -> g a) -> (a -> f a) hyloEta phi eta psi = phi . eta . fmap (hyloEta phi eta psi) . psi

We placed eta in the middle of the argument list because it is evocative of the fact that it occurs between phi and psi, and because that seems to be where everyone else puts it.

Now, clearly, we could roll eta into phi and get the more traditional hylo where f = g. Less obviously we could roll it into psi because it is a natural transformation and so the following diagram commutes:

This 'Hylo Shift' property (mentioned in that same paper) allows us to move the 'eta' term into the phi term or into the psi term as we see fit. Since we can move the eta term around and it adds no value to the combinator, it quietly returned to the void from whence it came. hyloEta offers us no more power than hylo, so out it goes.

So, if its dead, why talk about it?

Sat 26 Apr 2008

[3] Comments

First, we can make the generalized hylomorphism from the other day more efficient by noting that once you inline the hylomorphism, you can see that you do 3 fmaps over the same structure, so we can fuse those together yielding:

g_hylo :: (Comonad w, Functor f, Monad m) => (forall a. f (w a) -> w (f a)) -> (forall a. m (f a) -> f (m a)) -> (f (w b) -> b) -> (a -> f (m a)) -> (a -> b) g_hylo w m f g = extract . g_hylo' w m f g . return -- | the kernel of the generalized hylomorphism g_hylo' :: (Comonad w, Functor f, Monad m) => (forall a. f (w a) -> w (f a)) -> (forall a. m (f a) -> f (m a)) -> (f (w b) -> b) -> (a -> f (m a)) -> (m a -> w b) g_hylo' w m f g = liftW f . w . fmap (duplicate . g_hylo' w m f g . join) . m . liftM g

Also, the above made me realize that most of the generalized cata/ana, etc morphisms give you a little more interesting stuff to do if you separate out the recursive part. Then you can pass it a monad built with something other than return to perform substitution on, or inspect the comonadic wrapper on the result.

Oh, and to support my earlier claim that g_hylo generalizes g_cata and g_ana here are derivations of each in terms of g_hylo.

g_cata :: (Functor f, Comonad w) => (forall a. f (w a) -> w (f a)) -> (f (w a) -> a) -> Mu f -> a g_cata k f = g_hylo k (fmap Id . runId) f (fmap Id . outF) g_ana :: (Functor f, Monad m) => (forall a. m (f a) -> f (m a)) -> (a -> f (m a)) -> a -> Nu f g_ana k g = g_hylo (Id . fmap runId) k (InF . fmap runId) g

As an aside, histomorphisms have a dual that seems to be elided from most lists of recursion schemes: Uustalu and Vene call it a futumorphism. It basically lets you return a structure with seeds multiple levels deep rather than have to plumb 'one level at a time' through the anamorphism. While a histomorphism is a generalized catamorphism parameterized by the cofree comonad of your functor, a futumorphism is a generalized anamorphism parameterized by the free monad of your functor.

futu :: Functor f => (a -> f (Free f a)) -> a -> Nu f futu f = ana ((f ||| id) . runFree) . return

Now, g_hylo is painfully general, so lets look at a particularly interesting choice of comonad and monad for a given functor that always have a distributive law: the cofree comonad, and the free monad of that very same functor!

This gives rise to a particular form of morphism that I haven't seem talked about in literature, which after kicking a few names around on the haskell channel we chose to call a **chronomorphism** because it subsumes histo- and futu- morphisms.

chrono :: Functor f => (f (Cofree f b) -> b) -> (a -> f (Free f a)) -> a -> b

Unlike most of the types of these generalized recursion schemes, chrono's type is quite readable!

A chronomorphism's fold operation can 'look back' at the results it has given, and its unfold operation can 'jump forward' by returning seeds nested multiple levels deep. It relies on the fact that you always have a distributive law for the cofree comonad of your functor over the functor itself and also one for the functor over its free monad and so it works for any Functor.

You can generalize it like you generalize histomorphisms and futumorphisms, and derive ana and catamorphisms from it by noting the fact that you can fmap extract or fmap return to deal with the cofree comonad or free monad parts of the term.

Alternately, since the 'identity comonad' can be viewed as the cofree comonad of the Functor that maps everything to , you can also choose to rederive generalized futumorphisms from generalized chronomorphism using the distributive law of the identity comonad.

Below you'll find source code for generalized hylo- cata- ana- histo- futu- chrono- etc... morphisms and their separated kernels.

As an aside, Dan Doel (dolio) has started packaging these up for addition to category-extras in Hackage.

Thu 24 Apr 2008

1 Comment

I haven't seen written up anywhere the following operator (g_hylo), defined in the spirit of generalized catamorphisms and generalized anamorphisms, which seems to follow rather naturally from the definition of both -- I'm using liftW & liftM rather than fmap to make it clear what is being lifted over what.

class Functor w => Comonad w where -- minimal definition: extend & extract or duplicate & extract duplicate :: w a -> w (w a) extend :: (w a -> b) -> w a -> w b extract :: w a -> a extend f = fmap f . duplicate duplicate = extend id liftW :: Comonad w => (a -> b) -> w a -> w b liftW f = extend (f . extract) g_hylo :: (Comonad w, Functor f, Monad m) => (forall a. f (w a) -> w (f a)) -> (forall a. m (f a) -> f (m a)) -> (f (w b) -> b) -> (a -> f (m a)) -> a -> b g_hylo w m f g = extract . hylo (liftW f . w . fmap duplicate) (fmap join . m . liftM g) . return where hylo f g = f . fmap (hylo f g) . g

In the above, w and m are the distributive laws for the comonad and monad respectively, and hylo is a standard hylomorphism. In the style of Dave Menendez's Control.Recursion code it would be a 'refoldWith' and it can rederive a whole lot of recursion and corecursion patterns if not all of them.

Anyone?

Fri 11 Apr 2008

Today I'd like to talk about free monads.

The free monad of a functor is a monad that is uniquely determined by the functor (up to isomorphism, etc), given by:

data Free f a = Roll (f (Free f a)) | Return a -- newtype Free f a = Free { unfree :: Either a (f (Free f a))) }

Usually the above is written up using a newtype around a sum (Either) so you can write it using nice point-free style, but I think this makes for clearer introduction this way.

Wed 26 Mar 2008

[4] Comments

You may recall the definition for an exponential functor from my previous entry, which can also be viewed, I suppose, as functors in the

category of right-invertible functions in Haskell.

class ExpFunctor f where xmap :: (a -> b) -> (b -> a) -> f a -> f b

Clarifying the above, an instance of ExpFunctor should satisfy the slightly generalized version of the Functor laws from Control.Monad:

xmap id id = id xmap f g . xmap f' g' = xmap (f . f') (g' . g)

Since we like to apply xmap to a pair of functions such that f . g = id, as in the Fegaras/Sheard case, we get:

xmap f g . xmap g f = xmap (f . g) (f . g) -- by second xmap law = xmap id id -- by f . g = id = id -- by first xmap law

In any event, what I thought what I'd do today is note that Wouter Swierstra's Data Types a la Carte approach works over exponential functors.

Tue 25 Mar 2008

I have been trying out various representations for higher-order abstract syntax (HOAS) in Haskell, with an eye towards seeing what I can actually use to get real work done and I have run into a few unexpected headaches, and a couple of neat observations. That said, I should probably start by explaining some terminology.

Encoding a language that binds variables in higher order abstract syntax generally involves constructing an abstract data type that contains functions. A functor for representing expressions from Berendregdt's lambda cube in HOAS goes something like (ignoring any consolidation of binders and sorts)

data F a = Lam a (a -> a) | Pi a (a -> a) | App a a | Star | Box

There are a number of mathematical functors that are not instances has Haskell's Functor class, such as the above.

Tue 1 Jan 2008

Wordpress changed the slug of this post, but Planet Haskell has the old link.

Fri 13 Jul 2007

Updated my little type-level 2s and 16s complement integer library to be ghc 6.6 friendly and uploaded it to hackage based on popular (er.. ok, well, singular) demand.

O.K. it was more of a polite request, but I did update it.

Fri 13 Jul 2007

[5] Comments

Recently Eric Kidd and Dan Piponi have used a bit of type hackery by Oleg Kiselyov and -fno-implicit-prelude to build some interesting restricted monads, like the Wadler Set and Bag monads.

There is another interesting monad variation - a parameterized monad - where the monad carries around an additional parameter at the type level such as a type-level set of effects. One really good example of this is the separation logic monad in Hoare Type Theory. The pre- and post- conditions can be viewed as the parameter carried around on that monad. Wadler and Thiemann, Jean-Christophe Filliâtre and others have explore this notion for encoding effects.

Mon 21 May 2007

No Comments

It recently came to my attention that most of the actual code for my old javascript libraries was not accessible from the Wiki. Apparently, I deleted the wrong directory in a spate of cleaning several months back and the links just quietly went dead.

The URL http://comonad.com/jslib.tar.gz contains an archive that is a little out of date, but should contain most of the framework. (In particular the Recompiler seems to be missing pieces) I haven't had a chance to check it for sanity, completeness or consistency.

It relies on the use of the C preprocessor on the back-end. I may have forgotten some scripts it needs to actually build. I just used a linux box with spidermonkey and rhino to test. If there is any interest I'll try to drum up the rest of the pieces and make things functional, but I haven't heard much chatter about these since I moved things over from slipwave.com.

You hereby have the right to use this under the Apache Public License 2.0 with my name substituted in for the Apache Foundation, since thats what I said I would release it under. If you need a more permissive license feel free to ask.

Thu 9 Nov 2006

If we take a look at the Haskell (.) operator:

(.) :: (a -> b) -> (e -> a) -> e -> b

and take a moment to reflect on the type of fmap

fmap :: Functor f => (a -> b) -> f a -> f b

and the unnamed Reader monad from Control.Monad.Reader

instance Functor ((->) r)

we see that fmap applied to the Reader functor rederives (.).

Thu 9 Nov 2006

A number of us from the freenode #haskell channel have gone and formed/revived ##logic to avoid overwhelming the main Haskell channel with traffic. Originally, I just wanted to revive the #logic channel that was already there, but upon talking to the freenode staff, it appears that they have channel naming guidelines that preclude topical discussion channels getting single # names without some sort of clear trademark. They were however nice enough to forward the previous #logic channel to the new location.

In any event, if you are interested in logic at pretty much any level, feel free to stop by the channel.

Wed 1 Nov 2006

Was reading Castagna, Ghelli, and Longo's 1995 paper on "A Calculus for Overloaded Functions with Subtyping" today and in it they have to jump through some hoops to index their '&' types to keep them well behaved under β-reduction.

It seems to me, at least from my back-of-the-envelope scribblings, that if you CPS transform the calculus before, that the main technical innovation (overloaded functions using the tighter run-time type information) remains intact, but the need for this technical trick goes away. In this case you know what the reduction will evaluate out to regardless of call-by-value or call-by-need (just bottom), and if the specification changes during evaluation it is still sound, so no need for an index.

The above then would requires explicit continuations and might interfere with rederiving tupling from the overloading mechanism alone, but seems to eliminate some of the barriers they mention to the higher order case. However, I'm not convinced it is a net win regardless, because it would require a notion of typecase.