A new kind of programming language

The intuitionistic programming language (IPL) is a new open source programming language, implemented in OCaml, combining a very high level of abstraction with compilation to efficient LLVM bytecode.

The semantics of IPL is intuitionistic type theory without recursive types. Type-theoretic constructs, such as lambda abstraction, pairing, and proof objects, are eliminated at compile time using a new algorithm which translates any type-theoretic term of base type, in a context where all variables are of base type, into clean LLVM bytecode.

See http://intuitionistic.org for more information.

Heidelberg Laureate Forum

I participated in the 1st Heidelberg Laureate Forum last week and contributed a couple of blog posts to the official HLF blog. You can find them here: http://www.scilogs.com/hlf/author/granstroem/.

Virtues and vices of object-oriented programming

Some time ago, Paul Graham wrote an essay with the title “Why Arc isn’t especially object-oriented“, which contains some interesting arguments against object-oriented programming. Jonathan Rees’ comments on the essay are also worth reading.

To my mind, what makes object-oriented programming problematic is its complex denotational semantics. As far as I know, the state of the art of semantics for object-oriented programming is A Theory of Objects by Abadi and Cardelli. The complexity of the semantics of (recursive) object calculi is daunting in comparison with the semantics of, e.g., simply typed lambda calculus (or intuitionistic type theory for that matter).

In essence, the problem with the object-oriented paradigm of programming is that it allows for (and encourages) programs that make use of mutually recursive object classes. It is not unusual that the whole object model of a program has to be understood as a whole. Because of the tight coupling between object classes, the semantics of object-oriented programs is noncompositional (though, of course, one can program in an object-oriented language without making use of its noncompositional features). A lack of compositionality leads to a lack of reusability:

“I think the lack of reusability comes in object-oriented languages, not in functional languages. Because the problem with object-oriented languages is they’ve got all this implicit environment that they carry around with them. You wanted a banana but what you got was a gorilla holding the banana and the entire jungle.” — Joe Armstrong, quoted by Seibel in Coders at Work (2009).

However, as Jonathan Rees writes in the post cited above, object-orientation is not an entirely well-defined concept. He gives several examples of object-orientation being defined as subsets of the following list:

1. “Encapsulation – the ability to syntactically hide the implementation of a type. E.g. in C or Pascal you always know whether something is a struct or an array, but in CLU and Java you can hide the difference.
2. Protection – the inability of the client of a type to detect its implementation. This guarantees that a behavior-preserving change to an implementation will not break its clients, and also makes sure that things like passwords don’t leak out.
3. Ad hoc polymorphism – functions and data structures with parameters that can take on values of many different types.
4. Parametric polymorphism – functions and data structures that parameterize over arbitrary values (e.g. list of anything). ML and Lisp both have this. Java doesn’t quite because of its non-Object types.
5. Everything is an object – all values are objects. True in Smalltalk (?) but not in Java (because of int and friends).
6. All you can do is send a message (AYCDISAM) = Actors model. – there is no direct manipulation of objects, only communication with (or invocation of) them. The presence of fields in Java violates this.
7. Specification inheritance = subtyping – there are distinct types known to the language with the property that a value of one type is as good as a value of another for the purposes of type correctness. (E.g. Java interface inheritance.)
8. Implementation inheritance/reuse – having written one pile of code, a similar pile (e.g. a superset) can be generated in a controlled manner, i.e. the code doesn’t have to be copied and edited. A limited and peculiar kind of abstraction. (E.g. Java class inheritance.)
9. Sum-of-product-of-function pattern – objects are (in effect) restricted to be functions that take as first argument a distinguished method key argument that is drawn from a finite set of simple names.”

In intuitionistic type theory, these nine points can be interpreted as follows.

1. Encapsulation. In intuitionistic type theory, encapsulation can be achieved in the three ways: (1) as in abstract algebra, (2) by using a module system, and (3) by using interfaces.
2. Protection. Protection is achieved much in the same way as encapsulation.
3. Ad hoc polymorphism. An implementation of intuitionistic type theory can support ad hoc polymorphism.
4. Parametric polymorphism. Parametric polymorphism is an application of dependent types. That is, any implementation of intuitionistic type theory has to support parametric polymorphism.
5. Everything is an object. In intuitionistic type theory, a value is usually defined as a canonical object, and every entity dealt with is either a type or an object (though, the type-theoretic notion of object differs from that of object-oriented programming).
6. All you can do is send a message (AYCDISAM). This is true in a very strict sense in the component model of intuitionistic type theory. A component can only send messages on its required interface.
7. Specification inheritance. Subtyping is usually not implemented in intuitionistic type theory. The type-theoretic component model uses composition instead.
8. Implementation inheritance/reuse. The component model of intuitionistic type theory supports meta-programming, a very powerful mechanism for reuse. Though, implementation inheritance is not supported.
9. Sum-of-product-of-function pattern. Intuitionistic type theory makes a distinction between functions and methods and between objects and components. A component is essentially a sum of methods.

