Twan van Laarhoven wrote:
Isaac Dupree wrote:
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
Isaac Dupree wrote:
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)
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 co
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
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
