The Comonad.Reader

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