What Does the => Symbol Do in Haskell?

haskell

I'm fairly new to learning haskell, so I don't really understand the typing system when it comes to constraints. There's this weird => symbol that doesn't make sense to me. Is it actually just syntax? Or is it a type constructor? I'm not sure. Below are my thoughts about it. Can someone clarify what exactly => means in haskell?

In haskell, (->) is a type constructor, with kind * -> * -> *. This is nice, because it makes it clear why, for example, Double -> Bool has kind *. But then I wondered about types like (Integral a) => a -> a. Clearly, this has kind *, and a -> a has kind * (I think). Since Integral has kind * -> Constraint, Integral a must have kind Constraint. Then, I conclude that (=>) has kind Constraint -> * -> *. However, when I type :k (=>) in GHCi, I get an error ("parse error on input =>")! This seems to indicate that (=>) is not a type constructor. Then what is it?

GHCi also tells me that (Show List, Read List) has kind Constraint, but that (,) has kind * -> * -> *, which makes me very confused. Does (,) have two definitions? Are constraints some magical hocus-pocus that I just don't understand?

Any help is greatly appreciated.

Best Answer

The => is just there as a delimiter between context and type when you write a type signature. They aren't even saved after compilation. You can see it here: http://www.haskell.org/onlinereport/syntax-iso.html

Related Solutions

Does haskell have dependent types

Haskell doesn't quite have full dependent types, although it can get very close with extensions like DataKinds and TypeFamilies. The issue at the moment, as far as I know, is that value-level Haskell has explicit bottoms but type-level Haskell does not.

This doesn't stop you from parametrizing types over other types, including the DataKind-lifting of values. As of GHC 7.6, and with DataKinds enabled, you can use type-level naturals and strings, as well as type-level tuples, type-level lists, and the type-level liftings of any (non-higher-kinded, non-generalized, non-constrained) algebraic data types, which is similar to (but much more general than) C++'s ability to use integers in templates.

The logic behind the use of different arrows (-> <-) in Haskell

I've also always found it kind of odd that regular functions are defined with = but lambdas with ->. Why not use the arrow for both? Or the equals for both?

The equality symbol makes sense for named function definitions because it states that applying the named function to its arguments is equivalent to evaluating the right hand side of the equation. Defining lambdas that way makes no sense notationally: x = x + 1 implies x is equal to its successor, which can't be true.

The left arrow gets used in do notation as something similar to variable binding, in list comprehensions for the same (I'm assuming they are the same, as list comprehensions look like condensed do blocks), and in pattern guards, which have the form (p <- e).

All of those constructs bind a new variable. Using = here would not make much sense either, because a statement such as x = x + 1 implies that x refers to the same thing on both sides. A variable binding introduces a new x that's distinct from any x that may occur in the right hand side.

One alternative would've been to just use -> and place the variable on the right, but I believe placing it on the left is objectively more readable in cultures that read left to right. You scan text by moving your eyes along the left margin and thus placing all the variables on the left makes them easier to find. And although having two different symbols for variable bindings may not seem consistent, there's consistency in the position of the variable that gets bound; it's always on the left.

So that just leaves the question of why <- as opposed to some other symbol like :=. I don't know, but I can guess. Look at what desugared monadic code looks like:

[1, 2, 3] >>= \xs -> map (*2) xs

Considering that >>= with its arguments swapped is called =<<, it probably seemed natural to use a left-facing arrow.

Best Answer

Related Solutions

Does haskell have dependent types

The logic behind the use of different arrows (-> <-) in Haskell

Related Topic