The Comonad.Reader

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.

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.

Apparently, works.

Commutative diagrams, check.

All systems go.

World, meet blog; blog, meet world.