Difference between revisions of "Types in programming"

Latest revision as of 12:47, 11 July 2023

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.

For a view examples (using Annotated lambda diagrams as graphical code projection)
see: Annotated lambda diagram mockups

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 only
the three basic 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
• Purely functional programming
• Programming languages
• Curry-Howard-Lambeck isomorphism – propositions as types
• Annotated lambda diagram mockups

External links

Most links here are to Wikipedia.

• Parametric polymorphism (uniform behaviour for all argument types - e.g. map :: (a -> b) -> [a] -> [b] where a and b may be anything)
• Ad hoc polymorphism (nonuniform behavior, finite number of cases, name overloading)
• Type class ... instances of type classes define ad hoc polymorphic behaviour
• More generally: Polymorphism (computer science)

• Type family
• Kind (type theory)

General theory

Dimensions of extendability of type systems:

• Lambda cube
•  ?? Pure type system

Product types and sum types: Cartesian closed category
Related: Compiling to categories (Conal Elliott)

• Calculus of constructions
• Universe (mathematics)
• Structure_(mathematical_logic)#Many-sorted_structures

• Category theory
• Type theory & Category:Type_theory
• Homotopy type theory

Dependent typing

• https://en.wikipedia.org/wiki/Dependent_type

• https://thelittletyper.com/ – by David Thrane Christiansen and Daniel P. Friedman
• The Pie Reference https://docs.racket-lang.org/pie/
• https://github.com/the-little-typer/pie

Gradual typing

• https://en.wikipedia.org/wiki/Gradual_typing

Effects

• Effect system (algebraic effects, abilities)
• Functional reactive programming
  Related: Denotative continuous-time programming (Conal Elliott)
• Monad transformers
  Known problem: These are not well composable, introduce arbitrary nesting order, and
  thus introduce necessity of nested lifting. Incidental complexity.