Haskell is a strongly typed language. In fact, the type system in Haskell is both stricter and more
expressive than any type system I’ve seen for any non-functional language. The moment we get beyond
writing trivial integer-based functions, the type system inevitably becomes visible, so we need to
take the time now to talk about it a little bit, in order to understand how it works.
One of the most important things to recognize about Haskell’s type system is that it’s based on *type
inference*. What that means is that in general, you *don’t* need to provide type declarations. Based
on how you use a value, the compiler can usually figure out what type it is. The net effect is that
in many Haskell programs, you don’t write *any* type declarations, but your program is still
carefully type-checked. You *can* declare a type for any expression you want, but the only time you
*must* is when something about your code is ambiguous enough that type inference can’t properly
select one type for an expression.
The type inference system works on the principle of *most general type*; that is, when it’s inferring
a type for an expression, it will always pick the most general, inclusive type that can match the
expression. And that leads to one complication for beginners: Haskell’s type system is almost two
different type systems – a basic type system, and a *meta*-type system. The meta-type system is based on something called *type classes*, which group related families of types together.
The most general types that come up as a result of type inference are frequently based on type classes, rather than on specific concrete types. A type-class in code looks sort of like a *predicate* over a type variable. For example, the type of
the parameters to the “`+`” operator must be a numeric type. But since “`+`” can be used on integers,
floats, complex, rationals, and so on, the type of the “`+`” operator’s parameters needs to be
something that includes all of those. The way that Haskell says that is the type is “`Num a => a`”.
The way to read that is “Some type ‘a’ such that ‘a’ is a numeric type.”.
The thing to remember is that essentially, a type-class is a type for types. A *type* can be thought
of as a predicate which is only true for members of that type; a *type-class* is essentially a
predicate over *types*, which is only true for types that are members of the type-class. What
type-classes do is allow you to define a *general concept* for grouping together a family of
conceptually related types. Then you can write functions whose parameter or return types are formed
using a type-class; the type class defines a *constraint* over a group of types that could be used in
the function. So if we write a function whose parameters need to be numbers, but don’t need to be a
*specific kind* of number, we would write it to use Haskell will infer types based on the “`Num`”
type-class: “`Num`” is the most general type-class of numbers; the more things we actually *do* with
numbers, the more constrained the type becomes. For example, if we use the “/” operator, instead of
inferring that the type of parameter must be an instance of the “Fractional” type-class.
With that little diversion out of the way, we can get back to talking about how we’ll use types in
Haskell. Types start at the bottom with a bundle of *primitive* atomic types which are built in to
the language: `Integer`, `Char`, `String`, `Boolean`, and quite a few more. Using those types, we can
*construct* more interesting types. For now, the most important constructed type is a *function
type*. In Haskell, functions are just values like anything else, and so they need types. The basic form of a simple single-parameter function is “`a -> b`”, where “`a`” is the type of the parameter, and “`b`” is the type of the value returned by the function.
So now, let’s go back and look at our factorial function. What’s the type of our basic “`fact`”
function? According to Hugs, it’s “`Num a => a -> a`”.
Definitely not what you might expect. What’s happening is that the system is looking at the
expression, and picking the most general type. In fact, the only things that are done with the
parameter are comparison, subtraction, and multiplication: so the system infers that
the the parameter must be a *number*, but it can’t infer anything more than that. So it says that the type of the function parameter is a numeric type; that is, a member of the type-class “`Num`”; and that the return type of the function is the same as the type of the parameter. So the statement
“`Num a => a -> a`” basically says that “`fact`” is a function that takes a parameter of *some* type represented by a *type variable* “`a`” and returns a value of the *same* type; and it also says that the type variable “`a`” must be a member of the meta-type “`Num`”, which is a type-class which
includes all of the numeric types. So according to Haskell, as written the factorial function is a function which takes a parameter of *any* numeric type, and returns a value of the *same* numeric type as its parameter.
If we look at that type, and think about what the factorial function actually does, there’s
a problem. That type isn’t correct, because factorial is only defined for integers, and if we pass
it a non-integer value as a parameter, it will *never terminate*! But Haskell can’t figure that
out for itself – all it knows is that we do three things with the parameter to our function: we
compare it to zero, we subtract from it, and we multiply by it. So Haskell’s most general type for
that is a general numeric type. So since we’d like to prevent anyone from mis-calling factorial by
passing it a fraction (which will result in it never terminating), we should put in a type
declaration to force it to take the more specific type “`Integer -> Integer`” – that is, a function
from an integer to an integer. The way that we’d do that is to add an *explicit type declaration*
before the function:
fact :: Integer -> Integer
fact 0 = 1
fact n = n*fact(n-1)
That does it; the compiler accepts the stronger constraint provided by our type declaration.
So what we’ve seen so far is that a function type for a single parameter function is created from two
other types, joined by the “`->`” type-constructor. With type-classes mixed in, that can be
*prefixed* by type-class constraints, which specify the *type-classes* of any type variables in the
function type.
Before moving on to multiple parameter functions, it’s useful to introduce a little bit of syntax.
Suppose we have a function like the following:
poly x y = x*x + 2*x*y + y*y
That definition is actually a shorthand. Haskell is a lambda calculus based language,
so semantically, functions are really just lambda expressions: that definition is really just a binding from a name to a lambda expression.
In lambda calculus, we’d write a definition like that as:
>poly ≡ λ x y . x*x + 2*x*y + y*y
Haskell’s syntax is very close to that. The definition in Haskell syntax
using a lambda expression would be:
poly = ( x y -> x*x + 2*x*y + y*y)
The λ in the lambda expression is replaced by a backslash, which is the
character on most keyboards that most resembles lambda; the “.” becomes an arrow.
Now, with that out of the way, let’s get back to multi-parameter functions. Suppose we take the poly function, and see what Hugs says about the type:
poly x y = x*x + 2*x*y + y*y
> Main> :type poly
> poly :: Num a => a -> a -> a
This answer is very surprising to most people: it’s a *two* parameter function. So intuitively, there
should by *some* grouping operator for the two parameters, to make the type say “a function that
takes two a’s, and returns an a”; something like “`(a,a) -> a`”.
But functions in Haskell are automatically *curried*. Currying is a term from mathematical logic; it’s based on the idea that if a function is a value, then you don’t *ever* need to be able to take more than one parameter. Instead of a two parameter function, you can write a one-parameter function that returns another one-parameter function. Since that sounds really confusing, let’s take a moment and look again at our “poly” example:
poly x y = x*x + 2*x*y + y*y
Now, suppose we knew that “x” was going to be three. Then we could write a special one-parameter function:
poly3 y = 3*3 + 2*3*y + y*y
But we *don’t* know “`x`”. But what we *can* do is write a function that takes a *parameter* “`x`”, and returns a function where all of the references to `x` are filled in, and given a y value, will return the value of the polynomial for x and y:
polyn x = (y -> x*x + 2*x*y + y*y)
If we call “`polyn 3`”, the result is exactly what we wrote for “`poly3`”.
If we call “`polyn a b`”, it’s semantically *exactly* the same thing as “`poly a b`”. (That doesn’t mean that the compiler actually *implements* multi-parameter functions by generating single-parameter functions; it generates multi-parameters functions the way you’d expect. But everything *behaves* as if it did.) So what’s the type of `polyn`? Well, it’s a function that takes a parameter of
type `a`; and returns a *function* of type “`Num a => a -> a`”. So, the type of `polyn` is
“`Num a => a -> (a -> a)`”; and since the precedence and associativity rules are set up to make currying convenient, the parents in that aren’t necessary – that’s the same as “`Num a => a -> a -> a`”. Since “`poly`” and “`polyn`” are supposed to be semantically equivalent, that means that “`poly`”‘s type must also be “`Num a => a -> a -> a`”.
Just to be pedantic, I have to point out that:
is not quite true, e.g.
f xs = ys ++ ys
where
ys :: ???
ys = reverse xs
In vanilla Haskell 98, there’s nothing you can write in there (for ???) that will work. Intuitively, ‘ys’ can be a list of anything, but using ‘[a]’ won’t work, because the compiler won’t be able to match the explicit type variable ‘a’ with the inferred (or explicit) type variable for ‘f’. GHC includes an extension that allows a notation like:
f :: forall a. [a] -> [a]
f xs = ys ++ ys
where
ys :: [a]
ys = reverse xs
The ‘forall a.’ quantification introduces an explicit type variable that is scoped over both the type expression and the function definition, so the type expression for ‘ys’ will work. But without enabling the GHC extension, this won’t work, and there’s no way to specify an explicit type for ys (though there’s no need to).
I mention this to make it appear like I have an incredibly deep knowledge of Haskell (whereas in reality, I just happened to read the whole GHC manual the other day, and came across this extension).
MarkCC, when you said “a meta-type system”, I thought you were going to refer to the kind system, not typeclasses.
In reality of course, the factorial function is only defined on non-negative integers. Is there a way to express that using the type system?
I think that’s the first time I’ve really “gotten” why Haskell expresses types like a -> a -> a. Thanks, Mark!
So… type classes are basically a formalized version of duck typing?
Duck typing implies two things: dynamic equivalence, and equivalence inferred from operations (methods). Haskell’s type classes provide neither. They’re a static typing mechanism, and the compiler doesn’t infer class membership: it must be asserted.
I understand that Haskell doesn’t infer polymorphic recursion, but the type must be provided manually. Why don’t they use something like this: http://citeseer.ist.psu.edu/henglein91type.html
Granted, the type inference is undecidable, but Henglein argues that it won’t be a problem in practice.
Harald: factorial may be defined on non-integers. See http://en.wikipedia.org/wiki/Gamma_function.
To answer your question, though, if you wanted to restrict it to non-negative integers, you could declare a new type that is so restricted.
The Wikipedia article for the gamma function is http://en.wikipedia.org/wiki/Gamma_function — without a period at the end.
Harald Hanche-Olsen – Well, technically speaking, a real factorial (gamma function) would be defined for anything but negative integers (eg, -2.5 should work). However, you are correct in assessing that the type system doesn’t perform static checking on this sort of thing. Runtime checking can be done in this way:
fact :: Integer -> Integer
fact 0 = 1
fact n | n > 0 = n*fact(n-1)
This will complain “Non-exhaustive patterns in function fact” when a negative number is passed. Some haskell tools will also analyze programs and find spots that might fall through pattern matching/trigger an error.
Better yet might be to do this:
fact :: Integer -> Integer
fact 0 = 1
fact n | n > 0 = n*fact(n-1)
fact _ = error “Factorial is inapplicable to negative numbers”
I’m not sure if the error can be statically caught by enabling ghc flags, however I think there are tools/other compilers that manage it.
It is certainly true that advanced type systems can make such situations much better. The languages Epigram, Cayenne, and others are very interesting in this respect.
Anyway, the main article is nice. From the factorial example I realized that a dependant type system might infer constraints based on termination of the function (yes, i know its indeterminate, but for lots of cases it’s clear).
Writing as Haskell tutorial was a great idea…keep up the good work.
Haskell’s typeclasses give you what I like to call bounded parametric polymorphism. That is, they allow you to restrict the set of types over which some type variable ranges.
So this is somewhat like functions being able to say “I don’t care if it’s a duck or whatever, so long as it can quack like one.” and it is somewhat like duck-typing in that regard, with the subtle difference that type variables are only instantiated to one specific type at a time. If you have the type signature (Eq t) => t -> t -> Bool, then both t’s have to be the same type. Also, if you have a function of type (Ord t) => [t] -> [t], then the elements of the list which it takes are still all the same type, even though that type can be any one for which the ordering relations are defined (>=, etc.).
There is an additional extension to Haskell’s type system which is implemented by GHC called existential types, which is what I’d consider to be the right way to handle the extra bit of what duck-typing and/or subtyping polymorphism does (though I admit it is not either one of these).
Basically, you can construct containers where once you put values into them, the construction throws away all knowledge of what type of thing they were except that they belonged to some set of typeclasses. So the only things which are valid to do to elements retrieved from such a container are applying the methods of those typeclasses to them, anything else is a static error. So rather than “It quacks like a duck therefore it is a duck” you have “We’ve completely forgotten everything about it except that it can quack like a duck”.
It might not be immediately obvious why one would want to throw away all the information about a value except that it implements an interface, but this is in fact exactly what one is doing when “upcasting” from a subclass to a superclass in OO. The difference here is that there is no notion of a “downcast”, which is actually a good thing in my opinion — downcasting is a notorious source of bugs.
Now it seems that the C++0x Concepts System is such a reasonable go:-)
Haskell implements type inference by omitting the type specifier, while C++ does so by using ‘auto’, which, IMO, is better for a staticly typed language, ’cause the heads up by using a explicit keyword would help one to figure out whether some variable is implicitly-typed or explicitly-typed.
And also, *Concept* gives a much more formal and explicit description of the kind of meta-type system used in Haskell.
Any way, this is a very clear and specific introduction to the type inference mechanism Haskell employed:-)
Thanks for the information, Mark:)
For more on the formal development of Haskell type classes, I can recommend some papers from the typeclass archive. In particular “How to make ad-hoc polymorphism less ad hoc” (.ps.gz), and
“Functional Programming with Overloading and Higher-Order Polymorphism”.
Particularly the latter is a classic.
Confused. What do you mean by ‘Haskell says?’ What you you have to do to ‘a’ and what query do you make to get Haskell to respond ‘Num a => a”? What is the correspondence between that string and ‘the way to read that?’ (Which ‘a’ is which? Which symbol if any corresponds to ‘such that’ or ‘some’?)
Later on you start talking about ‘the factorial function’ and I was puzzled because you showed many different factorial functions in the last installment including some for which your assertions would not be true (I think). Maybe include the one you are referring to?
Yah, yah, of course I know about the gamma function. But Mark had already restricted attention to the integers (obviously, given what he was doing), and anyway if x is not an integer most people I know would prefer to write Γ(x+1) rather than x! anyhow. (I surely find the latter slightly perverse.)
That said, my thanks to mgsloan for his explanation. I wonder if, given his solution
fact :: Integer -> Integer
fact 0 = 1
fact n | n > 0 = n*fact(n-1)
fact _ = error “Factorial is inapplicable to negative numbers”
a smart Haskell compiler would infer that the checking for n>0 can be done only once and then dispensed with on further iterations? Otherwise, one might be tempted to help out by using a helper function that does not check for negative numbers, while the “front end” fact does the checking, then calls the helper function.
That way of course lurks the unspeakable evil of premature optimization, but that’s a different discussion.
@Peter
Type the function code in a file named fact.hs, fire up Hugs (http://www.haskell.org/hugs/) and load the file. You can either start Hugs like that:
hugs fact.hs
or after starting hugs, load the file with the command:
:l fact.hs
After that you can ask about the type of anything loaded in the current context with the command t:
:t factorial
or
:t [1, 2, 3]
etc.
Peter:
What I meant by “Haskell says” was that the semantics of Haskell dictate that the type inference system of a Haskell implementation would generate that type expression.
The “a” is a type variable – and all of the “a”s in the type expression are the same. The expression is representing *types*, not values. So “a -> a” is a type expression for “a function which takes a parameter of type “a”, and returns a value of the same type”.
The way that I translated the type expression with the type-class constraint isn’t intended to be a literal reading – so there’s no symbol that explicitly represents the “such that” or “some”; that’s just informal terminology for explaining the type expression. In full formality, all variables in type expressions in Haskell are universally quantified, so the real formal type written in logical form would be more like “&forall a; Num(a) => a -> a”, which you could read logically as “for all types a, Num(a) implies a -> a”. In logic, then, we can only instantiate the type with an “a” such that Num(a) is true; otherwise, the logical expression is false.
Does that help?
Thanks for the great post, Mark. Can’t wait for the next in this series!
pongba: “And also, *Concept* gives a much more formal and explicit description of the kind of meta-type system used in Haskell.”
That’s not really true. Haskell’s typeclass system is much, much more “formal” than the current C++ concept proposal.
The main difference is that typeclasses are type-based and concepts are behaviour-based. If a type Foo is a member of Eq in Haskell, that means there is a function (==) of type Foo -> Foo -> Bool. (It also needs to be a mathematical equivalence, but that’s another story.) The point is that this must be a function, so it can be dynamically bound.
In C++, however, if Foo is EqualityTestableConcept, that just means that the expression foo1 == foo2 is convertible to bool. (There are some other restrictions, of course, but again, that’s another story.) This isn’t a function, it’s an expression. There may not be any function bool operator==(const Foo&,const Foo&). There isn’t necessarily one function which does it, since there might be implicit conversions in at least three places in that expression.
In that sense, Haskell’s typeclasses are much more formally and explicitly defined. Typeclasses are a mathematical concept. C++ concepts pull in the rest of C++’s static semantics and name resolution, and hence are defined operationally rather than strictly formally.
Having said that, I do like the C++ proposal, and I think it’s a good fit for the C++ philosophy.
Pseudonym:
I’m afraid you may think of concepts as concepts in 1998, which is defined in the STL document rather than using ‘concept’.
Maybe I’m wrong here. But if you’ve read the most recent concept proposal, you must know that the definition of a concept in C++(may we call C++09 now) can be as strict as you can:
auto concept LessThanComparable {
bool operator
Sorry, but it seems the syntax is messed up by the HTML parser, try again:
auto concept LessThanComparable {
“bool operator
Thanks, ponga, I’ll take a look.
Typeclasses, particularly the Glasgow extentions, actually go much further than the examples in this blog entries. Multi-parameter type classes, for example, can constrain more than one type variable to be part of the same concept in a way that’s much more expressive than C++ concepts. It’s a single, theoretically pure formalism which can express many things for which in C++ you’d use a mix of C++ concepts, template metaprogramming, function overloading and more besides.
> Multi-parameter type classes, for example,
> can constrain more than one type variable
> to be part of the same concept in a way
> that’s much more expressive than C++
> concepts.
Read the C++ Concepts proposal, I’m sure you’ll find something interesting there:-)
Multi-parameter type class is just one thing among others that C++ concepts system supports.
It seems the weird HTML parser messed up my code, so I’m gonna use ” ” to circle around them:
“auto concept Convertible {
operator U(const T&);
}; ”
And this is just a simple one, you can express concepts as complex as you want with the C++ concepts system.
Is there in any of the proposed extensions something that will let you declare a type Positive or Natural a la Ada? An Integer that is typed to be in a certain range, checked at compile time, hopefully with run-time checks inserted where the range constraints can’t be proved?
There are a few different ways to to enforce the positivity constraint for integers at compile time. A quick way (though non-Haskell98) is to add a type signature forcing the argument to be one of the WordN types provided by GHC, though that also forces an upper bound. Another way is to use an alternate non-machine encoding such as Peano encoding (essentially a list of length N represents the integer N), or a string of binary digits, or …
In either case you have to convert to that type, which can fail, but the type system can force you to deal with that.