Trying to prove Applicative is superclass of Functor, etc

fmap = <*> . pure So we could write for example liftA2 f fa fb = f <$> fa <*> fb
Hi, well aware it's trivial so I'll be terse: do we have?: this way?:
liftA2 f fa fb = pure f <*> fa <*> fb <*>
Incidentally, do we have?:
liftA == liftM == fmap
Thanks!

Oh, and by the way, is it enough then to create an instance of Applicative or Monad to automatically get an instance of the respective superclasses? And the generalization for any superclass/subclass? Would be great... If not why so?

Oh, and by the way, is it enough then to create an instance of Applicative or Monad to automatically get an instance of the respective superclasses? And the generalization for any superclass/subclass? Would be great... If not why so?
I think the latest GHC should be able to give you the superclass instances like you said. Before GHC 7.10 the class hierarchy was a bit disjointed: a Monad was not necessarily an Applicative (even though it should be). https://wiki.haskell.org/Functor-Applicative-Monad_Proposal Daniel

Yes true, subclass, mixed up the terms. ^^ Ah true, I heard about this Dániel. But then it would be generalized to all classes, or just those three ones? Anyway, trying the same with Applicative and its *sub*class Monad:
pure = return (<*>) :: Monad m => m (a -> b) -> m a -> m b mf <*> ma = let mg = mf >>= \f -> return (return . f) in mg >>= \g -> (ma >>= g) As: f :: a -> b return . f :: Monad m => a -> m b mg :: Monad m => m (a -> m b)
Functor f => (a -> b) -> f a -> f b or: Functor f => Applicative f I'm far from an expert in Math, but I'm used to reading (=>) as an implication, but maybe is it completely different? At any rate, if it were an implication, i'd expect it to be written for example (Applicative f => Functor f), to denote maybe that anything being an Applicative should also be a functor (everything in the first is (= must be, in declarative terms) in the second). I mean if we see a class as a set of types (can we btw?)
Is there an easier solution? It's easy enough, but not as trivial as for
Applicative => Functor.
Which leads me to one question I have for a long now. I haven't found my
answer, but perhaps did I not search at the right place...
Why do we write constraints like that:
then if A(pplicative) is superclass of M(onad), A is a superset of M,
because (m in M) => (m in A), hence the direction of the implication arrow,
Monad => Applicative.
Same thing for types of function (and other values), eg (a -> b => Num a),
the type of the function would imply some constraint, which would therefore
imply that no type that doesn't respect the implied term (constraint) can
pretend to be "part" of the type of the function/value.
Maybe I'm misinterpreting the purpose or meaning, but I still wonder what
is the actual meaning then of those (=>) arrows as they don't *seem* to be
implications in the mathematical meaning I'd intuitively imagine.
Thanks both for your answers!
Le vendredi 29 avril 2016, Dániel Arató
Oh, and by the way, is it enough then to create an instance of Applicative or Monad to automatically get an instance of the respective superclasses? And the generalization for any superclass/subclass? Would be great... If not why so?
I think the latest GHC should be able to give you the superclass instances like you said. Before GHC 7.10 the class hierarchy was a bit disjointed: a Monad was not necessarily an Applicative (even though it should be). https://wiki.haskell.org/Functor-Applicative-Monad_Proposal
Daniel _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

