Lambda (was: Refactoring in Tunes)

[Laurent Martelli]

>>>>> "Fare" == Francois-Rene Rideau <fare@tunes.org> writes:

  Fare> On Wed, Jan 19, 2000 at 06:19:47PM -0800, btanksley@hifn.com
  Fare> wrote:
  >> I see typing as just a convenient way of having the compiler
  >> catch a very common class of stupid typos.

  Fare> It's more than that. It's a form of passing programming
  Fare> contracts.  Between the programmer and the machine; among
  Fare> programmers.  Contracts that are automatically enforced by the
  Fare> system.

To me, the contract is the program. We usually feel the need to use
types because the languages we use are not capable of expressing what
we want the way we want.

Let's take a simple program :

        f(x) {
          return x+2;
        }

It's clear that f(x) = x + 2. We don't have to prove this because the
code is written in a way that matches exactly what we want.

But if you take a more complicated program that computes the shortest
path in a valuated graph, you feel the need to prove that it's correct
the algorithm does not ressemble what you want (the returned path is
such that there exists no other path whose length is shorter).

The solution is to be able to build an interpreter for any kind of
language we think is suitable to express our needs. If we want to
express numerical operations, we should have a language for that. If
we want to do operationnal research, then we should have a language
for that. 

In fact, I think we should have an infinity of languages, which are in
fact all built on one language. But having *two* languages (HLL and
LLL) seems silly to me. One or an infinity, but not two. 

-- 
Laurent Martelli
martelli@iie.cnam.fr