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.)
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