Thus, in a sense, intuitionistic type theory with the component model can be seen as an object-oriented programming language with features 1, 2, 3, 4, 6, and, in a certain sense, 5, 8 and 9. In the explanations above, I speak of the component model of intuitionistic type theory. The concepts that form the basis of this component model are derived from an article by P. Hancock and A. Setzer (“Interactive programs in dependent type theory”, in Lect. Notes Comput. Sci., vol. 1862, pp. 317-331, 2000). The details on how these concepts make up a component model will be given in later post.

My conclusion is that many aspects of object-oriented programming are worth preserving. In particular I propose intuitionistic type theory as a way to unify functional programming, component based programming, metaprogramming (MDA), and logical verification. The aspect of object-oriented programming that has to give way is the notion of class. The notion of class unifies two notions I think ought to be kept separate, viz., the notion of record type (structure) and the notion of implementation of an interface, or collection of methods. The first notion is available in most programming languages, and, in particular, in intuitionistic type theory. For the second notion, the component model of intuitionistic type theory substitutes the notion of component.

Further reading…

Mathematics and computer science

Mathematics, logic, and computer science share a common history. Mathematics and logic are ancient dragons, and not much upheaval is to be expected in their futures. But where lies the future of computer science?

Many philosophers of the 20th century embraced a view going back, at least, to Leibniz, viz., that, by using a formal language where all assumptions are made explicit, most differences in opinion can be solved by tracing the differences back to different (implicit) assumptions. It becomes evident, by reading a newspaper, e.g., that this view, though of great potential, has not had a large impact in the domains of every-day life.

Computer science would seem to be much more fertile soil for such ideas, and this makes it all the more surprising that computer programming is an activity performed by people who, by and large, have little or no knowledge about formal languages and formal methods.^[1] Since at least three decades, the computer industry is full of buzzwords with little or no real signification. How many products, packages, and technologies have not promised to empower their users beyond what is reasonable to expect?

There seems to be no evidence that the quality of newly written software is better than the quality of old software. In many application domains it even seems to be worse. This is partially explained by the increasing complexity of software and the thin spread of competent programmers: a disastrous combination. Appeals for more scientific and rigorous approaches to IT-projects have been voices crying in the desert.^[2] This unfortunate development is a consequence of the human mind meeting the unrelenting computers, without sufficient respect for the complexity of the problem at hand. The obvious but tedious solution is the application of logic.

There are two approaches to logic in computer science. The first approach is to apply some logical formalism, e.g., propositional logic, to a conventional programming language. The second approach is to replace the conventional programming language with a language designed by logicians. In the former case we speak about formal methods and in the second case we speak about formal languages. The language advocated here, Martin-Löf’s type theory, is of the second kind, i.e., a formal language: type theory is not an add-on to a conventional programming language, but a programming language in its own right.^[3]

Though Martin-Löf’s type theory usually is associated with functional programming, there is no real reason to limit its application to batch computing. Haskell’s monad system, and the many interactive programs written using it, shows that the style of programming dubbed functional also can handle interactive programs.^[4] The long term goal of much ongoing research on Martin-Löf’s type theory is to enable programmers to write complete applications using the language of Martin-Löf’s type theory, including graphical user interfaces, web interfaces, business logic, workflows, integration components (e.g, Web Services, COM+, CORBA, etc.), system calls (Win32, POSIX, etc.), database interaction (e.g., ODBC), native code interoperability, and database schemata.

There is no royal road to software correctness. Martin-Löf’s type theory is a great tool, but we also need a method to address the quality problems of software: “Controlling complexity is the essence of computer programming”. Therefore, we, programming language designers, software architects, and computer programmers, have to face the hard facts and deal with the problems accordingly. At this point I think it is fitting to review Descartes’ method of rightly conducting the reason. In his Discours de la méthode he writes that he thought that the following four precepts are sufficient:^[5]

• “The first was never to accept anything for true which I did not plainly know to be such; that is to say, carefully to avoid hasty judgement and prejudice, and to include nothing more in my judgements than what presented itself to my mind so clearly and so distinctly that I had no occasion to call it in doubt.
• The second, to divide each of the difficulties I would examine into as many parts as possible and as was required in order better to resolve them.
• The third, to conduct my thoughts in an orderly fashion, by commencing with those objects that are simplest and easiest to know, in order to ascend little by little, as by degrees, to the knowledge of the most composite things, and by supposing an order even among those things that do not naturally precede one another.
• And the last, everywhere to make enumerations so complete and reviews so general that I was assured of having omitted nothing.”

I think that these four points, conceived in 1637, form a much more realistic and rigorous ground for software correctness than, most modern project methodologies.

