[Haskell-beginners] Trying to prove Applicative is superclass of Functor, etc

[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.

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 <silent.leaf0 at gmail.com> wrote:
> 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.