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