[Haskell-cafe] A "commutative diagram" conjecture
about applicative functors
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
>> 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
More information about the Haskell-Cafe
mailing list