View source for Types in programming


== 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 <br>
there are some major guarantees that can be made.

One can guarantee '''purity of code.''' Which is practically relevant for many reasons. <br>
First and foremost allowing one to treat code locally substitutably. Just like math. <br>
See: [[Purely functional programming]]

One can guarantee totality of code. That involves: <br>
– One can guarantee '''absence of undefined case branches''' (obviously practically relevant) <br>
– 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 <br>
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 <br>
drag and drop puzzle-game with the puzzle pieces pre-sorted <br>
showing only the ones that would fit at ewhat one currently is looking at.

For a view examples (using [[Annotated lambda diagram]]s as graphical code projection) <br>
see: '''[[Annotated lambda diagram mockups]]'''

== Dependent typing ==

In some cases it is desirable to have computing capabilities at the type level. <br>
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 <br>
the three basic SI units of kilograms, meters, and seconds <br>
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. <br>
Typically only for small code fragments as the space of possibilities for bigger code grows at least exponentially. <br>
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 <br>
types could still be used to aid artificial intelligence in suggesting various code examples. <br>
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 <br>
then one looses truing completeness of the language. <br>
That is: There are always valid programs that would work and terminate <br>
(or would within practical time-limit terminate) that are no longer possible (representable). <br>

<small>In fact almost all programs become blocked, but almost none of the practically relevant ones become blocked. </small><br>
<small>Similar to how there are much more irrational numbers than rational ones yet we know much more rational ones than irrational ones. </small><br>

To make some (never all) of these inaccessible programs accessible again <br>
the constraints from the type system need to be changed.

Possible interpretation: <br>
Total (or stronger) constraints from the type system <br> 
make all code on the value level fully formally governed. <br>
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). <br>
But then these types of types are informal. You see where this is going. <br>
Types, kinds, sorts, ... an infinite tower of "universes". And ...<br>
One can only ever shift the problem of informality upwards. Never get rid of it entirely. <br>
<small>(There's a relation to the halting problem and Russels paradox (~barbers paradox).)</small>

Somewhere beyond the last formal level "there be dragons", "magic", <br>
whatever your beliefs are you can put them there.

'''Practically''' shifting informality upwards is tremendously useful in the first step <br>
and useful with quickly diminishing returns with any further step. <br>
Only very few programming languages take even the second step. <br>
The second step (kinds) is still quite useful but most languages <br>
do not have sufficiently strong theoretical underpinnings to even try.

As doing interesting things at the type level and higher requires computational capability there <br>
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.
----
* [https://en.wikipedia.org/wiki/Parametric_polymorphism Parametric polymorphism] (uniform behaviour for all argument types - e.g. '''map :: (a -> b) -> [a] -> [b]''' where a and b may be anything)
* [https://en.wikipedia.org/wiki/Ad_hoc_polymorphism Ad hoc polymorphism] (nonuniform behavior, finite number of cases, name overloading)
* [https://en.wikipedia.org/wiki/Type_class Type class] ... instances of type classes define ad hoc polymorphic behaviour
* More generally: [https://en.wikipedia.org/wiki/Polymorphism_(computer_science) Polymorphism (computer science)]
----
* [https://en.wikipedia.org/wiki/Type_family Type family]
* [https://en.wikipedia.org/wiki/Kind_(type_theory) Kind (type theory)]

=== General theory ===

'''Dimensions of extendability of type systems:''' <br>
* [https://en.wikipedia.org/wiki/Lambda_cube Lambda cube]
* ?? [https://en.wikipedia.org/wiki/Pure_type_system Pure type system]
----
Product types and sum types: [https://en.wikipedia.org/wiki/Cartesian_closed_category Cartesian closed category] <br>
Related: '''[[Compiling to categories (Conal Elliott)]]'''
----
* [https://en.wikipedia.org/wiki/Calculus_of_constructions Calculus of constructions]
* [https://en.wikipedia.org/wiki/Universe_(mathematics) Universe (mathematics)] 
* [https://en.wikipedia.org/wiki/Structure_(mathematical_logic)#Many-sorted_structures Structure_(mathematical_logic)#Many-sorted_structures]
----
* [https://en.wikipedia.org/wiki/Category_theory Category theory]
* [https://en.wikipedia.org/wiki/Type_theory Type theory] & [https://en.wikipedia.org/wiki/Category:Type_theory Category:Type_theory]
* [https://en.wikipedia.org/wiki/Homotopy_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 === 

* [https://en.wikipedia.org/wiki/Effect_system Effect system] (algebraic effects, abilities)
* [https://en.wikipedia.org/wiki/Functional_reactive_programming Functional reactive programming] <br>Related: [[Denotative continuous-time programming (Conal Elliott)]]
* [https://en.wikipedia.org/wiki/Monad_transformer Monad transformers] <br> Known problem: These are not well composable, introduce arbitrary nesting order, and <br>thus introduce necessity of nested lifting. Incidental complexity.

[[Category:Programming]]