# [Haskell] Announce: revamped free theorems generator

Sebastian Fischer sebf at informatik.uni-kiel.de
Tue Jun 22 11:20:41 EDT 2010

```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

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

The theorem

> forall a. (F a -> a) -> a = μ F

looks interesting. I wonder whether it could be adapted to incorporate
a type-class constraint.

Thanks!
Sebastian

--
Underestimating the novelty of the future is a time-honored tradition.
(D.G.)

```