Descartes’ four precepts codify a mathematician’s way of approaching a problem. To my mind, there is no essential difference in how a computer programmer ought to approach a practical programming problem. Indeed, Martin-Löf’s type theory is both a foundation for constructive mathematics and for computer programming.

“In fact, I do not think that the search for high level programming languages that are more and more satisfactory from a logical point of view can stop short of anything but a language in which (constructive) mathematics can be adequately expressed”^[6]

The appeal for a programming language of mathematical rigor is even more urgent today, when we develop larger and larger systems. If the confidence in software is to be maintained, the links with mathematics and logic that computer science had in its infancy must be maintained and nurtured. By its very nature, Martin-Löf’s type theory is a very important link between the three subjects.

References

^[1] Cf., E. W. Dijkstra “On the role of scientific thought”, pp. 60-66, In Selected Writings on Computing: A Personal Perspective, Springer-Verlag, 1982 (PDF).
^[2] Again, cf., E. W. Dijkstra, op. cit.
^[3] Cf., Martin-Löf, “Constructive mathematics and computer programming”, 1982 (PDF).
^[4] I take the existence of the book Real World Haskell to be a constructive proof of this claim.
^[5] Descartes, Discours de la méthode, Ch. 2, transl. D. A. Cress.
^[6] Martin-Löf, op. cit., last sentence.

Software composability

On Channel9, there an interesting interview with Anders Hejlsberg, Herb Sutter, Erik Meijer and Brian Beckman from Microsoft.

http://channel9.msdn.com/shows/Going+Deep/Anders-Hejlsberg-Herb-Sutter-Erik-Meijer-Brian-Beckman-Software-Composability-and-the-Future-of/

One of my mantras is that compositionality is the key to programming language design and software architecture. It is great to hear that some of the greatest minds at Microsoft agree!

Three perspectives on the application

Let us consider the the notion of application from three different perspectives: from the user’s perspective, from the architect’s perspective, and from the perspective of Martin-Löf’s type theory. 

Assuming an interactive application, the first thing that strikes the user is, of course, the graphical user interface and its aestetic aspects, such as colour and shape. After that we have the ergonomic aspects, usability aspects, or interaction design, such as logical placement of buttons and menus, proper choice of controls, proper rating and aggregation of information, etc. 

Next we have the dynamic aspects of the application: the commands that the application supports and their proper implementation. For example, when checking out a shopping cart, money must be drawn and gods delivered. 

Finally we have the user’s view of the entities of the application, such as products, and shopping carts for a web-shop. These entities have relations between them, e.g., a shopping cart contains products. Moreover, entities have attributes, e.g., a product has a delivery status. These three, entities, relations, and attributes, can be called static aspects. This summarizes the user’s view of the application. 

We now turn our attention to the architect’s view. Here the ordering of the aspecs is different, indeed, often the reverse: while the user’s view follows the order of knowning (ordo cognoscendi), the architect’s view follows the order of being (ordi essendi), or, better, the order of conceptual priority. Moreover, while the user deals with individuals, the architect deals with universals. 

The architect considers the same static aspects as the user, albeit as universals rather than as particulars, i.e., he considers the entity book instead of this or that particular book. He also considers the same dynamic aspects as the user, but, again, universally instead of individually.  

With proper separation of concerns, the aestetic aspects need not be the concern of the architect. However, the ergonomic aspects are difficult to separate completely from the static and dynamic aspects, as the former depend on the latter. For example, one cannot display attributes that are not in the static model or aggregates that are not computable. Similarly, the dynamic model may limit the ergonomic design: perhaps one cannot pay before choosing delivery address because the shipping cost differs between addresses. 

To my mind, the correct order of conceptual priority is: static, dynamic, ergonomic. Although designing things in this order will not work if the static or dynamic models make unrealistic simplifications of actual problem domain. For example, the architect may allow only one delivery address per invoice while the ergonomic design requires the user to be able to pick delivery address per invoice line: here the static model is in error. The conceptual priority is correct, but reality is prior to every concept. On could say that the ergonomic aspects ought to have a corrective function on the static and dynamic models. 

Having said this much about the user’s and architec’s perspective of an application, it is time to have a look at how all artifacts that the architect deals with can be captured within the framework of Martin-Löf’s type theory. Martin-Löf’s type theory deals with 

• types, and
• objects of types.

Although the perspective of Martin-Löf’s type theory seems very limited compared to the user’s and architect’s perspectives, it in fact encompasses both in the sense that the user’s and architect’s notions can be given logically satisfactory definitions in type theory. In general, the notions of the architect become types and the notions of the user become objects.  

Yours truly at Channel9

http://channel9.msdn.com/posts/MSDNSweden/Svea-Ekonomi-uses-F-for-automated-billing-system-for-the-Telecom-industry/