Re: [Haskell-cafe] A commutative diagram conjecture about applicative functors
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
Re: [Haskell-cafe] A commutative diagram conjecture about applicative functors
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) = f (a1 - a) - f a1 - f (Int, a) Here the type annotation applies to the *body* of the lambda abstraction, adding parentheses around the whole thing solve your problem. :t (\f x - fmap ((,) (0::Int)) (f * x)) :: (Applicative f) = f (a1 - a) - f a1 - f (Int, a) Aside from the fact that ghci has some trouble formating the output. Twan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A commutative diagram conjecture about applicative functors
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 * x) :: (Applicative f) = f (a1 - a) - f a1 - f (Int, a) Here the type annotation applies to the *body* of the lambda abstraction, adding parentheses around the whole thing solve your problem. :t (\f x - fmap ((,) (0::Int)) (f * x)) :: (Applicative f) = f (a1 - a) - f a1 - f (Int, a) Aside from the fact that ghci has some trouble formating the output. thank you, oops, how annoying. I wonder if GHCi should output parentheses to make its :type result be a valid expression... Isaac ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] A commutative diagram conjecture about applicative functors
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) McBride and Patterson give four laws for applicative functors in their paper Functional Pearl: Applicative programming with effects. Can these laws be used to prove this conjecture for all applicative functors satisfying those laws? -- Robin P.S. I realise this might not look like a commutative diagram conjecture, but as I said, I've made it more specific - my actual conjecture is more general, but hopefully if I can understand how to prove the specific one, I'll be able to prove my real one in short order. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A commutative diagram conjecture about applicative functors
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: First of all, to avoid getting lost in parenthesis hell, define: let g = (,) (0::Int) let c = (.) fmap second f * fmap g x law: fmap*2 = (pure second * f) * (pure g * x) law: composition = (pure c * (pure second * f)) * pure g * x law: interchange = pure ($g) (pure c * (pure second * f)) * x law: composition = pure c $ pure ($g) * pure c * (pure second * f) * x law: homomorphism*2 = pure (c ($g) c) * (pure second * f) * x simplify = pure (. g) * (pure second * f) * x law: composition = pure c * pure (. g) * pure second * f * x law: homomorphism*2 = pure (c (. g) second) * f * x rewrite (unpl) = pure (\ d u - (0,d u)) * f * x rewrite some more = pure (c g) * f * x law: homomorphism = pure c * pure g * f * x law: composition = pure g * (f * x) law: fmap = fmap g (f * x) Q.E.D. Twan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
