On Jun 22, 2010, at 1:32 PM, Janis Voigtländer wrote:
A variant of the above statement incorporating type classes is: For every given type a and function f :: forall b . Monoid b => ((a -> b) -> b) one of the following cases holds: there exists x such that f = \k -> k x f = \_ -> mempty there exists g and h such that f = \k -> g k `mappend` h k
My take would be: for any a and f as you mention, there is a list l:: [a] such that
f k = foldr mappend mempty (map k l)
That makes sense because (I think) the type newtype FreeMonoid a = FreeMonoid { (>>-) :: forall m . Monoid m => (a -> m) -> m } is a free monoid over a and, thus, isomorphic to [a] : First, `FreeMonoid a` is a monoid via instance Monoid (FreeMonoid a) where mempty = FreeMonoid (\_ -> mempty) a `mappend` b = FreeMonoid (\k -> (a >>- k) `mappend` (b >>- k)) Second, for every monoid m and mapping `f :: a -> m` there is a unique monoid homomorphism from `FreeMonoid a` to m , namely `(>>- f)` . It follows that `(>>-(:[]))` and `foldr mappend mempty` are monoid isomorphisms. I am interested in the mentioned laws because I want to show the monad laws for the definition instance Monad FreeMonoid where return x = FreeMonoid ($x) a >>= f = a >>- f This definition of `>>=` is *not* the usual one for continuation monads, but if the mentioned properties hold, I think it also satisfies the monad laws. The theorem
forall a. (F a -> a) -> a = μ F
looks interesting. I wonder whether it could be adapted to incorporate a type-class constraint. I'll also look into Phil Wadler's draft on Recursive types for free. Thanks! Sebastian -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)