Informally speaking, what is a type?

As I confessed in my welcome blog, I had written blogs before. This is the first of my ported blogs. I chose this one to port first because this was the first time I stepped back from my blogs to reassess what I was trying to communicate, mainly information about Avail. I wanted to start from step one, and this seemed like the obvious choice. If I had to date this blog, I'd say circa January 2013.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

In the past few months I have been undertaking the feat of becoming a more knowledgable programmer. Scratch that, let's just say I have been trying to become a programmer; preferably one that is knowledgable about the domain as a whole. To achieve this goal I have been doing a lot of reading and research. The more I learn, the more doors open leading to more questions. These new questions lead to more reading and more research, which of course leads to more questions (it has been rather invigorating as I haven't been this cerebrally active since grad school). I've tried my best to catalog this academic journey on this blog. The posts have been an evolution in writing style as well as technical content. From that sentence if you understood my meaning to be "some posts have been good and some have sort of sucked", then you've drawn the right conclusion.

My goal, of course, is not to waste your time with pointless garbage, but to compose good posts that are worth reading. Because of that, I'd like to address something common to all of my posts that has been nagging at me: I have written them with the one very large assumption that all my readers know what a type is. While perusing the Avail website, if you find that you are often asking yourself, "What is a type?", then this is the blog post for you!

So what is it that I hope to achieve in this blog? Well, I don't think it is a good idea for me to go into a formal exhaustive discussion of type theory. In fact, that is exactly what I intend not to do. It is my goal to provide you with what I believe to be the basic understanding of types that will allow you to not only understand my blogs, but also to go off and comfortably compose your own programs. So in this post I will go over a few things that I believe are important to this topic.

In order to program Avail (or mostly any other languages for that matter), you should have:

1. some idea of what a type is
2. some grasp on how types interact

You might have picked up on how I slyly put a link to a somewhat basic academic description of Avail types in the question, "What is a type?", posed above. I did this to give you a starting point to work from as I do not intend to fully reinvent the wheel. In fact, I will link to other sources throughout this blog to help provide background on the discussion. So if you are unfamiliar with types, you should consider reading this before continuing on with this post. It's ok, go ahead and read it, I'll wait.

Finished? Good. If you read the the section on types linked in the previous paragraph, then you should at least know at a high level, that a type is a description of a common group of things. Number one: check.

Now for number 2. The good news is that if you have a basic understanding of set theory, then you are pretty much in a good place to understand how types interact. To be honest, the level at which sets approximates types is all you really need to know in order to program. And believe me, what you need to know about sets and types isn't much. If you don't know what a set is, I encourage you to go here and read a little. It will quickly become evident what a set is by reading this introduction. If you can read and understand the whole thing, great! Again, I'll wait until you've finished reading before proceeding.

Ok, got it? Good. Incidentally, Avail does have a type called set which you can read all about (though, I'd do that later).

Now that you know what a set is, there are two very important set operations that you should know about: union denoted by ∪, and intersection, denoted by ∩. If you are unfamiliar with these operations, read the hover text and/or go to the links provided to gain a better understanding of these operations. As you will soon see, these operations are also applicable to types.

So, how exactly is a type like a set? Membership. Things belong to types in the same way that things belong to sets. Sets have a collection of distinct elements that are members of the set. Similarly, types have a collection of distinct instances. An instance is a member of a type that represents some concrete implementation or value described by the type. For example, the number 1 is a concrete value that is an instance of the type, natural number. Natural numbers describe positive numbers; numbers that have some value greater than zero. The number 1 fits that definition, hence it is an instance of natural number. It is important to note that the number 1 belongs to more than just the type, natural number. It is also an instance of integer, whole number, and odd number just to name a few (in fact, it is an instance of infinitely many other types, but we'll talk about that when we get into the Avail type system).

Because sets and types are similar along the axis of membership, the operations of union and intersection as defined on sets can also be applied to types. The avail library has two nifty methods that do just that, "_∪_" and "_∩_". An example use of union would be the creation of the type integer from the three types: negative integer, positive integer, and 0's type (a type whose sole instance is the number 0).

This operation is called type union. We can also create a new type by finding the intersection of types. If you had the intersection of the two types, prime number and even number, the resulting type would be 2's type as 2 is the only number that is both even and prime. This operation is called type intersection.

Just like with sets, you can take "subsets" of types. A subtype relates to a type in the same way a subset relates to a set. You can take some instances from a type to create a subtype. For example, you can take from the type integer all negative integers to create a new type, negative integer. Because all instances of negative integer are also present as instances of the type integer, then you can say that negative integer is a subtype of integer:

To describe the relationship from the other direction, you would say that integer is a supertype of negative integer (all of the instances of negative integer can be found in integer). A supertype, S, of a type, T, is itself a type that contains at least all of the instances found in the type T. As you might have guessed, we do have a method that tests to see if one type is the subtype of another, "_⊆_".

So why does this all matter? Invariably all programming languages have to deal with the question, "can you do x with y?". Just as in everyday life, it only makes sense to perform certain actions with certain things. For example, I can ride a bike, but it would be silly to try to ride a scone. The bike is a vehicle, the scone is a food (if it is proven someday that a scone is in fact a vehicle, I will change this example). If you sat on a scone and tried to ride it, first off you wouldn't go anywhere. After not having gone anywhere, when you got up, what remained of the scone would not resemble a scone. Now it isn't that the bike "understands" the concept of being ridden and the scone does not, it is the fact that the bike and the scone have observably different properties that gives us clues on how we can interact with them. A bike has wheels, pedals, and a seat, so let's ride it! A scone contains nutrition, it is tasty, and it is digestible, so let's eat it! Hell, let's get on that bike and ride it while we eat our scone! This of course isn't advised, especially while drinking hot tea, but the intrinsic qualities of these things will permit us to attempt such an operation.

Of course there exists internal sensibilities that keeps us from sitting on that scone or chomping on that bike. These sensibilities have been developed through years of life experience and interacting with the things around us (or just a good friend who tells you, "dude, don't eat that bike"). It is the context of what we presently know that helps us categorize new things along side things with which we are already familiar. Thus we are able to confidently apply the sorts of operations we know to be compatible with similarly categorized things to said new thing. In this way, we develop our own type system for life.

Some programming languages replicate this life context in the form of a compiler. Not only does a compiler have the ability to translate your program into instructions the computer can understand, it also can have the potential to tell you if you've set up your instructions in such a way that, when run, could possibly lead to someone attempting to consume a bicycle. A language that does this for you is in some part type-safe. At a high level, the degree of type-safety in a programming language is measured by how effective the language is at keeping you from permitting an unintended operation on a type with which the operation is not compatible.

I can continue to go on about this at length as there is much more to be said. However, I indicated that this post was not about providing a full treatment on types, but instead to give an overview that will help in understanding Avail as well as the content of my posts. Naturally, this leads us into a conversation about the Avail type system, which will set us up nicely to discuss semantic restrictions. So marinade on this for a few days, and I will hopefully have another post coming out soon.

NOTE: I'd be remiss not to mention the fact that the Avail type system does not support user customizable predicate types such as even numbers or prime numbers. In other words, I cannot define a type as: {x ∈ ℤ, x = 2m + 1, m ∈ ℤ}. It is impossible to determine the equality of the range of two different functions that, in theory, produce the same results. Therefore it cannot be determined in general that two different, yet equivalent functions used as predicates for a type, are equal types. The examples provided above, though not applicable in the Avail type system, were used because they are fairly straightforward making the presented material more tractable for the concept it was conveying.

‹ Previous

|

Return to Rich's Blog

|

Next ›