Isaac Dupree isaacdupree at charter.net
Mon Dec 31 07:06:34 EST 2007

```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
>> 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
```