Skip to content
March 13, 2011 / cdsmith

Haskell’s Niche: Hard Problems

(This post isn’t really intended for experienced Haskell programmers.  It has no source code, and is a tad philosophical in tone.  You have been warned!)

A particularly trite phrase that reflexively comes up in programming language discussions is “use the right tool for the job.”  The notion is that different programming languages are good at different things, and that a software developer should be prepared to make different choices about their programming language depending on the characteristics of the problem they are trying to solve.

In some cases, this is obviously true: many programming languages are designed to play a niche role in software projects.  Other languages are more general purpose.  Nevertheless, many people are inclined to look for “the job” that a given language does well, and any language community ought to have a well considered answer.  What is the “job” for which you most think of this language as the right tool?

This is my answer for Haskell: Haskell’s “job” is solving hard problems.

At first, this might seem evasive or dishonest, or like another way of just saying Haskell is great; but that is not what I mean.  After all, a very small percentage of software is actually about solving hard problems.  If the task at hand is to make sure that the user’s password has at least 6 characters, and at least one digit or punctuation symbol, then most of us could probably whip up an implementation in any of a dozen different programming languages in 15 minutes or less.  The great majority of software development is like that.  You know the task, you understand what’s supposed to happen, and you just need to write it.

But then there’s the hard stuff: you need to find the right heuristics to interpret some fuzzy data, or optimize a process, or search a space of possible solutions… but you don’t start out with a clear idea of what you’re doing, what the right answers will be, and/or how to go about the task.  Those are the programming jobs where Haskell shines.  I’ll give three reasons for that.

Reason 1: Haskell shines at domain specific languages.

The first thing you want to do when you approach a difficult problem is to find the right notation and language to discuss it.  This step is absolutely crucial: entire fields of human knowledge have been held back by poor notation, and conversely have experienced something like a renaissance when better notation is introduced.  In programming communities, we call this idea domain specific languages, and if you can embed a domain specific language into the programming language you’re using, things that looked very difficult can start to appear doable.

Haskell, of course, excels at this.  If you look over a list of, say, the top 40 programming languages in use today, the three that have the most promise for domain specific languages would likely be Lisp, Haskell, and Ruby.  (Side note: this isn’t meant to unfairly slight languages like Factor that also excel in this area but don’t meet the arbitrary popularity line.)  Ruby does an adequate job while remaining basically a traditional modern language — object oriented and imperative.  Lisp is defined by this idea, and it dominates the language design, but sometimes at the cost of having a clean combinatorial approach to putting different notation together.  Haskell sits in the middle, with a clean and quiet syntax, arbitrary operators, lazy evaluation, combinatorial programming, and advanced type system features that together to let you build quite powerful and flexible embedded languages and notations and mix them cleanly.

Reason 2: Haskell shines at naming ideas.

The second crucial step to solving problems you didn’t already know how to solve is to start naming things.  If you watch people tackle difficult tasks in many other areas of life, you’ll notice this common thread.  You can’t talk about something until you have a name for it.  Programming languages are also largely built around naming things; but a lot of mainstream languages are limited in terms of what kinds of ideas can be expressed in the language and assigned a name.  One question you might ask of a language is how many things it lets you describe and name.

Haskell scores quite well on that count.  Monoids, for example, are pervasive and used frequently in many programming languages; but only in Haskell are they named in the standard library.  It’s common to hear “you can use monads in this language; but you can’t express the idea of a monad in the language itself.”  Giving things names is a more universal fact of Haskell programming than in any other language I’m aware of.  In this way, as well, programming in Haskell meshes very well with good practice in difficult problem-solving.

Reason 3: Haskell shines at making frequent fundamental changes.

Finally, a crucial aspect of difficult problem solving is that you’re frequently wrong.  You pursue an idea for a long time, only to discover that you had something backwards in an important way, and need to make some pervasive changes throughout your work.  Note that the maintenance programmer’s “surgical modification” style is a horrible idea here; the last thing you want, when you’re already working at the limits of your ability, is to wade through code whose structure arose out of your past major mistakes.  Rather, what you need is a way to make deep structural changes to your code, and still end up with a fair amount of confidence that the result is at least reasonable, that you haven’t forgotten something big.

Unit testing won’t do the job; there are just too many false failures, since making such a large change tends to invalidate huge swaths of your unit tests anyway.  You already know that they won’t work, because you deleted or changed the arguments to the pieces that you were testing.  Indeed, while test-driven development works great for the vast majority of programming tasks that fall squarely in the “not difficult” category, it has a tendency to crystallize the code a bit quickly here.  You don’t want to be told about and need to fix every place something changed; you want to know specifically when you’ve made changes that are not consistent between themselves.

That, of course, is the job of a type system.  Haskell has undoubtedly the most advanced type system of any popular language (let’s say “top 40” again) in use today.  This gives you (if you actually use it, rather than avoiding it and shutting it up!) the ability to make a large change that will affect the structure of your code, and know for sure that you’ve hit all the places where that change makes a difference.  Indeed, the type checker can direct your attention to what remains to be updated.  We’re not even talking about errors that look reasonable but contain subtle mistakes; those will need to be caught with some combination of careful thought and testing.  We’re talking about the kind of errors that would cry out at you if you reread that bit of code; but came into being because of a circuitous route of refactoring.  To quote Benjamin Pierce, “Attempting to prove any nontrivial theorem about your program will expose lots of bugs: The particular choice of theorem makes little difference!”  This is especially true when you’re dealing with rapidly changing code.

That, then, is the answer I give for what Haskell is the “right tool” for.  To be sure, there are a number of more specific answers, parallelism being a popular one.  But these are in a sense misleading.  Unlike, say, Erlang, Haskell was not designed for parallel programming; its usefulness for that task has arisen after the fact.  Indeed, parallelism in a sense qualifies as one of the hard problems for which Haskell is well-suited.  I also don’t mean to claim that Haskell is miserable at easy tasks; indeed, I use it routinely for the sort of thing many UNIX experts would pull out shell scripting and Perl.  But I am bold enough to say that those tasks are not where its shows to its best advantage.

That’s my slogan, then.  Haskell is for solving hard problems.

February 5, 2011 / cdsmith

HTML 5 in Haskell

I’ve just released the first version of the xmlhtml package, which is part of the Snap framework.  The purpose of the package is to be a common parser and renderer for both HTML 5 and XML.  I’m writing here to talk about what the package is, its goals and design choices, and so on.

Context: Heist and Hexpat

The Snap project includes a templating engine called Heist.  Since I didn’t write it, I can say that it is, in my opinion, the best model for real page template engines that exists.  If you’re generating very dynamic HTML using Haskell code, there are nice options like blaze; but if you want a template system, I think Heist is the clear choice.  It’s simple, easy to understand, and extremely powerful.

Under the hood, Heist works with hexpat, a wrapper around the native expat library for handling XML documents.  Unfortunately, HTML isn’t really XML, and it’s sometimes difficult to build pages that are valid XML and make use of a variety of client-side web techniques.  Some problems that arose:

  • JavaScript makes frequent use of reserved XML characters like ‘<‘, ‘&’, etc.  HTML-based browsers accept these without complaint, terminating the JavaScript only when it finds a closing script tag.
  • CSS is similar; special characters can occur in valid CSS, but are not okay in XML documents.
  • The converse problem exists as well; hexpat will escape special characters in text as entities, but web browsers that don’t expect that then won’t parse the code correctly.
  • Some tags like textarea and object need to have explicit close tags to be understood by many web browsers and be valid HTML 5.  Hexpat renders that as empty tags instead, with a slash in the start tag.
  • HTML allows certain end tags to be omitted; for example, end tags on list item, paragraphs, etc.  Hexpat is an XML parser, though, and insisted on close tags.
  • Hexpat insists on a single root element, as is the custom for XML.  However, Heist templates are allowed to have many root elements.  The tricks to work around this in Heist had bad effects on other bits, such as DTD declarations.  Better to have a proper parser that can understand multiple roots.

There are dozens of other such incompatibilities, and they formed a constant source of annoyance for Heist users.

The Answer: xmlhtml

To address these outstanding issues in Heist, I built a new library for handling both XML and HTML 5, which is creatively named xmlhtml.  Since this is a huge design space, we narrowed down the intent of the library as follows:

  • The intended use is for working with documents under your own control.  This includes, for example, the templates in a web application.
  • We support 99% of both XML and HTML 5.  We leave out a few small things on both sides (most notably, processing instructions are silently ignored in XML).
  • We use the same types for both HTML and XML, so you can write code to work with both seamlessly.
  • We focus on keeping the type as simple and small as possible.  The types and public API are designed to be as simple as possible.

