[Prev][Next][Index][Thread]
Re: Help with type advocacy
Dear Ken,
The following is my take on why types are interesting for many CS
disciplines, coming from my brief, and arguably rather nonstandard,
experience in this field.
* * *
Types are to me first of all classification. They classify program
phrases and, more generally, behaviour of software: and not only that,
along with classification, they also often give us an idea of algebra
of programs: how we can compose a program phrase (or a software
component) with another, when it is allowed and when it is forbidden.
This control of composition leads to the control of behaviour, by
allowing only specific types of programs to be composed by a given
operator, resulting in a specific type of programs.
Any computing disciplines deal with some ideas of computational
behaviour: most, in particular, treat the behaviour of software.
Visible, invisible, abstract, concrete, ... anyway that which is in
the mind of programmers when they design and program, and that which
is realised when the resulting program runs.
If to create, understand and control these behaviours is a main issue
in CS disciplines, and if it is important how one can control them
incrementally, then it matters how we classify them, and how we
control them based on the classification using basic operators for
program construction. The idea of types is potentially fundamental in
many CS disciplines at least for this one reason: and this potential
has indeed been realised, by the study in the last three decades, as
the powerful and refined control of programs' behaviour which modern
theories of types give, as the examples you listed in your post amply
show.
* * *
I would explain thus if I was asked about the significance of the
notion of types by a CS researcher who is not in this field. I however
fear what I wrote above may not sound either pertinent or crisp enough
for the purpose you noted.
Best wishes,
kohei