I know a bit of category theory, but I'm trying to look at it from a
fundamental perspective; I know that I intend (m :-> n) to mean "natural
transformation from functor m to functor n", but the type itself (forall x.
m x -> n x) doesn't necessarily enforce that.
However, the type of natural transformations comes with a free theorem, for
example
concat :: [[a]] -> [a]
has the free theorem
forall f :: a -> b, f strict and total, fmap f . concat = concat . fmap
(fmap f)
The strictness condition is needed; consider
broken_concat :: [[a]] -> [a]
broken_concat _ = [undefined]
f = const ()
fmap f (broken_concat []) = fmap f [undefined] = [()]
broken_concat (fmap (fmap f) []) = broken_concat [] = [undefined]
The 'taming selective strictness' version of the free theorem generator[1]
allows removing the totality condition on f, but not the strictness
condition.
But in the case of concat, you can prove a stronger theorem:
forall f :: a -> b, fmap f . concat = concat . fmap (fmap f)
My suspicion is that this stronger theorem holds for all strict and total
natural transformations, but I don't know how to go about proving that
suspicion. I'm a hobbyist mathematician and a professional programmer, not
the other way around :)
I think it's probably easy to prove that the monoid laws imply that mult'
and one' are strict and total.
> Thus, you can in principle define plenty of natural transformations which
do not have the type f :: forall X. M X -> N X.
Can you suggest one? I don't see how you can get around f needing to act
at multiple types since it can occur before and after g's fmap:
fmap g . f = f . fmap g
M A --fmap_M g--> M B
| |
f_A f_B
| |
v v
N A --fmap_N g--> N B
You can have n = m, of course, but that just means f :: M :-> M.
-- ryan
[1] http://www-ps.iai.uni-bonn.de/cgi-bin/polyseq.cgi
Use this term:
/\a. let flipappend =(\xs :: [a]. fix (\rec :: [a] -> [a]. \ys :: [a].
case ys of { [] -> xs; y:zs -> y : rec zs })) in
let concat = fix (\rec :: [[a]] -> [a]. \xss :: [[a]].
case xss of { [] -> []_{a}; xs:yss -> flipappend
(rec yss) xs}) in
concat
[2] See http://hpaste.org/56903 Summary:
-- both of these types have obvious Functor instances
newtype (f :. g) x = O (f (g x))
data Id x = Id x
class Functor m => Monad m where
one' :: Id :-> m
mult' :: (m :. m) :-> m
-- instances are required to satisfy monoid laws:
-- one' is a left/right identity for mult':
-- forall x :: m a
-- mult' . O . one' . Id $ x = x = mult' . O . fmap (one' . Id)
$ x
-- mult' is associative:
-- forall x :: m (m (m a))).
-- mult' . O . mult' . O $ x = mult' . O . fmap (mult' . O) $ x
On Thu, Jan 26, 2012 at 9:30 PM, wren ng thornton <w...@freegeek.org> wrote:
> On 1/23/12 10:39 PM, Ryan Ingram wrote:
>
>> type m :-> n = (forall x. m x -> n x)
>> class Functor f where fmap :: forall a b. (a -> b) -> f a -> f b
>> -- Functor identity law: fmap id = id
>> -- Functor composition law fmap (f . g) = fmap f . fmap g
>>
>> Given Functors m and n, natural transformation f :: m :-> n, and g :: a ->
>> b, how can I prove (f . fmap_m g) = (fmap_n g . f)?
>>
>
> That is the defining property of natural transformations. To prove it for
> polymorphic functions in Haskell you'll probably want to leverage
> parametricity.
>
>
> I assume you don't know category theory, based on other emails in this
> thread. But the definition of a natural transformation is that it is a
> family of morphisms/functions { f_X :: M X -> N X | X an object/type } such
> that for all g :: a -> b we have that f_b . fmap_m g == fmap_n g . f_a
>
> Thus, you can in principle define plenty of natural transformations which
> do not have the type f :: forall X. M X -> N X. The only requirement is
> that the family of morphisms obeys that equation. It's nice however that if
> a function has that type, then it is guaranteed to satisfy the equation (so
> long as it doesn't break the rules by playing with strictness or other
> things that make it so Hask isn't actually a category).
>
> --
> Live well,
> ~wren
>
>
> ______________________________**_________________
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
