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.