[TYPES] Declarative vs imperative

[Bram Geron]

On 04/23/2013 02:52 AM, Mark Janssen wrote:
> What machines do you use, where a C compiler fills in the gaps of your
> source code? Quantum computers?

Well, the C standard does not fully define the meaning of all C
programs, e.g. when a program divides by zero. The actual program output
may depend on the compiler options. The machine code is usually strictly
defined, so in a sense the C compiler fills in gaps. The LLVM people
have an interesting series of blog posts on this:
http://blog.llvm.org/2011/05/what-every-c-programmer-should-know.html .

In an attempt to better define declarative vs. imperative, or
specification vs. implementation, it may be valuable to distinguish
these categories of specification:

1. Functional specification
2. Asymptotic running time
3a. Asymptotic memory use
3b. Memory use up to a factor 2
4. Register use and instruction selection

This list is by no means complete. Categories 2,3a are typically upper
bounds: if the compiler can optimize stack usage from O(n) to O(1) by
eliminating tail calls, that's fine but optional; the compiler does, in
fact, compile according to specification. Furthermore, category 1 is
typically a lower bound: the compiler may make undefined behavior defined.

In my view, programs in these languages are specifications of these
categories:

ASP/SAT: 1
Prolog: 1, 2
Haskell: 1, 2, 3a
Java: 1, 2, 3a
C: 1, 2, 3b
Assembly: 1, 2, 3, 3a, 4

Typically, the more "declarative" languages specify less categories.

Apart from this numeric "axis", it may be interesting to regard the
connection between how programs in a language correspond to the
specification. For instance, programs in C explicitly have to free heap
memory. In Java, objects are freed when they can no longer be reached
from the stack. In Haskell, I guess thunks outside of global variables
are freed when they can no longer be reached from the active thunk, but
it is harder to make a mental model of this.

One could thus argue that programs in "declarative" languages correspond
closely to the induced functional spec, but loosely to the induced
extrafunctional spec. Reversely, programs in "imperative" languages
correspond closely to the extrafunctional spec, but more loosely to the
functional spec.

Cheers, Bram