{"id":826,"date":"2009-11-17T09:27:00","date_gmt":"2009-11-17T09:27:00","guid":{"rendered":"http:\/\/scientopia.org\/blogs\/goodmath\/2009\/11\/17\/types-in-haskell-types-are-propositions-programs-are-proofs\/"},"modified":"2009-11-17T09:27:00","modified_gmt":"2009-11-17T09:27:00","slug":"types-in-haskell-types-are-propositions-programs-are-proofs","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2009\/11\/17\/types-in-haskell-types-are-propositions-programs-are-proofs\/","title":{"rendered":"Types in Haskell: Types are Propositions, Programs are Proofs"},"content":{"rendered":"

(This is a revised repost of an earlier part of my Haskell tutorial.)
\n<\/em><\/p>\n

Haskell is a strongly typed language. In fact, the type system in Haskell
\nis both stricter and more expressive than any type system I’ve seen for any
\nnon-functional language. The moment we get beyond writing trivial
\ninteger-based functions, the type system inevitably becomes visible, so we
\nneed to take the time now to talk about it a little bit, in order to
\nunderstand how it works.<\/p>\n

<\/p>\n

One of the most important things to recognize about Haskell’s type system
\nis that it’s based on type inference<\/em>. What that means is that in
\ngeneral, you don’t<\/em> need to provide type declarations. Based on how
\nyou use a value, the compiler can usually figure out what type it is. The net
\neffect is that in many Haskell programs, you don’t write any<\/em> type
\ndeclarations, but your program is still carefully type-checked. You
\ncan<\/em> declare a type for any expression you want, but the only time you
\nmust<\/em> is when something about your code is ambiguous enough that type
\ninference can’t properly select one type for an expression.<\/p>\n

I’m not going to go into a lot of detail, but the basic idea behind
\nHaskell’s type system is that there’s a basic propositional logic of types.
\nEvery type is represented as a statement in the type-logic. So as you’ll see
\nbelow, an integer is written as type Integer<\/code>. A function
\nfrom integers to integers has a type which is an implication statement:
\n“Integer -> Integer<\/code>“, which you can read in the logic as
\n“If the input type is Integer then the output type is Integer”. The
\nway that type inference works is that values with known types become
\npropositions; the basic type inference process s just logical inference
\nover the type logic.<\/p>\n

The type logic is designed so that the inference process, when it analyzes
\nan expression, it will generate the most general<\/em> type; that is, when
\nit’s inferring a type for an expression, it will always pick the most general,
\ninclusive type that can match the expression. And that leads to one
\ncomplication for beginners: Haskell’s type system is almost two different type
\nsystems – a basic type system, and a meta<\/em>-type system. The meta-type
\nsystem is based on something called type classes<\/em>, which group related
\nfamilies of types together. The most general types that come up as a result of
\ntype inference are frequently based on type classes, rather than on specific
\nconcrete types.<\/p>\n

A type-class in code is basically a predicate<\/em> over a type
\nvariable. For example, the type of the parameters to the “+<\/code>”
\noperator must be a numeric type. But since “+<\/code>” can be used on
\nintegers, floats, complex, rationals, and so on, the type of the
\n“+<\/code>” operator’s parameters needs to be something that includes all
\nof those. The way that Haskell says that is the type is “Num a =>
\na<\/code>” – that is, that the type a is a member of the type-class
\nNum<\/code>. The way to understand that is “Some type ‘a’ such that ‘a’ is a
\nnumeric type.”.<\/p>\n

The thing to remember is that essentially, a type-class is a type for
\ntypes. A type<\/em> can be thought of as a predicate which is only true for
\nmembers of that type; a type-class<\/em> is essentially a second-order
\npredicate over types<\/em>, which is only true for types that are members
\nof the type-class. What type-classes do is allow you to define a general
\nconcept<\/em> for grouping together a family of conceptually related types.
\nThen you can write functions whose parameter or return types are formed using
\na type-class; the type class defines a predicate<\/em> which describes the
\nproperties of types that could be used in the function. <\/p>\n

So if we write a function whose parameters need to be numbers, but don’t
\nneed to be a specific kind<\/em> of number, we would write it to use
\na type-class that described the basic properties of numbers. Then you’d be
\nable to use any<\/em> type that satisfied the type-predicate defined
\nby the type-class “Num”.<\/p>\n

If you write a function that uses numeric operations, but you don’t write
\na type declaration, then Haskell’s type-inference system will infer types for
\nit based on the “Num<\/code>” type-class: “Num<\/code>” is the most
\ngeneral type-class of numbers; the more things we actually do<\/em> with
\nnumbers, the more constrained the type becomes. For example, if we use the “\/”
\noperator, instead of inferring that the type of parameter must be an instance
\nof the “Fractional” type-class.<\/p>\n

With that little diversion out of the way, we can get back to talking
\nabout how we’ll use types in Haskell. Types start at the bottom with a bundle
\nof primitive<\/em> atomic types which are built in to the language:
\nInteger<\/code>, Char<\/code>, String<\/code>,
\nBoolean<\/code>, and quite a few more. Using those types, we can
\nconstruct<\/em> more interesting types. For now, the most important
\nconstructed type is a function type<\/em>. In Haskell, functions are just
\nvalues like anything else, and so they need types. The basic form of a simple
\nsingle-parameter function is “a -> b<\/code>“, where “a<\/code>” is
\nthe type of the parameter, and “b<\/code>” is the type of the value
\nreturned by the function.<\/p>\n

So now, let’s go back and look at our factorial function. What’s the type
\nof our basic “fact<\/code>” function? According to Hugs, it’s
\n“Num a => a -> a<\/code>“.<\/p>\n

Definitely not what you might expect. What’s happening is that the system
\nis looking at the expression, and picking the most general type. In fact, the
\nonly things that are done with the parameter are comparison, subtraction, and
\nmultiplication: so the system infers that the the parameter must be a
\nnumber<\/em>, but it can’t infer anything more than that. So it says that
\nthe type of the function parameter is a numeric type; that is, a member of the
\ntype-class “Num<\/code>“; and that the return type of the function is the same as
\nthe type of the parameter. So the statement “Num a => a -> a<\/code>” basically says
\nthat “fact<\/code>” is a function that takes a parameter of some<\/em> type
\nrepresented by a type variable<\/em> “a<\/code>” and returns a value of the
\nsame<\/em> type; and it also says that the type variable “a<\/code>” must be a
\nmember of the meta-type “Num<\/code>“, which is a type-class which includes all of
\nthe numeric types. So according to Haskell, as written the factorial function
\nis a function which takes a parameter of any<\/em> numeric type, and returns a
\nvalue of the same<\/em> numeric type as its parameter.<\/p>\n

If we look at that type, and think about what the factorial function actually
\ndoes, there’s a problem. That type isn’t correct, because factorial is only
\ndefined for integers, and if we pass it a non-integer value as a parameter, it
\nwill never terminate<\/em>! But Haskell can’t figure that out for itself –
\nall 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
\nmost general type for that is a general numeric type. So since we’d like to
\nprevent anyone from mis-calling factorial by passing it a fraction (which will
\nresult in it never terminating), we should put in a type declaration to force
\nit to take the more specific type “Integer -> Integer<\/code>” – that is,
\na function from an integer to an integer. The way that we’d do that is to add
\nan explicit type declaration<\/em> before the function:<\/p>\n

\n> fact :: Integer -> Integer\n> fact 0 = 1\n> fact n = n*fact(n-1)\n<\/pre>\n
 That does it; the compiler accepts the stronger constraint provided by our
\ntype declaration.<\/p>\n
 So what we’ve seen so far is that a function type for a single parameter
\nfunction is created from two other types, joined by the “-><\/code>”
\ntype-constructor. With type-classes mixed in, that can be prefixed<\/em> by
\ntype-class constraints, which specify the type-classes<\/em> of any type
\nvariables in the function type.<\/p>\n
 Before moving on to multiple parameter functions, it’s useful to introduce a
\nlittle bit of syntax. Suppose we have a function like the following:<\/p>\n
\npoly x y = x*x + 2*x*y + y*y\n<\/pre>\n
 That definition is actually a shorthand. Haskell is a lambda calculus based
\nlanguage, so semantically, functions are really just lambda expressions: that
\ndefinition is really just a binding from a name to a lambda expression.<\/p>\n
 In lambda calculus, we’d write a definition like that as:<\/p>\n
\npoly ≡ λ x y . x*x + 2*x*y + y*y\n<\/pre>\n
 Haskell’s syntax is very close to that. The definition in Haskell syntax
\nusing a lambda expression would be:<\/p>\n
\npoly = ( x y -> x*x + 2*x*y + y*y)\n<\/pre>\n
 The λ in the lambda expression is replaced by a backslash, which is the
\ncharacter on most keyboards that most resembles lambda; the “.” becomes an
\narrow.<\/p>\n
 Now, with that out of the way, let’s get back to multi-parameter functions.
\nSuppose we take the poly function, and see what Hugs says about the type:<\/p>\n
\npoly x y = x*x + 2*x*y + y*y\nhugs>  Main> :type poly
\nhugs>  poly :: Num a => a -> a -> a\n<\/pre>\n
 This answer is very surprising to most people: it’s a two<\/em>
\nparameter function. So intuitively, there should by some<\/em> grouping
\noperator for the two parameters, to make the type say “a function that takes
\ntwo a’s, and returns an a”; something like “(a,a) -> a<\/code>“.\n<\/p>\n
 But functions in Haskell are automatically curried<\/em>. Currying is a
\nterm from mathematical logic; it’s based on the idea that if a function is a
\nvalue, then you don’t ever<\/em> need to be able to take more than one parameter.
\nInstead of a two parameter function, you can write a one-parameter function
\nthat returns another one-parameter function. Since that sounds really
\nconfusing, let’s take a moment and look again at our “poly” example:<\/p>\n
\npoly x y = x*x + 2*x*y + y*y\n<\/pre>\n
 Now, suppose we knew that “x” was going to be three. Then we could write a
\nspecial one-parameter function:<\/p>\n
\npoly3 y = 3*3 + 2*3*y + y*y\n<\/pre>\n
 But we don’t<\/em> know “x<\/code>“. But what we can<\/em> do
\nis write a function that takes a parameter<\/em> “x<\/code>“, and
\nreturns a function where all of the references to x<\/code> are filled
\nin, and given a y value, will return the value of the polynomial for x and
\ny:<\/p>\n
\npolyn x = (y -> x*x + 2*x*y + y*y)\n<\/pre>\n
 If we call “polyn 3<\/code>“, the result is exactly what we wrote for
\n“poly3<\/code>“. If we call “polyn a b<\/code>“, it’s semantically
\nexactly<\/em> the same thing as “poly a b<\/code>“. (That doesn’t mean
\nthat the compiler actually implements<\/em> multi-parameter functions by
\ngenerating single-parameter functions; it generates multi-parameters functions
\nthe way you’d expect. But everything behaves<\/em> as if it did.) So what’s
\nthe type of polyn<\/code>? Well, it’s a function that takes a parameter
\nof type a<\/code>; and returns a function<\/em> of type “Num a
\n=> a -> a<\/code>“. So, the type of polyn<\/code> is “Num a => a -> (a ->
\na)<\/code>“; and since the precedence and associativity rules are set up to
\nmake currying convenient, the parents in that aren’t necessary – that’s the
\nsame as “Num a => a -> a -> a<\/code>“. Since “poly<\/code>” and
\n“polyn<\/code>” are supposed to be semantically equivalent, that means
\nthat “poly<\/code>“‘s type must also be “Num a => a -> a ->
\na'\".<\/code><\/p>\n","protected":false},"excerpt":{"rendered":"
(This is a revised repost of an earlier part of my Haskell tutorial.) 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 […]<\/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-826","post","type-post","status-publish","format-standard","hentry","category-haskell"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-dk","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/826","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=826"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/826\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=826"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=826"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=826"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}