What is a type error?

[Chris Smith]

Joachim Durchholz <jo at durchholz.org> wrote:
> OTOH, isn't that the grail that many people have been searching for: 
> programming by simply declaring the results that they want to see?

Possibly.

> No, FPLs are actually just that: compilable postconditions.

This seems to me a bit misleading.  Perhaps someone will explain why I 
should stop thinking this way; but currently I classify statements like 
this in the "well, sort of" slot of my mind.  If functional programming 
were really just compilable postconditions, then functional programmers 
would be able to skip a good bit of stuff that they really can't.  For 
example, time and space complexity of code is still entirely relevant 
for functional programming.  I can't simply write:

(define fib
  (lambda (x) (if (< x 2) 1 (+ (fib (- x 1)) (fib (- x 2))))))

and expect the compiler to create an efficient algorithm for me.  This 
is true even though the above is (the LISP transcription of) the most 
natural way to describe the fibonacci sequence from a mathematical 
standpoint.  It still runs in exponential time, and it still matters 
that it runs in exponential time; and LISP programmers adapt their so-
called declarative code to improve time bounds all the time.  This makes 
it harder for me to call it declarative (or "compilable postconditions") 
and feel entirely honest.

(Yes, I realize that the above could be optimized in a language that 
does normal order evaluation with common subexpression elimination. and 
become linear-time.  However, that's not true of algorithms in general.  
It is not the case that all that's needed to find an efficient algorithm 
for something is to plug it into a Haskell compiler and observe what 
happens.  Or, if that is the case, there are a few CS professors I know 
who would be quite interested in hearing so.)

> Computability issues aren't more or less a factor than with other kinds 
> of compilers: they do limit what you can do, but these limits are loose 
> enough that you can do really useful stuff within them (in particular, 
> express all algorithms).

Is it really consistent to say that postconditions allow you to express 
algorithms?

-- 
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation