Sat Mar 27 13:34:57 CET 2010

Computation (pattern matching) vs. types

Some more non-obvious obvious stuff (NOOS ??).  Ha! I have some NOOS
for you!

Types (in the Haskell sense) give finite, static meaning to your
program.  All the other stuff to know about a program is about
1. loops (recursion) and 2. making decisions (conditionals) which are
necessary to get out of loops and produce terminating computations.

One of the things that really struck me when starting to use typed
programming languages is that types abstract away `if' statements.
You don't see their effect in a function type.  A program looks a lot
simpler when you can abstract away diverging control.

A bit less obvious to me at that time was that they also abstract away
recursion/loops.  You don't see in the types that a function recurses
and so possibly doesn't terminate.

In fact, that is what a type system is: what you can know about a
program (its structure) before running it.  Knowing its full behaviour
is `undecidable'; it can't be captured before running:

    - "infiniteness" comes from recursive functions acting on
      recursive data types = passing through the same control point
      more than once.

    - "decisions" come from conditionals like pattern matching =
      having run-time state influence future control points.

So "what happens inside types" can in general not be determined by the
type system.  Again, to turn this around, the type system says some
limitied thing about what happens at run time.  This limited thing --
the program's static structure -- is the "type".