Haskell is a strongly typed language. In fact, the type system in Haskell is both stricter and more
\nexpressive than any type system I’ve seen for any non-functional language. The moment we get beyond
\nwriting trivial integer-based functions, the type system inevitably becomes visible, so we need to
\ntake the time now to talk about it a little bit, in order to understand how it works.<\/p>\n
\nOne of the most important things to recognize about Haskell’s type system is that it’s based on *type
\ninference*. What that means is that in general, you *don’t* need to provide type declarations. Based
\non how you use a value, the compiler can usually figure out what type it is. The net effect is that
\nin many Haskell programs, you don’t write *any* type declarations, but your program is still
\ncarefully type-checked. You *can* declare a type for any expression you want, but the only time you
\n*must* is when something about your code is ambiguous enough that type inference can’t properly
\nselect one type for an expression.
\nThe type inference system works on the principle of *most general type*; that is, when it’s inferring
\na type for an expression, it will always pick the most general, inclusive type that can match the
\nexpression. And that leads to one complication for beginners: Haskell’s type system is almost two
\ndifferent 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.
\nThe 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
\nthe parameters to the “`+`” operator must be a numeric type. But since “`+`” can be used on integers,
\nfloats, complex, rationals, and so on, the type of the “`+`” operator’s parameters needs to be
\nsomething that includes all of those. The way that Haskell says that is the type is “`Num a => a`”.
\nThe way to read that is “Some type ‘a’ such that ‘a’ is a numeric type.”.
\nThe thing to remember is that essentially, a type-class is a type for types. A *type* can be thought
\nof as a predicate which is only true for members of that type; a *type-class* is essentially a
\npredicate over *types*, which is only true for types that are members of the type-class. What
\ntype-classes do is allow you to define a *general concept* for grouping together a family of
\nconceptually related types. Then you can write functions whose parameter or return types are formed
\nusing a type-class; the type class defines a *constraint* over a group of types that could be used in
\nthe function. So if we write a function whose parameters need to be numbers, but don’t need to be a
\n*specific kind* of number, we would write it to use Haskell will infer types based on the “`Num`”
\ntype-class: “`Num`” is the most general type-class of numbers; the more things we actually *do* with
\nnumbers, the more constrained the type becomes. For example, if we use the “\/” operator, instead of
\ninferring that the type of parameter must be an instance of the “Fractional” type-class.
\nWith that little diversion out of the way, we can get back to talking about how we’ll use types in
\nHaskell. Types start at the bottom with a bundle of *primitive* atomic types which are built in to
\nthe language: `Integer`, `Char`, `String`, `Boolean`, and quite a few more. Using those types, we can
\n*construct* more interesting types. For now, the most important constructed type is a *function
\ntype*. 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.
\nSo now, let’s go back and look at our factorial function. What’s the type of our basic “`fact`”
\nfunction? According to Hugs, it’s “`Num a => a -> a`”.
\nDefinitely not what you might expect. What’s happening is that the system is looking at the
\nexpression, and picking the most general type. In fact, the only things that are done with the
\nparameter are comparison, subtraction, and multiplication: so the system infers that
\nthe 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
\n“`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
\nincludes 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.
\nIf we look at that type, and think about what the factorial function actually does, there’s
\na problem. That type isn’t correct, because factorial is only defined for integers, and if we pass
\nit a non-integer value as a parameter, it will *never terminate*! But Haskell can’t figure that
\nout for itself – all it knows is that we do three things with the parameter to our function: we
\ncompare it to zero, we subtract from it, and we multiply by it. So Haskell’s most general type for
\nthat is a general numeric type. So since we’d like to prevent anyone from mis-calling factorial by
\npassing it a fraction (which will result in it never terminating), we should put in a type
\ndeclaration to force it to take the more specific type “`Integer -> Integer`” – that is, a function
\nfrom an integer to an integer. The way that we’d do that is to add an *explicit type declaration*
\nbefore the function:
\nfact :: Integer -> Integer
\nfact 0 = 1
\nfact n = n*fact(n-1)
\nThat does it; the compiler accepts the stronger constraint provided by our type declaration.
\nSo what we’ve seen so far is that a function type for a single parameter function is created from two
\nother types, joined by the “`->`” type-constructor. With type-classes mixed in, that can be
\n*prefixed* by type-class constraints, which specify the *type-classes* of any type variables in the
\nfunction type.
\nBefore moving on to multiple parameter functions, it’s useful to introduce a little bit of syntax.
\nSuppose we have a function like the following:
\npoly x y = x*x + 2*x*y + y*y
\nThat definition is actually a shorthand. Haskell is a lambda calculus based language,
\nso semantically, functions are really just lambda expressions: that definition is really just a binding from a name to a lambda expression.
\nIn lambda calculus, we’d write a definition like that as:
\n>poly ≡ λ x y . x*x + 2*x*y + y*y
\nHaskell’s syntax is very close to that. The definition in Haskell syntax
\nusing a lambda expression would be:
\npoly = ( x y -> x*x + 2*x*y + y*y)
\nThe λ in the lambda expression is replaced by a backslash, which is the
\ncharacter on most keyboards that most resembles lambda; the “.” becomes an arrow.
\nNow, 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:
\npoly x y = x*x + 2*x*y + y*y
\n>\tMain> :type poly
\n>\tpoly :: Num a => a -> a -> a
\nThis answer is very surprising to most people: it’s a *two* parameter function. So intuitively, there
\nshould by *some* grouping operator for the two parameters, to make the type say “a function that
\ntakes two a’s, and returns an a”; something like “`(a,a) -> a`”.
\nBut 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:
\npoly x y = x*x + 2*x*y + y*y
\nNow, suppose we knew that “x” was going to be three. Then we could write a special one-parameter function:
\npoly3 y = 3*3 + 2*3*y + y*y
\nBut 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:
\npolyn x = (y -> x*x + 2*x*y + y*y)
\nIf we call “`polyn 3`”, the result is exactly what we wrote for “`poly3`”.
\nIf 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
\ntype `a`; and returns a *function* of type “`Num a => a -> a`”. So, the type of `polyn` is
\n“`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`”.<\/p>\n","protected":false},"excerpt":{"rendered":"
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 […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[89],"tags":[],"class_list":["post-231","post","type-post","status-publish","format-standard","hentry","category-haskell"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-3J","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/231","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=231"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/231\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=231"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=231"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=231"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}