The first point is crucial to keeping the project manageable.  The latest draft HTML 5 specification contains over a hundred pages of intricate parsing rules designed to match the quirky behavior of 20 years worth of web browsers.  While it might be useful to implement these rules for writing web spiders, screen scraping, and such; the result would be too complex for working with clean, controlled documents.

At the same time, it was important to us not to take compatibility and standards lightly.  While we don’t adhere to all of the standards all of the time, we differ in controlled ways that are important for the application we have in mind.

Simplicity was also a huge design goal.  There’s a tendency in Haskell for libraries to get more and more generic over time, to the point that actual honest-to-goodness types are few and far between!  One goal of xmlhtml was to just go ahead and decide the types for you.  So text is represented with the Text type from Bryan O’Sullivan’s package, which is now part of the Haskell Platform.  Lists are lists, attributes and tags are also text… you don’t have to track down a hundred type variables to understand the types in the package.  If you want to convert to a different type, you can; but the xmlhtml Document type uses the types that it uses.

This fills a space that I think is pretty much unoccupied in Haskell so far.  For parsing and rendering valid XML, there’s hexpat.  For handling arbitrary and possible invalid HTML, there is TagSoup.  But for handling your own documents using both HTML and XML features, and without requiring detective work to figure out how to use it, this is the way to go.

A Brief Introduction

It’s dead simple to make basic use of the package.  The module Text.XmlHtml exports parsing and rendering functions:

  • parseXML and parseHTML: These are the starting points for parsing documents.  The result is a Document value containing the detected character encoding, document type and the content of the document.
  • render: This is the renderer.  The result is a Builder object from the blaze-builder package.  You can use blaze-builder’s toByteString if you prefer it in that form, but keep in mind that the Builder type has advantages if you’re further concatenating the result into a larger bit of output.
  • Basic types and functions: The Text.XmlHtml module exports another 16 simple functions and a few types for manipulating document structure.  They are all pretty obvious and simple; you can check if a node is an element, text node, or comment, get its children, get and set its attributes, and so on.  You can get lists of child and descendant nodes.  All of the basic things you’d expect.
  • Cursor: In the package Text.XmlHtml.Cursor, there are functions for acting on document trees more imperatively using a zipper over document trees.  The zipper type is Cursor, and there are a few dozen supporting functions for moving and expecting the nodes of the tree.
  • renderHtml: The Text.Blaze.Renderer.XmlHtml module contains a renderer from blaze into this package’s document type.  This is a sort of corner case, outside the expected usage, but occasionally helpful for some integration stuff if you do some of your HTML using Heist and other stuff with blaze.

So that’s the new xmlhtml package.  It’s a very simple and nice way to play with document trees; and that’s pretty much it!

January 24, 2011 / cdsmith

My Dream GHCi Session, Take 2

About three or four years ago, I write a blog entry describing my dream GHCi session; basically a wish list of things I wish GHCi did for me.  Well, since today is official program announcement day for Google Summer of Code 2011, I’m revisiting this subject in hopes of roping some hapless college students into doing my bidding inspiring others.

So here, revised and updated, is what I’d love to see next time I start GHCi.

$ ghci MyFile.hs
GHCi, version 9.9.02013010: http://www.haskell.org/ghc/  :? for help
Loading package base ... linking ... done.
[1 of 1] Compiling MyFile              ( MyFile.hs, interpreted )

