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.
Intuitionistic Type Theory 