In my last post I started a discussion about the classic usability book "The Design of Everyday Things" by Don Norman. I talked about the concepts of "Affordances" and "Signifiers". These are the primary mechanism by which users interact with design. Affordances refer to a relationship between an object, the functions it can perform, and the operations that can be performed by a user on it to achieve these functions. Signifiers are part of the design that help users identify the presence of an affordance. Signifiers further indicate to a user "where" a particular user-action is to be performed to achieve a function. I tried to illustrate these concepts with examples illustrating a few key formal methods artifacts ("things").
In this post, I would like to introduce another concept -- Mapping -- used by Don Norman in his book and try interpret it in the context of formal methods.
Let us take the example of a type-system that I introduced in my last post. The artifact under consideration is a programming language; the "affordance" is the ability to construct a program having some properties (lack of runtime-errors), and the "signifiers" are type annotations. Here, a "mapping" is the relationship between program being written and the type-annotations.
Mapping
If signifiers are part of the design that indicate how a user can interact with an object, "Mapping"s locate and relate signifiers to the context in which a user would interact with the artifact. Many of the examples of mappings given in the book have a "spatial" flavour to them -- the layout of light switches "mapped" to the actual physical layout of lights. A good mapping allows a user to understand and predict what their action would achieve.Let us take the example of a type-system that I introduced in my last post. The artifact under consideration is a programming language; the "affordance" is the ability to construct a program having some properties (lack of runtime-errors), and the "signifiers" are type annotations. Here, a "mapping" is the relationship between program being written and the type-annotations.
Most programming languages have a way of annotating types in a way that follows the syntax of a program. In this sense the mapping is as close to perfect as it can get! I would like to give a couple of examples where the mapping of the type-system works well, using a couple of different programming languages.
Example 1
Below is a simple C++ function to calculate the maximum element in a list. The type annotations here are indicated in bold text.
unsigned int maxVector(std::vector<unsigned int> inputVector) {
unsigned int max = 0;
for(unsigned int elem : inputVector) {
if (elem > max) max = elem;
}
return max;
}In this example, it is clear (if you are aware of the basics of C++ syntax) that the function maxVector takes as input a vector of type std::vector<unsigned int> and returns an unsigned int. Equally, the for-loop in the program iterates over each element of inputVector and the conditional updates the local variable max with the maximum element seen so far. The type of max matches with the return type of the function and so the overall program is well typed and we have some assurance that it is "correct".
Example 2
A similar implementation in a functional programming language OCaml is given below. Again the type annotations are in bold text.
let maxList (ls : int list) : int =
let max (x: int) (y: int) : int = if (x > y) then x else y in
List.fold_left max 0 ls
Let us also look at situations where the mapping is not great. How many among you have struggled at one time or another with getting the types right when writing a functional program.
When things go wrong
The utility of mapping in the case of type-systems is really seen when things go wrong; the mapping provided by the type-system to the program plays a big role in localizing, identifying and fixing the program. Consider the example below of a modified version of the examples above
Example 3
unsigned int maxVector(std::vector<unsigned int> inputVector) {
int max = 0;
for(unsigned int elem : inputVector) {
if (elem > max) max = elem;
}
return max;
}Compiling the example above will give the warning:
hello.cpp: In function ‘unsigned int maxVector(std::vector<unsigned int>)’:
hello.cpp:9:18: warning: comparison between signed and unsigned integer expressions [-Wsign-compare]
if (elem > max) max = elem;
~~~~~^~~~~
Basically, there is a problem in the expression (elem > max) and a quick inspection of the code allows us to easily localize the problem to the declarations of elem and max, which obviously do not match: the declarations
- int max
- std::vector<unsigned int> inputVector
Note that the warning provided by the type-system is related to the notion of "Constraints" that I will talk about in a future post.
Let us take this example further
Example 4
template <typename T>
auto maxVector(std::vector<T> inputVector) {
auto max = 0;
for(auto elem : inputVector) {
if (elem > max) max = elem;
}
return max;
}
int main()
{
std::vector<unsigned int> vect{1,2,3,4,56,7};
cout<<"Hello World " << maxVector(vect) << std::endl;
return 0;
}
In the above example, I have tried to eliminate explicit typing as far as possible to focus on the concept of mapping. Compiling the above code using C++14 compiler gives the following warnings:
hello.cpp:10:18: warning: comparison of integers of different signs: 'unsigned int' and 'int' [-Wsign-compare]
if (elem > max) max = elem;
~~~~ ^ ~~~
hello.cpp:20:29: note: in instantiation of function template specialization 'maxVector<unsigned int>' requested here
cout<<"Hello World " << maxVector(vect) << std::endl;
^
Here, although we can localize the warning to the expression, the mapping of types to the expressions is not so simple -- some of the mappings are implicit because of the use of the template argument T and the use of auto.
- We have to look at the instantiation of the template to the expression maxVector(vect) and from there further localize it to the declaration std::vector<unsigned int> vect{1,2,3,4,56,7}.
- We have to use the knowledge that the literal 0 in the declaration auto max = 0 is actually interpreted by the compiler as an int
- Finally, we can localize the problem to the mismatch between the types of vect and max.
This was a much more difficult exercise to decipher the error than Example 3, and this can be attributed to the fact that the implicit type rules in C++14, can result in much more complex mappings of the affordance of types.
A similar argument can be made in the OCaml example. In Example 2 above I have been explicit in terms of type-annotations. But OCaml (and many functional languages) are typically equipped with type-inference systems that do not require the programmer to annotate types. The following is a completely valid program that achieves the same purpose as Example 2
Example 5
let maxList ls =
let max x y = if (x > y) then x else y in
List.fold_left max 0 ls
As you can see there are no type annotations to be seen anywhere -- this is a particularly complex mapping of the affordance of he type-system: it is missing altogether!
Although type-inference allows the programmer to type less code and is arguably less "ugly" with fewer intervening annotations, the implicit mapping makes the affordance of the type-system much more difficult to use.
I am sure many of you have at some time or another torn out your hair when trying to fix a "type-error" in your program: in ocaml, you end up adding random type-annnotations at various points in the program, and in C++ you just wilt when faced with a 8000 line error message to do with templates that expand your horizons in terms of header files that you have never heard of before!
Conclusion
In the post above, I have tried to explain the notion of mapping when applied to the affordance of types provided by a programming language -- it is something that helps you "localize" and "locate" the affordance with respect to an artifact and helps users comprehend the relation between affordances and the artifact. In many cases it is spatial, and the example given in the book of mapping is spatial in the geometric sense:
the layout of light-switches on a switch-board mirrors the geometry of lights in the ceiling.
In the case of programming languages and type-systems it is also spatial, but not quite geometric.
