4

Given a function like negate, it has the type signature:

negate :: Num a => a -> a

which I would describe as a being the type in the context of Num (correct me if you think I am wrong).

But I not fully sure how to describe something like last, which has the type signature:

last :: [a] -> a

My guess would be to say it isn't type-specific, and that it takes a list and produces a single value of the same type as the list. Is this the correct way to think about it?

Jake Jackson
  • 1,055
  • 1
  • 12
  • 34
  • 2
    `Num a` is a "constraint", `Num` is a "type class" / "typeclass", `a -> a` is a "parametrically-polymorphic type", `a` is a "type variable" ( the "parameter" in the ["parametrically-polymorphic"](https://en.wikipedia.org/wiki/Polymorphism_(computer_science)#Parametric_polymorphism) ). `[b] -> b` is a parametrically-polymorphic type, `[b]` is a parametrically-polymorphic type, `b` is a type variable. – Will Ness Feb 08 '21 at 15:51

3 Answers3

6

First, a is not the type in the context of Num, but a type that has a Num instance.

Num a => a -> a is a constrained polymorphic type, while [a] -> a is an unconstrained polymorphic type, or just polymorphic type for short. In the unconstrained case, a can be any type; in the constrained case, it must be a type that obeys the given constraints.

chepner
  • 497,756
  • 71
  • 530
  • 681
3

In negate you need to operate on the element passed, in your case you could apply some operator to it, e.g. (-): negate a = -a.

You cannot define negate for any type, because you need to be able to call (-) on it. You need some guarantee that the argument given will be of some type which supports this operation.

Num is a type class which gives you exactly this - a compile-time guarantee that (-) is supported, and other functions like +, *, too. You can read more about it in the docs

In contrast, last :: [a] -> a does not (need to) do anything on the actual a values. It only accepts them and returns the last one. While negate operates on the a value, here last operates on the list, but does not do anything to its values, it only passes them around. Therefore, it does not need any knowledge about them, and so the type is unconstrained.

Al.G.
  • 4,327
  • 6
  • 31
  • 56
0

last :: [a] -> a is the Haskell98 syntax for the System F type

last :: ∀ a. [a] -> a

The ∀ a can be understood as a kind of type-level lambda binding, i.e. before the actual value level list parameter the function accepts a type-level argument telling what the type of elements contained in the list. This universal quantification makes the function parametrically polymorphic.

Normally, the type variables are automatically inserted by the type checker. In newer GHC Haskell, you can also explicitly apply them:

Prelude> :set -XTypeApplications 
Prelude> :t last @Int
last @Int :: [Int] -> Int
Prelude> last @Double [5,6,7]
7.0

negate is also parametrically polymorphic, but unlike last it does not work truely “for all” types, but only for those that have a Num instance (which both Int and Double do, but not e.g. Char). In other words, it accepts not only an extra argument specifying the type, but also a proof that it does indeed have a Num instance. That too will be inserted automatically by the compiler.

negate :: ∀ a. Num a => a -> a

Prelude> :t negate @Int
negate @Int :: Int -> Int
Prelude> :t negate @Char

<interactive>:1:1: error:
    No instance for (Num Char) arising from a use of ‘negate’
leftaroundabout
  • 117,950
  • 5
  • 174
  • 319