Types in programming
Contents
Using types for safety against crashes and bugs
Types can be used to put helpful constraints on your programs.
Beside just preventing that one sticks together stuff that is not supposed to go together
there are some major guarantees that can be made.
One can guarantee purity of code. Which is practically relevant for many reasons.
First and foremost allowing one to treat code locally substitutably. Just like math.
See: Purely functional programming
One can guarantee totality of code. That involves:
– One can guarantee absence of undefined case branches (obviously practically relevant)
– All programs terminate (practically irrelevant as termination may take aeons of time) but ...
One can guarantee automatic timeout-abort and timeout-handling.
This (when properly utilized) basically allows one to have all remaining errors
being high level logical errors that are not caught by the type system.
Using types for context sensitive suggestions
Very useful. This can potentially make programming feel like a
drag and drop puzzle-game with the puzzle pieces pre-sorted
showing only the ones that would fit at ewhat one currently is looking at.
Dependent typing
In some cases it is desirable to have computing capabilities at the type level.
The result types can depend on the argument types. Thus dependent typing (I think).
- Size of lists, arrays, matrices, vectors, tensors, ...
- Computing with physical units (mass times speed gives impulse)
As all physical units can be represented via the SI units of kilograms, meters, and seconds
Resulting units can be calculates by simple arithmetic.
Using types for the automatic synthesis of programs
Types can be used to aid automatic synthesis of code.
Typically only for small code fragments as the space of possibilities for bigger code grows at least exponentially.
Probably more something for more advanced programmers writing (highly) generalized library code.
For bigger code fragments where the types do not uniquely determine the program
types could still be used to aid artificial intelligence in suggesting various code examples.
This will be for everyone.
Philosophical aspects
Acceptable over-blocking when types are used to enforced totality (or stronger)
Note that whenever one introduces totality (or stronger) via type system constraints
then one looses truing completeness of the language.
That is: There are always valid programs that would work and terminate
(or would within practical time-limit terminate) that are no longer possible (representable).
In fact almost all programs become blocked, but almost none of the practically relevant ones become blocked.
Similar to how there are much more irrational numbers than rational ones yet we know much more rational ones than irrational ones.
To make some (never all) of these inaccessible programs accessible again
the constraints from the type system need to be changed.
Possible interpretation:
Total (or stronger) constraints from the type system
make all code on the value level fully formally governed.
But the type level is still fully informal. No rules. Anything goes.
Shifting informality upwards
To make the type level formal too one might wish for something like types of types (aka kinds).
But then these types of types are informal. You see where this is going.
Types, kinds, sorts, ... an infinite tower of "universes". And ...
One can only ever shift the problem of informality upwards. Never get rid of it entirely.
(There's a relation to the halting problem and Russels paradox (~barbers paradox).)
Somewhere beyond the last formal level "there be dragons", "magic",
whatever your beliefs are you can put them there.
Practically shifting informality upwards is tremendously useful in the first step
and useful with quickly diminishing returns with any further step.
Only very few programming languages take even the second step.
The second step (kinds) is still quite useful but most languages
do not have sufficiently strong theoretical underpinnings to even try.
As doing interesting things at the type level and higher requires computational capability there
this is strongly related to dependent typing.
Related
- Typed holes
- Curry-Howard-Lambeck isomorphism – propositions as types
- Purely functional programming
- Programming languages