Yes true, subclass, mixed up the terms. ^^
Ah true, I heard about this Dániel. But then it would be generalized to all classes, or just those three ones?
Anyway, trying the same with Applicative and its *sub*class Monad:
pure = return (<*>) :: Monad m => m (a -> b) -> m a -> m b mf <*> ma = let mg = mf >>= \f -> return (return . f) in mg >>= \g -> (ma >>= g) As: f :: a -> b return . f :: Monad m => a -> m b mg :: Monad m => m (a -> m b)
Is there an easier solution? It's easy enough, but not as trivial as for Applicative => Functor.
Which leads me to one question I have for a long now. I haven't found my answer, but perhaps did I not search at the right place...
Why do we write constraints like that:
Functor f => (a -> b) -> f a -> f b or: Functor f => Applicative f I'm far from an expert in Math, but I'm used to reading (=>) as an implication, but maybe is it completely different? At any rate, if it were an implication, i'd expect it to be written for example (Applicative f => Functor f), to denote maybe that anything being an Applicative should also be a functor (everything in the first is (= must be, in declarative terms) in the second). I mean if we see a class as a set of types (can we btw?)
Lol, well I said "thanks both" but actually there's only one person. Don't
mind me I'm drunk.
Le vendredi 29 avril 2016, Silent Leaf
Same thing for types of function (and other values), eg (a -> b => Num
a), the type of the function would imply some constraint, which would therefore imply that no type that doesn't respect the implied term (constraint) can pretend to be "part" of the type of the function/value.
Maybe I'm misinterpreting the purpose or meaning, but I still wonder what
is the actual meaning then of those (=>) arrows as they don't *seem* to be implications in the mathematical meaning I'd intuitively imagine.
Thanks both for your answers!
Le vendredi 29 avril 2016, Dániel Arató
a écrit : Oh, and by the way, is it enough then to create an instance of
Applicative
or Monad to automatically get an instance of the respective superclasses? And the generalization for any superclass/subclass? Would be great... If not why so?
I think the latest GHC should be able to give you the superclass instances like you said. Before GHC 7.10 the class hierarchy was a bit disjointed: a Monad was not necessarily an Applicative (even though it should be). https://wiki.haskell.org/Functor-Applicative-Monad_Proposal
Daniel _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

For a drunk person you're getting these equivalences surprisingly right. :)
Ah true, I heard about this Dániel. But then it would be generalized to all classes, or just those three ones?
It would make sense for it to work for any class hierarchy, but honestly I just don't know and I've got an old GHC on my laptop so I can't check. Maybe someone who actually knows will come along and enlighten us. ¯\_(ツ)_/¯
Anyway, trying the same with Applicative and its *sub*class Monad:
pure = return
That's right.
mf <*> ma = let mg = mf >>= \f -> return (return . f) in mg >>= \g -> (ma >>= g)
Is there an easier solution? It's easy enough, but not as trivial as for Applicative => Functor.
I've got (an alpha-equivalent of) the following on a scrap piece of paper: mf <*> mx = mf >>= \f -> mx >>= \x -> return . f $ x It reads nice and fluent.
Why do we write constraints like that:
Functor f => (a -> b) -> f a -> f b or: Functor f => Applicative f
That's a very good question. I agree that it would make a bit more sense if the arrows were reversed. I think it helps to read "Functor f => Applicative f where ..." as "if you've got a Functor then you can have an Applicative if you just implement these functions" as opposed to "if f is a Functor that implies that f is an Applicative" (wrong). Daniel

instance Applicative Maybe => Monad Maybe where ... I don't think I've ever seen something like that but I'm asking just in case, esp as it might precisely be the way to write implied superclasses in
I didn't get this version of ghc already existed! it seems I have it, i'll thus check all that ASAP. Technical question: class constraints should not be written in definitions of instances too, right? Wouldn't be "parametric" anymore and all: the latest ghc(?) Indeed, your definition of (<*>) in terms of monads is much simpler to read! I think I was too much centered on finding a way to replicate the types, to more simply find a way to replicate directly what does the function. Obviously, my def can become yours by some simple operations. Mine:
let left = mf >>= \f -> return $ return . f right = \mg -> ma >>= mg in left >>= right Here with mg = return . f eventually (when called).
Two things bound together, the wrapped value of left (== return.f) being the parameter of the function right. It's clear that the wrapped result is just wrapped so it can be unwrapped immediately after. Might as well not wrap it at all in the first place, and do everything in the first bind operation:
mf >>= \f -> let mg = return . f in ma >>= mg and of course, (mg == \a -> return $ f a).
Anyway, yeah that's also how I read (=>) arrows, obviously, how else to do?
^^ It's just, as most of the syntax and terminology of haskell is based on
what looks like very solid math roots, I imagined the syntax for
constraints was also justified mathematically somehow.
Le vendredi 29 avril 2016, Dániel Arató
For a drunk person you're getting these equivalences surprisingly right. :)
Ah true, I heard about this Dániel. But then it would be generalized to all classes, or just those three ones?
It would make sense for it to work for any class hierarchy, but honestly I just don't know and I've got an old GHC on my laptop so I can't check. Maybe someone who actually knows will come along and enlighten us. ¯\_(ツ)_/¯
Anyway, trying the same with Applicative and its *sub*class Monad:
pure = return
That's right.
mf <*> ma = let mg = mf >>= \f -> return (return . f) in mg >>= \g -> (ma >>= g)
Is there an easier solution? It's easy enough, but not as trivial as for Applicative => Functor.
I've got (an alpha-equivalent of) the following on a scrap piece of paper: mf <*> mx = mf >>= \f -> mx >>= \x -> return . f $ x
It reads nice and fluent.
Why do we write constraints like that:
Functor f => (a -> b) -> f a -> f b or: Functor f => Applicative f
That's a very good question. I agree that it would make a bit more sense if the arrows were reversed. I think it helps to read "Functor f => Applicative f where ..." as "if you've got a Functor then you can have an Applicative if you just implement these functions" as opposed to "if f is a Functor that implies that f is an Applicative" (wrong).
Daniel _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

