[Haskell-cafe] A "commutative diagram" conjecture about applicative functors

[Isaac Dupree]

Twan van Laarhoven wrote:
> Robin Green wrote:
> 
>> I am proving various statements relating to applicative functors, using
>> the Coq proof assistant (I am considering only Coq terms, which always
>> terminate so you don't have to worry about _|_). However, I'm not sure
>> how to go about proving a certain conjecture, which, translated back
>> into Haskell and made more specific to make it easier to think about,
>> looks like this (assuming Control.Applicative and Control.Arrow are
>> imported):
>>
>> "For all applicative functors:
>>
>> \f x -> fmap second f <*> fmap ((,) (0::Int)) x
>>
>> is equivalent to
>>
>> \f x -> fmap ((,) (0::Int)) (f <*> x)"
> 
> Using the laws from the Control.Applicative haddock page, and some 
> puzzling:

good!  I was still confused whether 'second' was necessarily in the (,) 
arrow (it is, here).  So I used GHCi (6.8.2), and seemed to discover a 
GHC bug afterwards?


Prelude Control.Arrow Control.Applicative
 > :t \f x -> fmap second f <*> fmap ((,) (0::Int)) x
\f x -> fmap second f <*> fmap ((,) (0::Int)) x
    :: (Applicative f) => f (b -> c) -> f b -> f (Int, c)

 > :t \f x -> fmap ((,) (0::Int)) (f <*> x)
\f x -> fmap ((,) (0::Int)) (f <*> x)
    :: (Applicative f) => f (a1 -> a) -> f a1 -> f (Int, a)

Unfortunately, I get puzzling type errors if I annotate either one of 
them with their type (e.g.
(Applicative f) => f (a -> b) -> f a -> f (Int, b)
) in an expression.  The very answer doesn't seem to typecheck.


 > :t \f x -> fmap ((,) (0::Int)) (f <*> x) :: (Applicative f) => f (a1 
-> a) -> f a1 -> f (Int, a)

<interactive>:1:14:
     Couldn't match expected type `f a1 -> f (Int, a)'
            against inferred type `(Int, a11)'
     Probable cause: `(,)' is applied to too many arguments
     In the first argument of `fmap', namely `((,) (0 :: Int))'
     In the expression:
           fmap ((,) (0 :: Int)) (f <*> x) ::
             (Applicative f) => f (a1 -> a) -> f a1 -> f (Int, a)

 > :t \f x -> fmap second f <*> fmap ((,) (0::Int)) x :: (Applicative f) 
=> f (b -> c) -> f b -> f (Int, c)

<interactive>:1:13:
     Couldn't match expected type `f b -> f (Int, c)'
            against inferred type `(d, c1)'
     Probable cause: `second' is applied to too many arguments
     In the first argument of `fmap', namely `second'
     In the first argument of `(<*>)', namely `fmap second f'

Of course if I leave out ":t" and leave out all type signatures then it 
complains that it needs monomorphism, which is fair, but...

 > \f x -> fmap second f <*> fmap ((,) (0::Int)) x 


<interactive>:1:8:
     Ambiguous type variable `f' in the constraint:
       `Applicative f' arising from a use of `<*>' at <interactive>:1:8-46
     Probable fix: add a type signature that fixes these type variable(s)



Isaac