Campaign for real turnstiles

Veronika Romashkina has an excellent blogpost “Arrows Zoo”, which mostly explains the several semantically distinct uses of the symbols -> and <- in Haskell.

It gives a brief mention of =>, but in fact there are two very different uses of this arrow, and I think the difference between them is liable to confuse. They are:

=> as implication

The => symbol resembles the mathematical symbol ⇒, which denotes implication: to a mathematician “p ⇒ q” means “p implies q”, which is the same thing as “if p, then q”.

Within constraints themselves, the => symbol has been usable since the QuantifiedConstraints extension was made available in GHC 8.6.1, and implication is the only interpretation of it. The example given in the manual is of trees parametric in the data structure used in the branches, as well as in the leaves:

data Rose f a = Branch a (f (Rose f a))

instance (Eq a, forall b. (Eq b) => Eq (f b))
      => Eq (Rose f a)
  where
    (Branch x1 c1) == (Branch x2 c2)
      = x1==x2 && c1==c2

The use of => within the constraint is an implication: “if b has a notion of equality so does f b”.

=> as turnstile

The more common use of =>, however, is to separate contexts from class definitions and instances. This can’t be seen to stand for ⇒: it is what type theorists write as ⊢ (the “turnstile”). When one writes

class Eq a => Ord a

that means “in order for it to make sense to talk about a being an ordered type, we must know that a has a notion of equality”.

This is not an implication. It does in fact create an implication, but it’s the wrong way around: we have Ord a => Eq a: if a is ordered then certainly a has a notion of equality.

Instance definitions are slightly closer to implications, but behave somewhat differently: if we write

instance Ord k => Ord (Set k)

then there is not just an implication but an equivalence (assuming we are not using the IncoherentInstances language extension, whose use is rare and problematic anyway): if k has an ordering then Set k does, but also if Set k has an ordering then k does (since, without incoherent instances, there can be no other way to order Set k).

Moralising

It would probably be better if Haskell used a proper turnstyle symbol instead of =>. Notation that makes it clear that one is an implication and the other delimits a context would be better.

As anyone who’s marked a lot of undergraduate mathematics knows, some students have a compulsion to indicate the structure of their argument with arrows, despite the fact that (or maybe because) it obscures the actual relationship between the things being connected. “This enables us to talk about” is different from “this implies”, and there doesn’t seem like there’s a very good excuse for using the same notation.