[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
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.)
More information about the Haskell
mailing list