MyFile.hs:13:5: Not in scope: `callDatabase'

MyFile.hs:112:16:
    No instance for (Fractional Integer)

Partially failed, modules loaded: MyFile
*MyFile> :t foo
Warning: foo depends on callDatabase, which was not found.
Warning: Inferred type may be too general.

foo :: forall a b. (SQL a, SQLData b) => a -> t -> STM [b]

*MyFile> foo (Just 7) (DB $ connectPostgreSQL "dbname=fluffybunnies")

*** Exception: callDatabase: unresolved compile error

*MyFile> foo Nothing NoDB  -- doesn't force value for callDatabase

Just 42

*MyFile> :list 110-114

110:       return [a]
111:
112: bar x = (baz x) / 5
113:
114: superCoolFunction = unsafePerformIO $ do

*MyFile> :t baz
baz :: forall a. a -> Integer
*MyFile> let bar = fromIntegral (baz x) / 5
*MyFile> let callDatabase = undefined :: (SQL a, DBDriver b) => b -> a -> STM TVar
*MyFile> :recomp MyFile
[1 of 1] Compiling MyFile              ( MyFile.hs, interpreted )
Ok, modules loaded: MyFile

*MyFile> :t foo

foo :: forall a b. (SQL a, DBDriver t, SQLData b) => a -> t -> STM [b]

*MyFile> let data MyTree a = Leaf a | Branch (MyTree a) (MyTree a)
*MyFile> instance Monoid (MyTree a) where mappend = Branch
*MyFile> Leaf 6 `mappend` Leaf 7
Branch (Leaf 6) (Leaf 7)

*MyFile> :t 6              -- check type by itself
6 :: Num a => a

*MyFile> :t {{ 6 }} / 5  -- check type in context
6 :: Fractional a => a

MyFile> superCoolFunction
... BOOM!

Notes:

  1. It’s nice that I had to remove some parts of my old list because they’ve since been implemented!  In particular, the :list command was added with the GHCi debugger; GHCi now does multiline blocks with :{ and :}, and one of my requests for a better error message seems to no longer be an issue.  This is nice to see!
  2. The first request is for GHCi to continue doing its best to load a module when something goes wrong.  Instead of punting entirely, it could still put those bits in scope that work correctly, and just report the errors on the bits that don’t work.  This should probably only work for the open module (the one with an asterisk by it in the prompt.)
  3. Going further in this direction, the behavior of the first ‘:t foo’ suggests that GHCi may be able to report guess (possibly incorrect) at piecing together the rest of the file in the event of errors.  Here, callDatabase is not in scope, so type checking and inference can’t possible proceed correctly.  However, type checking and inference can still proceed speculatively, by assuming callDatabase :: forall a. a!  A warning is needed, of course, since the given type will likely be insufficiently specific once callDatabase is brought into scope.
  4. The next two lines record what happens to callDatabase (you know, that symbol that wasn’t in scope).  Basically, it’s treated as a bottom (i.e., undefined) value, so if it’s forced, then you get an exception.  If it’s not forced, you can still use foo.
  5. The :list command now exists for symbols or single lines.  I still think a line range is a reasonable idea.
  6. The next few lines show me interactively fixing the errors in MyFile.hs and using a made-up command “:recompile” to try to rebuild the currently loaded source file, except with  currently defined symbols from the command line added to the top-level scope to replace those from the file where relevant.  With that done, I can now ask for the type of foo, and get the true type, which is less general than the guess from earlier.
  7. Next, I define a data type and an instance on the command line.  I’d like to be able to define classes as well.  These may not even need to be GHCi-specific enhancements to Haskell.  Local instance declarations, for example, are already suggested (with restrictions would be needed to preserve principal types and coherence) by Oleg in the now-famous functional pearl on implicit configurations.  Their use within GHCi is another potential motivating example.
  8. The last bit I threw in is something I’ve found myself wanting far more often than I’d expect: a way to ask GHCi for the type of an expression in context.  So while 6 has type Num a => a as expected, if taken in the given context, it turns out to have the more restricted type Fractional a => a, because of the upcoming division.  I chose {{ and }} as markers in the unverified belief that at least “{{” can never occur in legal Haskell code, so they clearly form a subexpression marker instead of actual code.

Most of these are bigger projects, perhaps, than GSoC gives time for… or at a minimum, would need an applicant already familiar with GHC.  But they sure would be convenient.

January 21, 2011 / cdsmith

A Recap About Cabal and Haskell Libraries

Wow, it turns out I’m not the only person having issues with managing dependencies in Haskell!  There has been a lot of discussion and sharing of ideas and information in a few different places, starting from my original article about “DLL hell” in Haskell three days ago.  I’m going to try to collect all the relevant points together, along with some added reading I’ve done, and organize them into a coherent summary.  I’m sure I’ll inadvertently leave some things out, and if so, I apologize.

Regarding “Blame”

First of all, I want to echo Johan Tibbe, who mentioned on Reddit that this is, in many ways, a sign of good things.  Haskell isn’t running into this problem because something broke; it’s running into this problem because it’s being used for a remarkable variety of projects in a way that hasn’t happened before.  I also agree with John Millikin, Mike Burns, and others who pointed out that the problem isn’t uniquely Haskell.  Indeed, I think it’s fair to say that perhaps Haskell is one of the few environments where we’ve got a prayer at solving the problem.

The causes come down to two things, basically,

  1. Haskell encourages the writing of many small libraries.  This is in part because we do such a good job of managing the dependencies on all those libraries.  Can anyone imagine that we’d have a lot of the stuff we have now on Hackage if we didn’t have excellent tools for working with it?  If there’s any lesson to be learned here, it’s just that people will try to do more things until they hit the limits of the tools available to them!
  2. Haskell is now being used to write “integration” type software; packages that pull together a lot of very different functionality and build something out of the pieces.  I think this is a relatively new phenomenon, at least at the scale it’s happening.  And it puts a lot more stress on systems like Cabal.

So I’d be unhappy if someone walked away from my article thinking “Haskell sucks at dependency management; I should use something else.”  The thing is, something else probably sucks too, quite possibly a lot more!  In many cases, it sucks so much that you wouldn’t even attempt to do the things we routinely do in Haskell.  No one releases a Java library with only 50 lines of code – in part because it’s hard to do anything interesting in 50 lines of Java, but also because the effort of getting it installed and working with all your other libraries would be so great that it would swamp the effort of rewriting the functionality.

Regarding Defeatism

On the other side, several comments were made to the effect that it’s too much to hope that we can solve version dependency problems in Haskell.  The argument goes that there are lots of other languages that also have these same problems; they haven’t found answers, and we probably won’t either.  There’s mention that this is an “active research topic,” implying that it should be left to the researchers.

It’s good to inject some context into the discussion about the scope of the problem, but ultimately I think we should reject the idea that Haskell isn’t going to solve these problems, for three reasons:

  1. We’re almost there! Despite the admittedly negative tone in the article that started this all, I think I’ve actually enumerated most of the issues with the current system, and they all look solvable.  GHC and Cabal developers have put immense amounts of effort into working on these problems, and they have nearly gotten us to a place where Haskell dependencies just work in a way that’s not true in any other language.  (A key point here: Isolation-based answers help tremendously in practice, but still leave possibilities of problems.  In fact, any time something only works because of isolation, it’s also the case that someone trying to combine that code together into a bigger system is going to run into problems.  So any environment that widely recommends an isolation-based answer is clearly short of the “just works” point, and instead settling for “works so far, and we hope no one tries to do something bigger.”)
  2. These are Haskell’s problems to solve. While dependency management comes up in many different programming languages, the solutions in this case are Haskell solutions.  If you look at the central two issues I pointed out – internal dependencies, and the Cabal butterfly effect – what’s ultimately holding up a solution is work on the compiler to contribute things that relate to its understanding of the Haskell programming language and the interfaces between modules that the compiler builds.  If Haskell doesn’t solve these problems, then no one else is going to do it for us.
  3. Since when does the Haskell community shy away from hard problems? Sure, this is a difficult problem.  So are/were lazy evaluation in a general-purpose language, type classes, models for I/O in a pure functional framework, functional dependencies and type families, software transactional memory, vectorization of data parallel code, type inference for GADTs, and the construction of what is almost certainly the most advanced optimizing compiler in the world.  Haskell did (and/or is doing) all of those.

I don’t mean to dismiss those who pointed out this is a hard problem; it may take a while to solve it; so those who are trying to use Haskell in practice right now are well-advised to find temporary workaround or partial answers, such as isolating dependencies of projects, for example.  At the same time, though, part of the unique spirit of Haskell has always been the willingness to live with our problems all the way up to (but not past) our tolerance point, and take the time to find the right answer instead of the expedient one.

That’s always been my interpretation of the Haskell motto to “avoid success at all costs” – what we’re really avoiding is the temptation to take short-cuts with duct-tape and glue, and in the process compromise the effort to find the right answers to questions about Haskell.  This isn’t the fault of the duct tape or the glue, which are useful short-term tools.  But when keeping up with the duct tape and glue gets in the way of making correct decisions, then a programming language starts that deadly race wherein we try to get as popular as we can before the language gets too crufty to use any more, and people jump to something else.

Isolating Environments

Another very informative part of the conversation relates to isolation of different build environments.  I’m not active in the Python or Ruby development communities, but several people (including John Millikin and Mike Burns, mentioned that they routinely solve these kinds of problems with sandbox or isolation tools.  These tools maintain local package databases that are just big enough to build a particular piece of software, thereby guaranteeing that installing some unrelated library for a separate project won’t break your libraries for this one.  Ruby’s tool for this purpose is rvm (Ruby Version Manager), while the Python community uses virtualenv.

It may come as a surprise to many people that Haskell has its own tool for isolated build environments, called cabal-dev.  John Millikin wrote an in-depth introduction on building and using it on Reddit.  Basically, it keeps a private package database for you in a subdirectory of your build directory.  The idea is that you can install a minimal amount of stuff in the system-wide or user-wide databases, and let cabal-dev download and build most dependencies on demand for your specific project and store them locally.  It’s not quite an rvm-level tool, in that it does not manage multiple versions of the compiler, but it sure helps with library version isolation.

As I mentioned above, I see isolation as a short-term good, but perhaps a premature casting off of a hair shirt.  If I can only build all my Haskell stuff because of isolated package databases, then this means there are some integration projects that I could not embark on because they would be too large for the isolated package databases.  So I’m of mixed minds about this; it’s no-doubt good that cabal-dev exists.  On the other hand, I’d hope it does not obscure the need for a right answer to package dependencies.

A few other notes related to isolation:

  • Another idea that was brought up again, and that’s come up in many other places recently, is installing and using a local copy of Hackage for use in a collection of related projects.  Michael Snoyman’s Yackage is a minimal example of this that looks like a piece of cake to install.  It’s also supposed to (eventually?  now?) be relatively easy to install hackage-server and customize the exact set of features you want.  I have yet to do any of this, but it certainly looks appealing, especially if you’re trying to maintain an ecosystem of connected software.
  • Something else that came up with respect to cabal-dev and rvm, for example, is that rvm also isolates the version of the compiler you’re using, as well.  It looks rather difficult, currently, to have multiple versions of the ghc compiler installed at the same time.  Indeed, this is part of what turned me off from doing GHC work some time ago; it looks like it’s more work to keep several GHC versions in working order at once than it is to actually modify the code.  It seems we’re a long way from ‘cabal install ghc-7.1’!
  • Finally, a sort of “partial isolation” that seems unambiguously to be a good thing was mentioned in the context of Ruby’s bundlr by Darrin Thompson.  The comment was that when Ruby’s gem system resolves dependencies, it can be asked to write out the exact resolution to a file, and then other tools on other systems can bring exactly that same package dependency tree into being.  I think to date, the Haskell community has largely avoided struggling with deployment issues and integration systems, but it doesn’t seem difficult to get Cabal and cabal-install to pick up the idea of fixing a specific solution to version constraints, to ensure that packages used on deployed systems exactly match their development counterparts, even if a rebuild is needed (e.g., different processor architecture).  Of course, Ruby has a somewhat greater need for this, in that I can generally copy a compiled and statically linked binary in Haskell; but as the move to shared libraries continues, this may well become far more relevant.

Internal Dependencies

Nothing new here, except that there seems to be a general consensus that this needs to be one of the first changes made to the Haskell build infrastructure.  As Duncan has pointed out before, this involves a coordinated change involving both GHC and Cabal.

Something I find myself in agreement with is that perhaps the best approach going forward would be to fix this, and the next point (the “butterfly effect”), and then take stock again of where we are.  Fixing the internal dependencies issue would hopefully reduce the number of version constraints Cabal needs to deal with by an order of magnitude or so.  That might make many of the other issues people are facing go away, or reduce them to the point that they are solvable by people just talking to each other and politely requesting bumps in version upper bounds.  That seems sensible to me; there’s a legitimate hope that this fix would make everything else a matter of patching up the odd points here and there.

The Butterfly Effect

This was point number 3 in the “DLL Hell” article, but I’ve since written an expanded description of what is happening, and made up a name for it in hopes of making it easier to discuss.  The idea is that, while Cabal and GHC are fine with multiple packages existing having different versions, they are not okay with multiple packages have the same name and version, but different dependencies.  As a result, one can end up in a situation where installing a package breaks another package.  This is the only issue in the list that I consider to be a bug (albeit probably a known and understood one) in Cabal.

A number of people have brought up GHC’s ABI hash… that long sequence of hexadecimal that GHC appends to your package when you rebuild it.  I’ve spent some time doing a bit of reading into what GHC does here.  While it’s certainly related, unfortunately this still doesn’t actually solve the problem.  What it does do is help GHC to detect the problem.  The idea is that GHC hashes together all the information about the ABI – that is, all the information that needs to be known to correctly link against a package.  Then if some package gets recompiled and exposes a different ABI, the hask will differ, and GHC will notice that packages that depend on it are broken.

This raises the question of whether GHC could just keep around multiple copies of the same library, differing only in their ABI hash.  The answer, as Simon Marlow pointed out, is no.  Because the ABI hash is not included in the names of symbols in a library, trying to link two different packages with the same name and version but different ABI hashes would lead to problems later on.  So currently, the ABI hash is used to detect when a dependency is recompiled, but it cannot be used to keep several instances of the same package version.  The reason for not including the ABI hash in the symbol name seems to be related to avoiding unnecessarily recompiling things that don’t need to be recompiled.  That’s also a valid goal; so something a bit more complex would have to happen to get this sort of thing working.  Still, it doesn’t look undoable.

Several people mentioned the Linux package manager Nix as inspiration here.  It does look very much like what ought to be done.  Whether we would want deferred garbage collection or shared –user installed packages is an interesting question, but I think far less important than solving the immediate problems.

About the Package Versioning Policy (PVP)

One of the surprises for me was the response to my comments about the PVP (the Package Versioning Policy).  This comes back to different people having different kinds of projects, I suppose.  I personally have never witnessed a package that used to build breaking because of upgrades elsewhere and someone failing to put upper bounds on their package dependencies.  Don’t get me wrong; I’ve seen a few Cabal build failures in my time, but generally they’ve always been traced to some other problem; I’ve just never seen it be the case that the package would have been fine with an appropriate upper bound, but failed to compile because there wasn’t.  There’s always been something else involved; usually a compiler version difference and resulting changes in some package for which an older version doesn’t exist for the new compiler.

Apparently other people consider this a significant problem, though, and if others are having problems even today with the PVP not being followed tightly enough, then I certainly retract my suggestion that we consider weakening it.  Suggestions were made to have Hackage enforce the PVP, but my personal feelings always come back to what I think we ought to consider an axiom of Hackage: anything we do that makes it less likely people would upload their packages is a step backward, not forward.  The fact that practically all open-source Haskell code out there is contained in Hackage is an immense treasure of the Haskell community, and we’d be fools to jeopardize that in any way.  Having Hackage enforce the PVP means requiring that a package be buildable in the Hackage environment before accepting it, and that seems like a non-starter.

One question I’d like to keep on the table is the possibility of telling Cabal to distinguish between strong bounds (“I know this won’t work”) and weak bounds (“I haven’t tested this, possibly because it doesn’t exist yet to test“).  Perhaps new version bound operators (>>) and (<<) could be introduced to capture the strong bounds.  Cabal could then be told on a case-by-case basis to override the weak version bounds on other people’s packages.  Then one might imagine an interaction something like:

$ cabal install foo
Configuring foo...
Cannot resolve dependencies for foo (... for some reason involving upper bound on bar ...)
$ cabal relax-depends bar 'baz < 0.5'
$ cabal install foo
(successful build)

It’s also worth mentioning, here, Michael Snoymans packdeps package and its web front end.  These are tools for alerting package authors when they are excluding other libraries because of upper bounds on their packages.  This can help reduce the problem of keeping package dependencies up to date.

Interactions With OS Packaging

Finally, there were a few comments about using the operating system package manager instead of trying to “reinvent the wheel” with Cabal.  All things considered, this doesn’t look like a reasonable idea.  The amount of interconnection between Cabal and GHC, mentioned in several places earlier, is good proof that package management is somewhat intimately connected to the build tools of the language we’re doing it in.  Add to this the fact that there are nearly 3000 different packages on Hackage (never mind all the different versions, where some old versions are still needed!), and the fact that several of them are updated several times per day.  Packaging libraries for distribution with the operating system is a completely different model.

However, this brings up the question of what to do about OS-packaged Haskell libraries.  Personally, what I do is just let the operating system manage my global package database, and manage my own user package database.  Then if the operating system packaged libraries are updated, I may even just have to blow away and reinstall all of my user packages, but it’s infrequent enough to not be an issue.  Maybe there’s something theoretically better we could do here, but I don’t see it as a serious issue.

January 17, 2011 / cdsmith

The Butterfly Effect in Cabal

This is an elaboration on a point from my previous article, and an ensuing reddit comment.

Twitter has a unique language all its own, and it would be nice to be able to understand and do something cool with all those twitter tags… you know, @cdsmithus, #haskell, etc.  The first step is to parse them from a block of text.  So I hypothetically might decide to write a very simple Haskell package called “twittertags” to do that.  Since I’d like my work to be extensible by others, I’ll export my work as parser combinators using parsec.  Then other people can use my code for the oh-so-difficult task of recognizing special punctuation as tags on Twitter.

Now, I’m well aware that while the current version of Parsec is 3.1, quite a few people are still using 2.1 because of performance concerns (or just lack of time to update their code).  Fortunately, if I import the compatible module names, I can be careful and make my code work with any version of parsec you like.

Of course, now that I’ve done the hard work of recognizing punctuation, people come along to use my library, building various Twitter and social media applications on top of this package of mine.  In particular, let’s consider two such packages called “twitclient” and “superblog”.  The both expose their own libraries, too, for extensibility.  They want to use my parser combinators in their own, so they also depend on Parsec, but neither of these folks is going to test against two different Parsec versions!  The author of “twitclient” decides to go with parsec 2.1, because of a measurable performance hit with the newer version.  But the author of “superblog” is all for the latest versions, and depends on 3.1.  My package works with both, so there’s no problem… right?

Wrong.

The dependencies now look like this…

Figure: The Cabal Butterfly Effect

Cabal allows several different versions of the same package to be installed at once, so there’s no problem with having both parsec versions installed at once.  But the question is how my own library should be built.  Should it be built against parsec 2.1?  Or against parsec 3.1?  The answer is both.  We need versions of twittertags to built against both of the two dependencies, or else one of the two packages that depends on it will fail.  But Cabal currently can’t do this.

What is does is certainly… suboptimal.  When you build twitclient, it will recompile twittertags against parsec-2.1, which will break superblog.  If you then reinstall superblog to fix it, Cabal will recompile twittertags against parsec-3.1, and break twitclient… and so on, ad infinitum.  What’s worse, it will break these packages without even telling you that it is doing so!

That’s what I’m now dubbing the “Cabal Butterfly Effect”, and one of the issues I brought up in the earlier post.

January 16, 2011 / cdsmith

Haskell’s Own DLL Hell

I touched on this issue in a more positive way in this recent entry.  But now I’m going to be more negative about it.  You see, here’s the thing: Significant Haskell software projects are struggling under the weight of the Haskell equivalent of “DLL hell”.

If you’re not familiar with the term, here’s a definition of “DLL hell”, a concept painfully familiar to many Windows system administrators:

“In computing, DLL hell is a colloquial term for the complications that arise when working with dynamic link libraries (DLLs) used with Microsoft Windows operating systems.”

The idea is that various applications on the computer share libraries.  These libraries have different versions, and different programs often need different versions.  The “hell” starts when some programs overwrite the libraries with other, incompatible, versions, or when one program somehow turns out to need both of two incompatible sets of libraries.

To be sure, Haskell is better equipped to handle the problem than historical Windows executables.  In old versions of Windows, programs often blindly copied the DLLs they needed into a system-wide location (Windows\System) without regard to any versioning at all.  However, in Haskell, we are dealing with the problem on a different order of magnitude.  Whereas a DLL on Windows is generally a pretty substantial project in its own right, many Haskell package on Hackage consist of just a few lines of code (put in a positive light, they do one thing, and do it well!), and as a result, many other projects depend on dozens of different packages, either directly or indirectly.

This has consequences: my experience is that it’s currently near-impossible to embark on most nontrivial Haskell software projects without spending a substantial percentage of one’s time fighting dependency version issues.  This is especially true of “real world” sorts of projects: those that often involve pulling together a lot of different functionality, rather than solving specific, well-defined computational problems.

That’s where we are.  The question is what we do about it.  I’d like to propose some questions for discussion:

1. Is it a good idea to follow the Package Versioning Policy?  Should the PVP be modified?

This one is certainly going to be controversial.  For background, the PVP is a set of guidelines for things like specifying the dependencies of a Haskell package, and how to manage your own package’s version number.  The short version is that packages shuld bump at least the minor version number (the x in version 1.x) every time they make a potentially breaking change, such as whenever any entity is removed or renamed or their types are changed.  Furthermore, the PVP suggests that dependencies should have have upper bounds on their versions. The goal here is that if you make a change that might break someone else’s package, you should create a new version and their package will continue to build against the old version.

There are two possible effects of following the PVP by adding upper bounds on dependencies:

  • Someone might try to install some package, and because of an upper bound, Cabal builds it against an older version of some library.  This causes the build to succeed, where it otherwise would have failed because you removed or renamed something.
  • Someone might try to install some package, and because of an upper bound, Cabal fails to find the right combination of dependencies, and refuses to build it at all.

Just to be argumentative, I’ll mention that it’s pretty clear to me from personal experience that #2 happens a lot more often than #1.  People following the package versioning policy by specifying upper bounds is far more likely to prevent ‘cabal install’ from succeeding, than to allow it to succeed.  Upper bounds, on balance, make it harder to get Haskell libraries installed successfully.  When (again, from personal experience) attempts to build any nontrivial Haskell application have a less than 30% chance or succeeding anyway, should we be all that worried about the theoretical chance that a build might fail?

That’s just one side of the story, though.  It’s true that an error due to failed dependencies makes it clearer what is going on than a random failure involving an unresolved symbol or type mismatch during a compile.  So this is an open question in my mind.

Perhaps the less contentious way to ask the question would be this: should Cabal be modified to give a warning instead of an error for upper bounds when they would prevent the package from building at all?  (And if so, perhaps it should get a new strong upper bound, which indicates someone actually knows that the build fails.)

2. How close are we to the goal of getting GHC and Cabal to tell the difference between exported and non-exported dependencies?

It would be one thing if the problem here were actual incompatibilities in code.  If I’m using libraries that rely on different versions of the same package, and they both export things that rely on types or instances from that package, then I should expect the build to fail.  But a lot of the time (I’d guess a majority of the time!) that’s not the case.  One place this comes up a lot is with network‘s dependency on parsec.  But it doesn’t actually export any parsers; its use of parsec is an implementation detail.

Similar issues arise in many other situations.  Many library dependencies are a matter of implementation, not public interface.  Even where it’s not currently the case, if this is fixed, it will change the community’s best practice to include using a lot more newtype wrappers rather than re-exporting other package’s types, or splitting packages if they provide substantial functionality that does not need the re-exports.

I mentioned earlier that Haskell deals with this problem on a whole different scale than other languages: part of the reason is this lack of distinction between implementation detail and exposed interfaces.

3. Can we stop cabal-install from breaking the package database?

A very special case of this problem happens in a particularly disturbing way.  It goes like this:

  • Package foo depends on bar-0.5 and baz-1.2.
  • Package flox depends on bar-0.5 and baz-1.1.
  • Package bar-0.5 depends on baz, but has no preference between versions 1.1 and 1.2.

The way this works now is as follows: When I cabal install foo, Cabal first builds baz-1.2, and then bar-0.5, and then foo.  But if I later cabal install flox, then Cabal will build baz-1.1 (this is fine, since multiple package versions can exist at once), then it will rebuild bar-0.5, linking against baz-1.1.  (This does not coexist; because bar has the same version number, it gets overwritten.).  At this point, foo is broken.  Running ghc-pkg check will complain about it being broken because of a missing dependency.

I’m not sure what the right thing to do is here; I suppose that if bar-0.5 re-exports types from baz, then its “version” needs to include the version information from baz somewhere.  In any case, this is an extremely confusing, and extremely common, issue to run into, and it results in an inconsistent package database without so much as a warning.  Something really needs to be done.

4. What is the best way to deal with this in the interim?

Yackage is a great idea.  (Or any other way to maintain a local Hackage; I’m aware of discussion about whether it might be better to just use the new hackage server code eventually, and I don’t think the implementation particularly matters.)  Michael Snoyman’s goal was really more about maintaining collections of packages that he’s maintaining… but for a real-world software project that otherwise won’t build, it sounds like a great way to keep track of local modifications to other people’s packages.

Another idea that might work really well is to just be able to ask cabal-install to remember a modification to various packages’ build-depends’ fields persistently.  So instead of having to download, build, and manually install these packages just to change their package.cabal files, cabal-install would continue updating from Hackage, but reconcile your existing build-depends requests (“relax fizbuzz’s build-depends to build with foobar-0.5”) automatically.  Even better, make it easy to get a list of which of these local changes are still at odds with public packages, to report to either the maintainer.

All of these are options for mitigating the problem.  But first, I think we need to realize that this is a serious problem.  I’m afraid there’s a bit of sampling bias here; I have to believe that these problems aren’t getting solved because many established Haskellers tend to work on projects with very narrowly tailored scope… and this is true because many people who want to work on more general (“real world” by my definition above) projects have often fled to languages that don’t make it a week-long job to get the dependencies for a project to all build at once.

January 9, 2011 / cdsmith

An Old Article I Wrote

I was asked by someone to put this old piece of writing of mine somewhere more permanent, so here it is.  A few comments off the top:

  • This isn’t new.  I wrote it years ago.
  • Yes, I’m a bit embarrassed at some of the wording, as most people are when they read content they wrote a long time ago.  There are things that I’d say differently if I wrote something like this today.  There is clumsy wording, and there are poor choices of examples.  I’m not taking this opportunity to revise the writing; this is exactly as I wrote it all those years ago.
  • If pressed for an answer, though, yes I still do believe in the central conclusions of the article.  Namely:
    • That “static typing” and “dynamic typing” are two concepts that are fundamentally unrelated to each other, and just happen to share a word.
    • That “static types” are, at their core a tool for writing and maintaining computer-checked proofs about code
    • That “dynamic types” are, at their core, there to make unit testing less tedious, and are a tool for finding bugs.
    • That the two are related in the way I outline: that one establishes lower bounds on correctness of code, while the other establishes upper bounds, and that questions about their real world use should come down to the possibility and effectiveness of addressing certain kinds of bugs by either computer-checked proof, or testing.

With that said, here is the original article:


What To Know Before Debating Type Systems

I would be willing to place a bet that most computer programmers have, on multiple occasions, expressed an opinion about the desirability of certain kinds of type systems in programming languages. Contrary to popular conception, that’s a great thing! Programmers who care about their tools are the same programmers who care about their work, so I hope the debate rages on.

There are a few common misconceptions, though, that confuse these discussions. This article runs through those I’ve encountered that obscure the most important parts of the debate. My goal is to build on a shared understanding of some of the basic issues, and help people get to the interesting parts more quickly.

Classifying Type Systems

Type systems are commonly classified by several words, of which the most common are “static,” “dynamic,” “strong,” and “weak.” In this section, I address the more common kinds of classification. Some are useful, and some are not.

Strong and Weak Typing

Probably the most common way type systems are classified is “strong” or “weak.” This is unfortunate, since these words have nearly no meaning at all. It is, to a limited extent, possible to compare two languages with very similar type systems, and designate one as having the stronger of those two systems. Beyond that, the words mean nothing at all.

Therefore: I give the following general definitions for strong and weak typing, at least when used as absolutes:

  • Strong typing: A type system that I like and feel comfortable with
  • Weak typing: A type system that worries me, or makes me feel uncomfortable

What about when the phrase is used in a more limited sense? Then strong typing, depending on the speaker or author, may mean anything on the spectrum from “static” to “sound,” both of which are defined below.

Static and Dynamic Types

This is very nearly the only common classification of type systems that has real meaning. As a matter of fact, it’s significance is frequently under-estimated. I realize that may sound ridiculous; but this theme will recur throughout this article. Dynamic and static type systems are two completely different things, whose goals happen to partially overlap.

A static type system is a mechanism by which a compiler examines source code and assigns labels (called “types”) to pieces of the syntax, and then uses them to infer something about the program’s behavior. A dynamic type system is a mechanism by which a compiler generates code to keep track of the sort of data (coincidentally, also called its “type”) used by the program. The use of the same word “type” in each of these two systems is, of course, not really entirely coincidental; yet it is best understood as having a sort of weak historical significance. Great confusion results from trying to find a world view in which “type” really means the same thing in both systems. It doesn’t. The better way to approach the issue is to recognize that:

  • Much of the time, programmers are trying to solve the same problem with static and dynamic types.
  • Nevertheless, static types are not limited to problems solved by dynamic types.
  • Nor are dynamic types limited to problems that can be solved with static types.
  • At their core, these two techniques are not the same thing at all.

Observing the second of these four simple facts is a popular pass-time in some circles. Consider this set of presentation notes, with a rather complicated “the type system found my infinite loop” comment. From a theoretical perspective, preventing infinite loops is in a very deep sense the most basic possible thing you can do with static types! The simply-typed lambda calculus, on which all other type systems are based, proves that programs terminate in a finite amount of time. Indeed, the more interesting question is how to usefully extend the type system to be able to describe programs that don’t terminate! Finding infinite loops, though, is not in the class of things most people associate with “types,” so it’s surprising. It is, indeed, provably impossible with dynamic types (that’s called the halting problem; you’ve probably heard of it!). But it’s nothing special for static types. Why? Because they are an entirely different thing from dynamic types.

The dichotomy between static and dynamic types is somewhat misleading. Most languages, even when they claim to be dynamically typed, have some static typing features. As far as I’m aware, all languages have some dynamic typing features. However, most languages can be characterized as choosing one or the other. Why? Because of the first of the four facts listed above: many of the problems solved by these features overlap, so building in strong versions of both provides little benefit, and significant cost.

Other Distinctions

There are many other ways to classify type systems. These are less common, but here are some of the more interesting ones:

  • Sound types. A sound type system is one that provides some kind of guarantee. It is a well-defined concept relating to static type systems, and has proof techniques and all those bells and whistles. Many modern type systems are sound; but older languages like C often do not have sound type systems by design; their type systems are just designed to give warnings for common errors. The concept of a sound type system can be imperfectly generalized to dynamic type systems as well, but the exact definition there may vary with usage.
  • Explicit/Implicit Types. When these terms are used, they refer to the extent to which a compiler will reason about the static types of parts of a program. All programming languages have some form of reasoning about types. Some have more than others. ML and Haskell have implicit types, in that no (or very few, depending on the language and extensions in use) type declarations are needed. Java and Ada have very explicit types, and one is constantly declaring the types of things. All of the above have (relatively, compared to C and C++, for example) strong static type systems.
  • The Lambda Cube. Various distinctions between static type systems are summarized with an abstraction called the “lambda cube.” Its definition is beyond the scope of this article, but it basically looks at whether the system provides certain features: parametric types, dependent types, or type operators. Look here for more information.
  • Structural/Nominal Types. This distinction is generally applied to static types with subtyping. Structural typing means a type is assumed whenever it is possible to validly assume it. For example, a record with fields called x, y, and z might be automatically considered a subtype of one with fields x and y. With nominal typing, there would be no such assumed relationship unless it were declared somewhere.
  • Duck Typing. This is a word that’s become popular recently. It refers to the dynamic type analogue of structural typing. It means that rather than checking a tag to see whether a value has the correct general type to be used in some way, the runtime system merely checks that it supports all of the operations performed on it. Those operations may be implemented differently by different types.

This is but a small sample, but this section is too long already.

Fallacies About Static and Dynamic Types

Many programmers approach the question of whether they prefer static or dynamic types by comparing some languages they know that use both techniques. This is a reasonable approach to most questions of preference. The problem, in this case, is that most programmers have limited experience, and haven’t tried a lot of languages. For context, here, six or seven doesn’t count as “a lot.” On top of that, it requires more than a cursory glance to really see the benefit of these two very different styles of programming. Two interesting consequences of this are:

  • Many programmers have used very poor statically typed languages.
  • Many programmers have used dynamically typed languages very poorly.

This section, then, brings up some of the consequences of this limited experience: things many people assume about static or dynamic typing that just ain’t so.

Fallacy: Static types imply type declarations

The thing most obvious about the type systems of Java, C, C++, Pascal, and many other widely-used “industry” languages is not that they are statically typed, but that they are explicitly typed. In other words, they require lots of type declarations. (In the world of less explicitly typed languages, where these declarations are optional, they are often called “type annotations” instead. You may find me using that word.) This gets on a lot of people’s nerves, and programmers often turn away from statically typed languages for this reason.

This has nothing to do with static types. The first statically typed languages were explicitly typed by necessity. However, type inference algorithms – techniques for looking at source code with no type declarations at all, and deciding what the types of its variables are – have existed for many years now. The ML language, which uses it, is among the older languages around today. Haskell, which improves on it, is now about 15 years old. Even C# is now adopting the idea, which will raise a lot of eyebrows (and undoubtedly give rise to claims of its being “weakly typed” — see definition above). If one does not like type declarations, one is better off describing that accurately as not liking explicit types, rather than static types.

(This is not to say that type declarations are always bad; but in my experience, there are few situations in which I’ve wished to see them required. Type inference is generally a big win.)

Fallacy: Dynamically typed languages are weakly typed

The statement made at the beginning of this thread was that many programmers have used dynamically typed languages poorly. In particular, a lot of programmers coming from C often treat dynamically typed languages in a manner similar to what made sense for C prior to ANSI function prototypes. Specifically, this means adding lots of comments, long variable names, and so forth to obssessively track the “type” information of variables and functions.

Doing this prevents a programmer from realizing the benefits of dynamic typing. It’s like buying a new car, but refusing to drive any faster than a bicycle. The car is horrible; you can’t get up the mountain trails, and it requires gasoline on top of everything else. Indeed, a car is a pretty lousy excuse for a bicycle! Similarly, dynamically typed languages are pretty lousy excuses for statically typed languages.

The trick is to compare dynamically typed languages when used in ways that fit in with their design and goals. Dynamically typed languages have all sorts of mechanisms to fail immediately and clearly if there is a runtime error, with diagnostics that show you exactly how it happened. If you program with the same level of paranoia appropriate to C – where a simple bug may cause a day of debugging – you will find that it’s tough, and you won’t be actually using your tools.

(As a side comment, and certainly a more controversial one, the converse is equally true; it doesn’t make sense to do the same kinds of exhaustive unit testing in Haskell as you’d do in Ruby or Smalltalk. It’s a waste of time. It’s interesting to note that the whole TDD movement comes from people who are working in dynamically typed languages… I’m not saying that unit testing is a bad idea with static types; only that it’s entirely appropriate to scale it back a little.)

Fallacy: Static types imply upfront design or waterfall methods

Some statically typed languages are also designed to enforce someone’s idea of a good development process. Specifically, they often require or encourage that you specify the whole interface to something in one place, and then go write the code. This can be annoying if one is writing code that evolves over time or trying out ideas. It sometimes means changing things in several different places in order to make one tweak. The worst form of this I’m aware of (though done mainly for pragmatic reasons rather than ideological ones) is C and C++ header files. Pascal has similar aims, and requires that all variables for a procedure or function be declared in one section at the top. Though few other languages enforce this separation in quite the same way or make it so hard to avoid, many do encourage it.

It is absolutely true that these language restrictions can get in the way of software development practices that are rapidly gaining acceptance, including agile methodologies. It’s also true that they have nothing to do with static typing. There is nothing in the core ideas of static type systems that has anything to do with separating interface from implementation, declaring all variables in advance, or any of these other organizational restrictions. They are sometimes carry-overs from times when it was considered normal for programmers to cater to the needs of their compilers. They are sometimes ideologically based decisions. They are not static types.

If one doesn’t want a language deciding how they should go about designing their code, it would be clearer to say so. Expressing this as a dislike for static typing confuses the issue.

This fallacy is often stated in different terms: “I like to do exploratory programming” is the popular phrase. The idea is that since everyone knows statically typed languages make you do everything up front, they aren’t as good for trying out some code and seeing what it’s like. Common tools for exploratory programming include the REPL (read-eval-print loop), which is basically an interpreter that accepts statements in the language a line at a time, evaluates them, and tells you the result. These tools are quite useful, and they exist for many languages, both statically and dynamically typed. They don’t exist (or at least are not widely used) for Java, C, or C++, which perpetuates the unfortunate myth that they only work in dynamically typed languages. There may be advantages for dynamic typing in exploratory programming (in fact, there certainly are some advantages, anyway), but it’s up to someone to explain what they are, rather than just to imply the lack of appropriate tools or language organization.

Fallacy: Dynamically typed languages provide no way to find bugs

A common argument leveled at dynamically typed languages is that failures will occur for the customer, rather than the developer. The problem with this argument is that it very rarely occurs in reality, so it’s not very convincing. Programs written in dynamically typed languages don’t have far higher defect rates than programs written in languages like C++ and Java.

One can debate the reasons for this, and there are good arguments to be had there. One reason is that the average skill level of programmers who know Ruby is higher than those who know Java, for example. One reason is that C++ and Java have relatively poor static type systems. Another reason, though, is testing. As mentioned in the aside above, the whole unit testing movement basically came out of dynamically typed languages. It has some definite disadvantages over the guarantees provided by static types, but it also has some advantages; static type systems can’t check nearly as many properties of code as testing can. Ignoring this fact when talking to someone who really knows Ruby will basically get you ignored in turn.

Fallacy: Static types imply longer code

This fallacy is closely associated with the one above about type declarations. Type declarations are the reason many people associated static types with a lot of code. However, there’s another side to this. Static types often allow one to write much more concise code!

This may seem like a surprising claim, but there’s a good reason. Types carry information, and that information can be used to resolve things later on and prevent programmers from needing to write duplicate code. This doesn’t show up often in simple examples, but a really excellent case is found in the Haskell standard library’s Data.Map module. This module implements a balanced binary search tree, and it contains a function whose type signature looks like this:

lookup :: (Monad m, Ord k) => k -> Map k a -> m a

This is a magical function. It says that I can look something up in a Map and get back the result. Simple enough, but here’s the trick: what do I do if the result isn’t there? Common answers might include returning a special “nothing” value, or aborting the current computation and going to an error handler, or even terminating the whole program. The function above does any of the above! Here’s how I compare the result against a special nothing value:

case (lookup bobBarker employees) of
    Nothing     -> hire bobBarker
    Just salary -> pay bobBarker salary

How does Haskell know that I want to choose the option of getting back Nothing when the value doesn’t exist, rather than raising some other kind of error? It’s because I wrote code afterward to compare the result againstNothing! If I had written code that didn’t immediately handle the problem but was called from somewhere that handled errors three levels up the stack, then lookup would have failed that way instead, and I’d be able to write seven or eight consecutive lookup statements and compute something with the results without having to check for Nothing all the time. This completely dodges the very serious “exception versus return value” debate in handling failures in many other languages. This debate has no answer. Return values are great if you want to check them now; exceptions are great if you want to handle them several levels up. This code simply goes along with whatever you write the code to do.

The details of this example are specific to Haskell, but similar examples can be constructed in many statically typed languages. There is no evidence that code in ML or Haskell is any longer than equivalent code in Python or Ruby. This is a good thing to remember before stating, as if it were obviously true, that statically typed languages require more code. It’s not obvious, and I doubt if it’s true.

Benefits of Static Types

My experience is that the biggest problems in the static/dynamic typing debate occur in failing to understand the issues and potential of static types. The next two sections, then, are devoted to explaining this position in detail. This section works upward from the pragmatic perspective, while the next develops it into its full form.

There are a number of commonly cited advantages for static typing. I am going to list them in order from least to most significant. (This helps the general structure of working up to the important stuff.)

Performance

Performance is the gigantic red herring of all type system debates. The knowledge of the compiler in a statically typed language can be used in a number of ways, and improving performance is one of them. It’s one of the least important, though, and one of the least interesting.

For most computing environments, performance is the problem of two decades ago. Last decade’s problem was already different, and this decades problems are at least 20 years advanced beyond performance being the main driver of technology decisions. We have new problems, and performance is not the place to waste time.

(On the other hand, there are a few environments where performance still matters. Languages in use there are rarely dynamically typed, but I’m not interested enough in them to care much. If you do, maybe this is your corner of the type system debate.)

Documentation

If, indeed, performance is irrelevant, what does one look to next? One answer is documentation. Documentation is an important aspect of software, and static typing can help.

Why? Because documentation isn’t just about comments. It’s about everything that helps people understand software. Static type systems build ideas that help explain a system and what it does. The capture information about the inputs and outputs of various functions and modules. This is exactly the set of information needed in documentation. Clearly, if all of this information is written in comments, there is a pretty good chance it will eventually become out of date. If this information is written in identifier names, it will be nearly impossible to fit it all in. It turns out that type information is a very nice place to keep this information.

That’s the boring view. As everyone knows, though, it’s better to have self- documenting code than code that needs a lot of comments (even if it has them!). Conveniently enough, most languages with interesting static type systems have type inference, which is directly analogous to self-documenting code. Information about the correct way to use a piece of code is extracted from the code itself (i.e., it’s self-documenting), but then verified and presented in a convenient format. It’s documentation that doesn’t need to be maintained or even written, but is available on demand even without reading the source code.

Tools and Analysis

Things get way more interesting than documentation, though. Documentation is writing for human beings, who are actually pretty good at understanding code anyway. It’s great that the static type system can help, but it doesn’t do anything fundamentally new.

Fundamentally new things happen when type systems help computer programs to understand code. Perhaps I need to explain myself here. After all, a wise man (Martin Fowler, IIRC) one said:

“Any fool can write code that a computer can understand. Good programmers write code that humans can understand.”I don’t disagree with Martin Fowler, but we have different definitions of understand in mind. Getting a computer to follow code step by step is easy. Getting a computer to analyze it and answer more complex questions about it is a different thing entirely, and it is very hard.

We often want our development tools to understand code. This is a big deal. I’ll turn back to Martin Fowler, who points this out as well.

Correctness

Ultimately, though, the justification for static typing has to come back to writing correct code. Correctness, of course, is just the program doing “what you want.”

This is a really tough problem; perhaps the toughest of all. The theory of computation has a result called Rice’s Theorem, which essentially says this: Given an arbitrary program written in a general purpose programming language, it is impossible to write a computer program that determines anything about the program’s output. If I’m teaching an intro to programming class and assign my students to write “hello world”, I can’t program a grader to determine if they did so or not. There will be some programs for which the answer is easy; if the program never makes any I/O calls, then the answer is no. If the program consists of a single print statement, it’s easy to check if the answer is yes. However, there will be some complicated programs for which my grader can never figure out the answer. (A minor but important technical detail: one can’t run the program and wait for it to finish, because the program might never finish!) This is true of any statement about programs, including some more interesting ones like “does this program ever finish?” or “does this program violate my security rules?”

Given that we can’t actually check the correctness of a program, there are two approaches that help us make approximations:

  • Testing: establishes upper bounds on correctness
  • Proof: establishes lower bounds on correctness

Of course, we care far more about lower bounds than upper bounds. The problem with proofs, though, is the same as the problem with documentation. Proving correctness is easy only somewhat insanely difficult when you have a static body of code to prove things about. When the code is being maintained by three programmers and changing seven times per day, maintaining the correctness proofs falls behind. Static typing here plays exactly the same role as it does with documentation. If (and this is a big if) you can get your proofs of correctness to follow a certain form that can be reproduced by machine, the computer itself can be the prover, and let you know if the change you just made breaks the proof of correctness. The “certain form” is called structural induction (over the syntax of the code), and the prover is called a type checker.

An important point here is that static typing does not preclude proving correctness in the traditional way, nor testing the program. It is a technique to handle those cases in which testing might be guaranteed to succeed so they don’t need testing; and similarly, to provide a basis from which the effort of manual proof can be saved for those truly challenging areas in which it is necessary.

Dynamic Typing Returns

Certainly dynamic typing has answers to this. Dynamically typed languages can sometimes perform rather well (see Dylan), sometimes have great tools (see Smalltalk), and I’m sure they occasionally have good documentation as well, though the hunt for an example is too much for me right now. These are not knock-down arguments for static typing, but they are worth being aware of.

The correctness case is particularly enlightening. Just as static types strengthened our proofs of correctness by making them easier and automatic, dynamic typing improves testing by making it easier and more effective. It simply makes the code fail more spectacularly. I find it amusing when novice programmers believe their main job is preventing programs from crashing. I imagine this spectacular failure argument wouldn’t be so appealing to such a programmer. More experienced programmers realize that correct code is great, code that crashes could use improvement, but incorrect code that doesn’t crash is a horrible nightmare.

It is through testing, then, that dynamically typed languages establish correctness. Recall that testing establishes only upper bounds on correctness. (Dijkstra said it best: “Program testing can be used to show the presence of bugs, but never to show their absence.”) The hope is that if one tries hard enough and still fails to show the presence of bugs, then their absence becomes more likely. If one can’t seem to prove any better upper bound, then perhaps the correctness really is 100%. Indeed, there is probably at some correlation in that direction.

What is a Type?

This is as good a point as any to step back and ask the fundamental question: what is a type? I’ve already mentioned that I think there are two answers. One answer is for static types, and the other is for dynamic types. I am considering the question for static types.

It is dangerous to answer this question too quickly. It is dangerous because we risk excluding some things as types, and missing their “type” nature because we never look for it. Indeed, the definition of a type that I will eventually give is extremely broad.

Problems with Common Definitions

One common saying, quoted often in an attempt to reconcile static and dynamic typing, goes something like this: Statically typed languages assign types to variables, while dynamically typed languages assign types to values. Of course, this doesn’t actually define types, but it is already clearly and obviously wrong. One could fix it, to some extent, by saying “statically typed languages assign types to expressions, …” Even so, the implication that these types are fundamentally the same thing as the dynamic version is quite misleading.

What is a type, then? When a typical programmer is asked that question, they may have several answers. Perhaps a type is just a set of possible values. Perhaps it is a set of operations (a very structural-type-ish view, to be sure). There could be arguments in favor of each of these. One might make a list: integers, real numbers, dates, times, and strings, and so on. Ultimately, though, the problem is that these are all symptoms rather than definitions. Why is a type a set of values? It’s because one of the things we want to prove about our program is that it doesn’t calculate the square roots of a string. Why is a type a set of operations? It’s because one of the things we want to know is whether our program attempts to perform an impossible operation.

Let’s take a look at another thing we often want to know: does our web application stick data from the client into SQL queries without escaping special characters first? If this is what we want to know, then these becomes types. This article by Tom Moertel builds this on top of Haskell’s type system. So far, it looks like a valid definition of “type” is as follows: something we want to know.

A Type System

Clearly that’s not a satisfactory definition of a type. There are plenty of things we want to know that types can’t tell us. We want to know whether our program is correct, but I already said that types provide conservative lower bounds on correctness, and don’t eliminate the need for testing or manual proof. What makes a type a type, then? The other missing component is that a type is part of a type system.

Benjamin Pierce’s book Types and Programming Languages is far ans away the best place to read up on the nitty gritty details of static type systems, at least if you are academically inclined. I’ll quote his definition.

A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.This is a complex definition, but the key ideas are as follows:

  • syntactic method .. by classifying phrases: A type system is necessarily tied to the syntax of the language. It is a set of rules for working bottom up from small to large phrases of the language until you reach the result.
  • proving the absence of certain program behaviors: This is the goal. There is no list of “certain” behaviors, though. The word just means that for any specific type system, there will be a list of things that it proves. What it proves is left wide open. (Later on in the text: “… each type system comes with a definition of the behaviors it aims to prevent.”)
  • tractable: This just means that the type system finishes in a reasonable period of time. Without wanting to put words in anyone’s mouth, I think it’s safe to say most people would agree that it’s a mistake to include this in the definition of a type system. Some languages even have undecidable type systems. Nevertheless, it is certainly a common goal; one doesn’t expect the compiler to take two years to type-check a program, even if the program will run for two years.

The remainder of the definition is mainly unimportant. The “kinds of values they compute” is basically meaningless unless we know what kinds we might choose from, and the answer is any kind at all.

An example looks something like that. Given the expression 5 + 3, a type checker may look at 5 and infer that it’s an integer. It may look at 3 and infer it’s an integer. It may then look at the + operator, and know that when + is applied to two integers, the result is an integer. Thus it’s proven the absence of program behaviors (such as adding an integer to a string) by working up from the basic elements of program syntax.

Examples of Unusual Type Systems

That was a pretty boring example, and one that plays right into a trap: thinking of “type” as meaning the same thing it does in a dynamic type system. Here are some more interesting problems being solved with static types.

  • http://wiki.di.uminho.pt/twiki/pub/Personal/Xana/WebHome/report.pdf. Uses types to ensure that the correct kinds of data are gotten out of a relational database. Via the type system, the compiler ends up understanding how to work with concepts like functional dependencies and normal forms, and can statically prove levels of normalization.
  • http://www.cs.bu.edu/~hwxi/academic/papers/pldi98.pdf. Uses an extension to ML’s type system to prove that arrays are never accessed out of bounds. This is an unusually hard problem to solve without making the languages that solve it unusable, but it’s a popular one to work on.
  • http://www.cis.upenn.edu/~stevez/papers/LZ06a.pdf. This is great. This example uses Haskell’s type system to let someone define a security policy for a Haskell program, in Haskell, and then proves that the program properly implements that security. If a programmer gets security wrong, the compiler will complain rather than opening up a potential security bug in the system.
  • http://www.brics.dk/RS/01/16/BRICS-RS-01-16.pdf. Just in case you thought type systems only solved easy problems, this bit of Haskell gets the type system to prove two central theorems about the simply typed lambda calculus, a branch of computation theory!

The point of these examples is to point out that type systems can solve all sorts of programming problems. For each of these type systems, concepts of types are created that represent the ideas needed to accomplish this particular task with the type system. Some problems solved by static type systems look nothing like the intuitive idea of a type. A buggy security check isn’t normally considered a type error, but only because not many people use languages with type systems that solve that problem.

To reiterate the point above, it’s important to understand how limiting it is to insist, as many people do, that the dynamic typing definition of a “type” is applied to static typing as well. One would miss the chance to solve several real-world problems mentioned above.

The True Meaning of Type

So what is a type? The only true definition is this: a type is a label used by a type system to prove some property of the program’s behavior. If the type checker can assign types to the whole program, then it succeeds in its proof; otherwise it fails and points out why it failed. This is a definition, then, but it doesn’t tell us anything of fundamental importance. Some further exploration leads us to insight about the fundamental trade-offs involved in using a static type checker.

If you were looking at things the right way, your ears may have perked up a few sections back, when I said that Rice’s Theorem says we can’t determine anything about the output of a program. Static type systems prove properties of code, but it almost appears that Rice’s Theorem means we can’t prove anything of interest with a computer. If true, that would be an ironclad argument against static type systems. Of course, it’s not true. However, it is very nearly true. What Rice’s Theorem says is that we can’t determine anything. (Often the word “decide” is used; they mean the same thing here.) It didn’t say we can’t prove anything. It’s an important distinction!

What this distinction means is that a static type system is a conservative estimate. If it accepts a program, then we know the program has the properties proven by that type checker. If it fails… then we don’t know anything. Possibly the program doesn’t have that property, or possibly the type checker just doesn’t know how to prove it. Furthermore, there is an ironclad mathematical proof that a type checker of any interest at all is alwaysconservative. Building a type checker that doesn’t reject any correct programs isn’t just difficult; it’s impossible.

That, then, is the trade-off. We get assurance that the program is correct (in the properties checked by this type checker), but in turn we must reject some interesting programs. To continue the pattern, this is the diametric opposite of testing. With testing, we are assured that we’ll never fail a correct program. The trade-off is that for any program with an infinite number of possible inputs (in other words, any interesting program), a test suite may still accept programs that are not correct – even in just those properties that are tested.

Framing the Interesting Debate

That last paragraph summarizes the interesting part of the debate between static and dynamic typing. The battleground on which this is fought out is framed by eight questions, four for each side:

  1. For what interesting properties of programs can we build static type systems?
  2. How close can we bring those type systems to the unattainable ideal of never rejecting a correct program?
  3. How easy can it be made to program in a language with such a static type system?
  4. What is the cost associated with accidentally rejecting a correct computer program?
  5. For what interesting properties of programs can we build test suites via dynamic typing?
  6. How close can we bring those test suites to the unattainable ideal of never accepting a broken program?
  7. How easy can it be made to write and execute test suites for programs?
  8. What is the cost associated with accidentally accepting an incorrect computer program?

If you knew the answer to those eight questions, you could tell us all, once and for all, where and how we ought to use static and dynamic typing for our programming tasks.

Follow

Get every new post delivered to your Inbox.

Join 86 other followers