: New: The Power of Type Theory in the Context of Buffoonery

In programming, there are types. E.g., if your program says x = 2, it's also useful to say that x has the Integer type. That allows us to organize our functions based on the kinds of thingies they can operate on.

Type can let you keep track of things that might not be obvious from the data itself. Maybe you're writing a web app. Much of the data it juggles is text blobs, and you want to keep track of which of these have already been HTML-encoded. If you just see "foo", you don't know whether it's gone through an HTML-escaping. It's pretty easy to define RawText and HTMLText and to write functions to convert between them. And for each text blob that your webserver needs to display, you can easily figure out what kind of text the display function expects to work with. Yay, you can write your web server with some confidence that you're not displaying un-escaped HTML.

You can do more sophisticated correctness-checking with types. At my last job, this backfired. In C++, if you want to do really sophisticated things with types, you probably need template metaprogramming. This tends to mean that you're writing code which few people can read. There probably isn't anyone who can double-check your work. If your template metaprogramming spaghetti needs changing and you are on vacation, expect things to break when someone else tries to understand your code.

Now I work with Scala programmers. Scala allows you to do some pretty powerful things with types; you can do so more simply than you can in C++. (I don't know yet whether that means that you can write sophisticated-yet-readable type-fiddling code in Scala; I haven't tried to read any yet. But at least there's potential.) So now I hear about type theory. Not just hear about it as a bugbear that lures you into writing unreadable code; I hear about it as a legit tool.

So I heard about container types. Type theory aficionados delight in telling me that containers are not exactly the same as collections, but you have to study type theory for years before you can understand the difference.

Scala has other interesting types. There's the Option[Foo] type, which might be a Foo or might be nothing. You might imagine a square-root function returning an Option[Number]; sqrt(9) would return 3, but sqrt(-9) would return None. A program can pass around an Option, only peeking at the answer when needed.

There's a similar Future[Foo] type, which represents a value which we might not know yet, but which is expected to show up eventually. Maybe your program needs some data that's stored on another computer on the network. Your program wants to dispatch a request to that other computer, but wants to work on some other stuff meanwhile. Your program can use a Future as a handle on that request. When a response comes back from the other computer, the response goes into that Future. When your program gets the value from the Future, things might pause if that response hadn't shown up yet, but they start up again when the response arrives; your program can then read the value.

While kibbitzing at a Scala class (yes, I've fallen back into internal technical training), I learned that Options and Futures aren't containers. I still don't know what containers are. I hear that they're more general than collections. Options and Futures seem pretty darned close to collections. Maybe it's the word "container" and a particular container that sticks in my mind. That's what was in my mind when I piped up in the class' IRC peanut gallery

Options and Futures seem like containers to me.
Specifically, they remind me of Schroedinger's cat box.

The type theory experts told me that I'd made a funny joke. I was glad that they'd found it funny. But I was just 50% joking. Just as an Option allows a program to manipulate a value which may or may not exist, type theory allowed me to put together a joke based on a concept that I may or may not understand.

Tags: programming

web+comment@lahosken.san-francisco.ca.us
blog comments powered by Disqus

Updates:

Tags