Sun Aug 30 19:18:57 CEST 2009

Dynamic vs. Static Types

I've been reading up a bit about logic and type systems.  This is
seriously complex stuff, in the sense that there are a great number of
different ways to approach static structure.  If you compare this to
the simplicity of dynamic typing (predicates / set membership without
static structure) I sometimes if people that use this heavy machinery
get anything done at all.

I do see that there can be a lot of payback if your applications are
complex, but exhibit some arbitrary but well-defined static structure.
Heavy types allow some of the correctness burdon carried by the
compiler, at the expense of 5+ years graduate studies of the
programmers :)

It seems that typing is about defying undecidability.  What you really
want is the machine to write your program for you.  Since that's quite
difficult, maybe you scale down expectations and ask the machine to at
least tell you that what you just did is not what you really intended.

When this ``intention'' can be codified in a structure that doesn't
lead to undecidable problems when trying to interpret it, you can
offload some of the thinking to the machine.  For dependent types this
can be taken quite far: as long as you (the programmer) can help the
verification system to solve the undecidable part of the problem
(provide a proof for certain parts) then it can use this to check the