[Haskell] Announce: revamped free theorems generator

[Sebastian Fischer]

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