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 $\perp$ Functor that maps everything to $\perp$, 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.

Source Code

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

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?

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.

(more...)

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.

(more...)

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.

(more...)

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

Here is the actual content.

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.

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.

(more...)

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.

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 (.).

(more...)

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.

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.

 \inference{\Gamma \vdash M:W_1 \leq \lbrace\neg U_i\rbrace_{i\leq(n-1)} & \Gamma \vdash N : W_2 \leq \neg U_n}{\Gamma \vdash (M \binampersand N) : \lbrace \neg U_i \rbrace_{i \leq n }}[$\lbrace\rbrace$-I]

 \inference{\Gamma \vdash M : \lbrace \neg U_i \rbrace_{i \in I} & \Gamma \vdash N : U & U_j = \min_{i \in I} \lbrace U_i \vert U \leq U_i \rbrace } {\Gamma \vdash M \bullet N : \perp }[$\lbrace\rbrace$-E]

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.

I almost have the blog integrated with the old slipwave wiki content. I kludged something together to display it in WordPress. While I may add a flashy dynamic in-page loading feature like TiddlyWiki, for right now its functional and backwards compatible with my old content and gracefully degrades in the absence of javascript.

By way of example, you might try to view some Haskell source code.

This also might provide better context when I start to talk about things like continuations because I can link right inline to more extended static content.

This also provides me with a more convenient venue for static content than WordPress' default page management system.

Please, let me know if some bit of markup doesn't show up right.

 
 
import qualified Control.Comonad as Comonad
import qualified Edward hiding (personal_details)
import Blog.Software
 
-- Hello, World!
 
instance Blog Comonad.Reader where
    url = "http://comonad.com/reader"
    author = Edward.Kmett
 
main = forever $ post stuff
 

Syntax highlighting works.

 \inference{}{\Gamma, x:\tau \vdash x:\tau}[var]

 \inference{\Gamma,x:\sigma \vdash M:\tau}{\Gamma \vdash \lambda x : \sigma. M : \sigma \rightarrow \tau}[abs]

 \inference{\Gamma \vdash M : \sigma \rightarrow \tau & \Gamma \vdash N:\sigma}{\Gamma \vdash M N : \tau}[app]

Apparently, \LaTeX works.

\bfig \square/>>`>`>` >->/[A`B`C`D;e`f`g`m] \morphism(500,500)|m|/.>/< -500,-500>[B`C;h] \efig

Commutative diagrams, check.

All systems go.

World, meet blog; blog, meet world.

« Previous Page