So many types, so little CPU time
As I confessed in my welcome blog, I had written blogs before. This is yet another previously written blog. I chose this one to port second because it naturally follows up my previously ported post on types. So her is the Avail type system blog circa January 2013.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A long time ago in a decade far away (the 1980's), there lived a little boy who enjoyed watching TV. He often watched PBS, as children without cable often did at that time. One show in particular caught the attention of this boy; the show was called Square One. The show was all about math. It had mini-game shows and pseudo dramas all centered around math. In the very first episode of Square One, there was a song about the number infinity. It challenged someone to think of the biggest number there was, then, after sputtering out a number in the billions, he was told to add the number one. This little tirade popped up every now and then throughout this episode, to drive home the point that infinity is, well, infinite. During that show, a light went off in the mind of that little boy and a burgeoning math nerd was born.
Who was that boy you ask? Well, that boy was me … Wait, I hope you weren't expecting some sort of Shyamalan-esque twist just then. Because it really is just a small anecdote from my life when I was about 6 years old that I'm using to introduce the Avail type system. I know, I know, pretty far from narrative genius. On that I would agree. But this was my very first encounter with the formal concept of infinity. A pretty significant event in my life. Of course this wasn't my first notion of something infinite. No my earliest memories of an attempt at thinking and reasoning was that the city of New York had no end because it was all I could see when I looked out the window. Hey, when you are about 3 years old, you draw your conclusions based upon the data available to you at the time. And let me tell you, for a kid that age, an infinite New York is a pretty deep thought! Fast forward to half my life later and you have that episode of Square One introducing me to infinity. Numbers going on and on forever? As a six year old boy, that was something I could get behind. Why? Well, when I was 6, "just add one", was a reasonable response to just about anything.
In Avail, I've come across the concept of infinity quite often. Not only because I have used the character, ∞, in the construction of many tuple types, but because the concept of infinity is a core part of the Avail type system. And wouldn't you know, type systems is the thing I'm about to talk about next.
In my previous post on types, I discuss how types are used to categorize common things. At a very high level, the formal organization of types in a programming language is referred to as a type system. From the very primitive type system of C, to the very rich type system of Avail, all programming languages have some form of a type system that varies in complexity. Avail's type system can be described as an infinitely calculable Structural type system that is both Strongly Statically typed as well as Strongly Dynamically typed and contains both implicit and explicit typing… Or at least, I think that's how it should be described. You see, I've run into a problem when attempting to describe Avail's type system. Now that problem isn't that I don't know how the Avail type system works because I understand it fairly well. No, the problem appears to be with the subject of type systems; it isn't evident to me how type systems should be described.
The study of type systems in computer programming is a rather new field of study. It lacks the years of maturation found in subjects such as algebra or physics. It would be nice to be able to rattle off a few well accepted general descriptors about type systems in this post and be on my way. But as far as I can tell, there doesn't even seem to be a consistent lexicon across the entire subject. Couple that with the variation inherent in type systems across programming languages, and you find yourself with quite the onerous task when attempting to describe a type system.
Now, Todd has gone through quite a lot of work to describe the Avail type system in great detail. And after you feel like you have a decent grasp on type systems, I highly encourage you to read his work, though, it would be nice if you finished reading this post first (I mean, you already started reading it and I spent so much time writing it…). As is typical with my recent posts, I won't be rehashing concepts that have been treated well elsewhere. In order to help you understand the Avail type system, I will, however, be providing descriptions of what appear to be common high level classifications of type systems. I'll close it out with a word or 50 on the Avail type system in particular.
Structural versus Nominative
If you know what identity is, then you already know about the fundamental difference between nominative and structural types: the types of nominative type systems have identity where as the types of structural type systems do not. By providing something with identity, you are providing an artificial way of distinguishing two identical things. Identity is a rather important concept in programming, so I think it is important to provide more detail about it. Let's roll out an example using my prize possessions and see if it is enough to capture the essence of identity.
I have two identical book ends sitting on my bookshelf holding up books (identical in a way that if I were to take them off the book shelf, shuffle them behind my back, then bring them out, you wouldn't know which bookend came from where). Aside from the fact that there are two bookends visible, the only way you can tell them apart is from information that has nothing to do with being a bookend, chiefly location. For my bookends, I will refer to the one on the left as Tom and the one on the right as Jerry. Now the only way you can tell Tom and Jerry apart is based on their current location. By labeling my bookends based upon their location, I have given the bookends identity. What were two indistinguishable bookends have now become distinguishable by their reference, a construct that has nothing to do with what being a bookend means. Now that my bookends have identity, can I no longer interchange them at will? After observing Tom and Jerry on my bookshelf, could you be certain that the Tom and Jerry you observe today is going to be the same Tom and Jerry you might observe the day after tomorrow? Would I be so devious as to swap them when you are not around? Well, maybe… However, I can tell you that I am devious enough to fabricate the existence of bookends that I do not have in order to make a point. That point being some things, though given identity, are still interchangeable.
So, identity is an artificial construct you provide to a thing in order to distinguish it from other things that are otherwise indistinguishable from it. Clear? Great! Now back to structural and nominative type systems. Structural type system types do not have identity. Therefore the types integer, (-∞,∞), and ℤ are all considered the same type in a structural type system even though they have different names. The structure of the type itself determines equality, not the reference of the type (in this case the reference being the name). On the other hand, nominative type system types have identity. Under this type system the types integer, (-∞,∞), and ℤ are considered to be different because they have identity; different names or references provide a way to differentiate these structurally identical types. The consequence of this is that two functions that perform the same operation but only vary by their signature, would be considered inequivalent. For example, the addition function, "_+_", when defined under the two signatures, [integer,integer]→integer and [(-∞,∞),(-∞,∞)]→(-∞,∞), would be considered two distinctly different functions. Within a structural type system, you would only need to define this function once regardless of the name you use for the types as long as they were structurally equal.
Static and dynamic typing refer to the practice of type-checking. Type-checking is the process that a computer programming language uses to confirm a written program is performing compatible operations on the types appearing in the program. In essence, it is the same thing as following your friend into the kitchen to watch them make toast to ensure they use the toaster and not the dishwasher. The extent to which a language performs type checking indicates, in a nebulously defined way, the "strength" of the type checking (strong vs weak). "Less checking" leads to a system being labeled Weak, where as more checking leads to a system as being labeled Strong. The key difference between Static typing and Dynamic typing is primarily when the types are checked for a given program.
Static typing refers to a system that does type-checking at compile-time. Compile-time refers to the point at which the language translates a written program from human-readable code to another type of code, generally machine-readable. At this point, a computer program is not being "run". There is no data flowing through the program, hence the state of your program is static. It is just the code someone has written being translated to a set of instructions that the computer can use to execute your program. During this process, information is made available to the compiler through the written program. This enables the compiler to tell what sorts of types can be expected when running the program. The more a compiler can confirm the type correctness of your program (no making toast in the dishwasher), the stronger the static type-checking is said to be, which results in less errors when your program is run. As the program is not being run at this point, it cannot use the context of the executing program to determine if there will be a problem down the road.
Dynamic typing refers to a system that does type checking during run-time. Run-time is the state of a program when it is actually running. When you interact with a computer, your interactions are generally with a running program. The implications of run-time type checking vary from that of compile time checking. Though it is generally too late for a programmer to fix a type error in his/her code once the program is running, it permits a programmer to use a powerful tool, dynamic dispatch (the ability to hold off on deciding what operation to take until you know what type you are working with).
It is important to note that static typing and dynamic typing are not mutually exclusive features in a programming language. The more a language can utilize both features, the less error prone and more flexible their programs become.
There seems to be an identity crisis with this concept in the subject of type systems. It is apparent that there exists two sets of names for this one concept. Lets take the structural type system approach and call the named versions equal as they are equal in structure. Explicit typing (manifest typing) describes the act of explicitly declaring a type while programming. For example, the code: x : integer := 5; creates a variable, x, and sticks the number 5 into it. We know that the variable, x, is of type integer because it is explicitly labeled to be integer. And that's all there is to it. As you can see, explicit typing is pretty straight forward.
As you might have guessed, implicit typing is the practice of not explicitly declaring a type. Implicit typing is when a compiler can infer what the type of something might be given the context clues of its usage. For example, the code: x := 3 + 5 does not explicitly tell us the type of the variable, x. Though it can be inferred by the compiler that the x is an integer because both the number 3 and the number 5 are both integers.
Given the above descriptions, you should be able to parse my earlier description of the Avail type system, "...an infinitely calculable Structural type system that is both Strongly Statically typed as well as Strongly Dynamically typed and contains both implicit and explicit typing...". The only part I haven't described is that "infinitely calculable" bit. See, Avail's type system is infinite in nature, but as we've learned from Square One, you can't just sit around and wait for infinity to be calculated. When you load up Avail, it doesn't take until the end of time to load because it does not precompute the entire type system. However, it does have the ability to recognize an infinite number of types. In this way, Avail's type system is infinitely calculable.
You might be wondering how there can be an infinite number of types. Let's consider the Avail type, integer. There are infinitely many integers. To understand the implications of that, take for example the integer range [2..4]. This is a subtype of the type integer, however integer is not the only supertype of this integer range. It is actually a subtype of infinitely many other distinct subtypes of integers. One can easily illustrate this by constructing the integer type range, [2..n], where n is an integer strictly greater than 4. There are infinitely many integers that fit this criteria. Subtyping integers in this way alone provides an infinite number of types.
To sum it all up, what infinitely calculable mostly means is that Avail does not need to explicitly know about a type that exists in its type system before a type is presented to Avail by a programmer. Once Avail is told by a programmer about the existence of one of its types, Avail can then tell you a lot about that type and it'll know what can and can't be done with it. In this way Avail is like a sleepy old librarian. She couldn't tell you the name and contents of every book in the library, but if you hand the librarian a book, she can walk you to where that book came from and tell you all sorts of things about that book and even answer any questions you might have about the books related to it. Of course, this particular library is infinite in size and filled with an infinite number of books. But like Hilbert's Grand Hotel, there is always room in Avail's type system for more books!
| ‹ Previous | | | Return to Rich's Blog | | | Next › |