Well, I think it didn't work. From:
data Foo a = Foo a instance Monad Foo where return = Foo (Foo a) >>= f = f a I got: No instance for (Applicative Foo) arising from the superclasses of an instance declaration In the instance declaration for ‘Monad Foo’
I didn't get this version of ghc already existed! it seems I have it, i'll thus check all that ASAP. Technical question: class constraints should not be written in definitions of instances too, right? Wouldn't be "parametric" anymore and all:
instance Applicative Maybe => Monad Maybe where ... I don't think I've ever seen something like that but I'm asking just in case, esp as it might precisely be the way to write implied superclasses in
Doesn't seem to build 'em automatically. :(
Le vendredi 29 avril 2016, Silent Leaf
Indeed, your definition of (<*>) in terms of monads is much simpler to
Obviously, my def can become yours by some simple operations. Mine:
let left = mf >>= \f -> return $ return . f right = \mg -> ma >>= mg in left >>= right Here with mg = return . f eventually (when called).
Two things bound together, the wrapped value of left (== return.f) being
mf >>= \f -> let mg = return . f in ma >>= mg and of course, (mg == \a -> return $ f a).
Anyway, yeah that's also how I read (=>) arrows, obviously, how else to do? ^^ It's just, as most of the syntax and terminology of haskell is based on what looks like very solid math roots, I imagined the syntax for constraints was also justified mathematically somehow.
Le vendredi 29 avril 2016, Dániel Arató
a écrit : For a drunk person you're getting these equivalences surprisingly right. :)
Ah true, I heard about this Dániel. But then it would be generalized to all classes, or just those three ones?
It would make sense for it to work for any class hierarchy, but honestly I just don't know and I've got an old GHC on my laptop so I can't check. Maybe someone who actually knows will come along and enlighten us. ¯\_(ツ)_/¯
Anyway, trying the same with Applicative and its *sub*class Monad:
pure = return
That's right.
mf <*> ma = let mg = mf >>= \f -> return (return . f) in mg >>= \g -> (ma >>= g)
Is there an easier solution? It's easy enough, but not as trivial as for Applicative => Functor.
I've got (an alpha-equivalent of) the following on a scrap piece of
read! I think I was too much centered on finding a way to replicate the types, to more simply find a way to replicate directly what does the function. the parameter of the function right. It's clear that the wrapped result is just wrapped so it can be unwrapped immediately after. Might as well not wrap it at all in the first place, and do everything in the first bind operation: paper:
mf <*> mx = mf >>= \f -> mx >>= \x -> return . f $ x
It reads nice and fluent.
Why do we write constraints like that:
Functor f => (a -> b) -> f a -> f b or: Functor f => Applicative f
That's a very good question. I agree that it would make a bit more sense if the arrows were reversed. I think it helps to read "Functor f => Applicative f where ..." as "if you've got a Functor then you can have an Applicative if you just implement these functions" as opposed to "if f is a Functor that implies that f is an Applicative" (wrong).
Daniel _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

My understanding is that both the -> and => arrows represent
implication, in the Curry-Howard view of types as proofs. Maybe someone
else can provide better examples of translating back and forth this way.
I'd interpret fmap in English as something like:
`fmap g fa` is a proof that for all f, g, fa, given that f is a Functor
and given g is a function from a to b, and given fa has type `f a`,
there is a value of type `f b`.
You can shuffle things around in other ways, like:
... for all f, g, ... there is a function from `f a` to `f b`.
The => in instance definitions plays a similar role:
Num a => Num (V2 a) where ...
means: For all types a, given that a is a Num, it follows that `V2 a` is
a Num (as proven by the following definitions ...)
A class definition with a superclass requirement means something like:
Functor f => Applicative f where ...
You can show that a type f is an Applicative by providing a proof (type
class instance) that f is a Functor, and proofs (definitions) of the
following class functions.
I hope this helps, and that I've gotten it right.
bergey
On 2016-04-29 at 06:16, Silent Leaf
Which leads me to one question I have for a long now. I haven't found my answer, but perhaps did I not search at the right place...
Why do we write constraints like that:
Functor f => (a -> b) -> f a -> f b or: Functor f => Applicative f I'm far from an expert in Math, but I'm used to reading (=>) as an implication, but maybe is it completely different? At any rate, if it were an implication, i'd expect it to be written for example (Applicative f => Functor f), to denote maybe that anything being an Applicative should also be a functor (everything in the first is (= must be, in declarative terms) in the second). I mean if we see a class as a set of types (can we btw?) then if A(pplicative) is superclass of M(onad), A is a superset of M, because (m in M) => (m in A), hence the direction of the implication arrow, Monad => Applicative.
Same thing for types of function (and other values), eg (a -> b => Num a), the type of the function would imply some constraint, which would therefore imply that no type that doesn't respect the implied term (constraint) can pretend to be "part" of the type of the function/value.
Maybe I'm misinterpreting the purpose or meaning, but I still wonder what is the actual meaning then of those (=>) arrows as they don't *seem* to be implications in the mathematical meaning I'd intuitively imagine.

Excellent answer. I kind of suspected the same but I couldn't quite
find an appropriate translation for "=>".
It's not really implication though. At least not in the same sense as "->". :(
On 29/04/2016, Daniel Bergey
My understanding is that both the -> and => arrows represent implication, in the Curry-Howard view of types as proofs. Maybe someone else can provide better examples of translating back and forth this way. (snip) A class definition with a superclass requirement means something like:
Functor f => Applicative f where ...
You can show that a type f is an Applicative by providing a proof (type class instance) that f is a Functor, and proofs (definitions) of the following class functions.
I hope this helps, and that I've gotten it right.
bergey

I think I got what exactly was the change of ghc 7.10. basically it only adds a constraint Applicative on the Monad class, and same with Functor/Applicative. it doesn't automatically write implied instances, but just forces one to actually write said instances of those superclasses. In short you can't anymore make monads without making Applicatives, "beforehand" (even though order is not important). In my opinion it's pretty shitty. I totally agree that it's (partially) more mathematically correct, and that's great. yet in my opinion, given superclasses can always be derived from their subclasses, it should be mathematically automatic to prove superclass instances by proving any subclass thereof. Otherwise it's forcing the programmer to do even more possibly-useless work (we don't always need applicative and functors for every use of a new monad, do we?) without gaining anything in return but a very abstract idea of "correctness". in short i think if they wanted mathematical correctness they should have added automatic instanciation of superclasses, with possibility to override the default definitions, like they do so with some superfluous methods. Not that write functors or applicative functor instances is actually heavywork, of course, thankfully. I kinda wonder, can we define Applicative methods in function of Monad methods, even though those latter can only be type-valid if the Applicative instance is already created and checked? or maybe we can write a class-neutral version (without constraints)? Say something like that:
-------- version one, with constraints mkAp :: (Monad m, Applicative m) => m (a -> b) -> m a -> m b mkAp mf ma = mf >>= \f -> ma >>= \a -> return $ f a -- (not entirely sure on the necessary constraints of this type signature...) instance Functor f => Applicative f where <*> = mkAp -- the value is automatically different depending on the instance right? pure = return
course, I'm pretty sure mkAp == ap, aka the monad equivalent of (<*>) is automatically defined at instanciation of the monad. But i think to remember it uses fmap, and in theory the idea is that neither instances of Functor or Applicative would yet exist. All depends on the possibility to define a superclass instance in terms of a subclass instance.
-------- version two, without class -- can we use type constructors in signature without classes? mkAp :: (**signature of bind**) -> (a -> m a) -> (( m (a -> b) -> m a -> m b )) mkAp bind return mf ma = ... -- defined in terms of those given class-independent functions
I'mma check myself but if it fails i wonder if anyone knows a way around?

On 2016-04-30 at 15:14, Silent Leaf
I think I got what exactly was the change of ghc 7.10. basically it only adds a constraint Applicative on the Monad class, and same with Functor/Applicative.
7.10 adds the constraint on the Monad class. Prior to 7.10, both Monads and Applicatives already needed to be Functors.
Otherwise it's forcing the programmer to do even more possibly-useless work (we don't always need applicative and functors for every use of a new monad, do we?)
The practical advantage comes when I want to write some code that is generic over Monads. If I can't assume that every Monad is Applicative, my choices are: 1) Write (Applicative m, Monad m) =>, and not work for those Monads 2) Write `ap` everywhere I mean <*>, which for some instances is less efficient 3) Write two versions, one like (1) and one like (2) None of these are very appealing, and orphan instances are a pain, so there's already strong social pressure that any Monad instance on Hackage should have the corresponding Applicative instance defined.
in short i think if they wanted mathematical correctness they should have added automatic instanciation of superclasses, with possibility to override the default definitions, like they do so with some superfluous methods.
Several ways of automatically defining superclasses were discussed as part of the AMP changes. Maybe we'll get one in some future GHC. I don't know the details, but some of the discussion: https://ghc.haskell.org/trac/ghc/wiki/IntrinsicSuperclasses https://ghc.haskell.org/trac/ghc/wiki/DefaultSuperclassInstances https://ghc.haskell.org/trac/ghc/wiki/InstanceTemplates
Not that write functors or applicative functor instances is actually heavywork, of course, thankfully.
You know that if the instances are all in the same module, you can use the Monad functions, right? So the extra work is just pasting in: instance Functor m where fmap = liftM instance Applicative m where pure = return (<*>) = ap

I see, thanks for all this information! Here must be the answer of why,
possibly, liftM is written in terms of monads and not of fmap.
Yes I was saying "not heavywork" at the time I didn't know you could create
an instance of Monad and use its methods to fill the superclasses even
though intuitively it looked like the Monad instance couldn't be accepted
if the superclass weren't already.
Does anyone have an explanation for this?
Le samedi 30 avril 2016, Daniel Bergey
On 2016-04-30 at 15:14, Silent Leaf
wrote: I think I got what exactly was the change of ghc 7.10. basically it only adds a constraint Applicative on the Monad class, and same with Functor/Applicative.
7.10 adds the constraint on the Monad class. Prior to 7.10, both Monads and Applicatives already needed to be Functors.
Otherwise it's forcing the programmer to do even more possibly-useless work (we don't always need applicative and functors for every use of a new monad, do we?)
The practical advantage comes when I want to write some code that is generic over Monads. If I can't assume that every Monad is Applicative, my choices are:
1) Write (Applicative m, Monad m) =>, and not work for those Monads 2) Write `ap` everywhere I mean <*>, which for some instances is less efficient 3) Write two versions, one like (1) and one like (2)
None of these are very appealing, and orphan instances are a pain, so there's already strong social pressure that any Monad instance on Hackage should have the corresponding Applicative instance defined.
in short i think if they wanted mathematical correctness they should have added automatic instanciation of superclasses, with possibility to override the default definitions, like they do so with some superfluous methods.
Several ways of automatically defining superclasses were discussed as part of the AMP changes. Maybe we'll get one in some future GHC. I don't know the details, but some of the discussion:
https://ghc.haskell.org/trac/ghc/wiki/IntrinsicSuperclasses https://ghc.haskell.org/trac/ghc/wiki/DefaultSuperclassInstances https://ghc.haskell.org/trac/ghc/wiki/InstanceTemplates
Not that write functors or applicative functor instances is actually heavywork, of course, thankfully.
You know that if the instances are all in the same module, you can use the Monad functions, right? So the extra work is just pasting in:
instance Functor m where fmap = liftM
instance Applicative m where pure = return (<*>) = ap

Applicative is actually a *sub*class of Functor. :)
Hi, well aware it's trivial so I'll be terse: do we have?:
fmap = <*> . pure
That's right. You have to wrap the "<*>" in parantheses though.
liftA2 f fa fb = f <$> fa <*> fb
So we could write for example this way?:
liftA2 f fa fb = pure f <*> fa <*> fb <*>
You don't need the last "<*>", but other than that yeah, that's exactly right.
Incidentally, do we have?:
liftA == liftM == fmap
Correct. The Prelude defines liftM in terms of do notation though for reasons that escape me. But it's basically just fmap. Daniel
participants (3)
-
Daniel Bergey
-
Dániel Arató
-
Silent Leaf