RE: Lambda (was: Refactoring in Tunes)

> From: Laurent Martelli [mailto:martelli@xxxxxxxxxxx]
> Subject: Re: Lambda (was: Refactoring in Tunes)

> >>>>> "billy" == btanksley  <btanksley@xxxxxxxx> writes:

>   >> My point is that those annotations are not needed to run the
>   >> code, so a code evaluator should not be required to understand
>   >> them. If annotations are included in the code, it's hard to
>   >> commnicate your code to someone whose system does not understand
>   >> annotations, or understands another type of anotations.

>   billy> How many types of annotations do we need?  I'm only
>   billy> suggesting one -- type annotations.  Very simple.  Easy to
>   billy> write.  

> Things are always simple at the beginning. But they don't usually
> remain simple very long. We start requiring very small things which
> may have no importance at the time we start requiring them, and a few
> years later, we realize we've just another bloatware.

But this does have some importance -- if you want typechecking, you need
these annotations.  If you don't want typechecking but do want to read the
code, these annotations follow loosely the Forth conventions for stack
comments, and so provide useful information to authors and readers.

> It may be useful
> not to understand annotations in minimalist embeded system where
> resources are scarce and expensive.

True.  On those systems typechecking will also have to be disabled, since
the annotations are either crucial to typechecking or merely helpful to
typechecking.

>   billy> If your system doesn't understand them it's BROKEN.  If your
>   billy> system requires an annotation where I don't have one it's
>   billy> also broken.

> In oher words, your system is correct, and mine is broken just because
> if different from yours ? :-)

Yes.  Just as broken as if it didn't understand the annotation which says
"the following name is the title of a new definition."  Just as broken as a
C system would be if it didn't understand the keyword 'int' when used in the
declaration of a parameter.

>   >> Annotations are like a style sheet, it just allow *some* kind of
>   >> reader to *better* manipulate some objects. There can be many
>   >> different annotations : params type, params names ... That's what
>   >> I'm trying to say in my paper on separation of concerns : if it's
>   >> not needed, don't require it.

>   billy> But it's _not_ required unless it _is_ needed.  

> I can't see where it could be neeeded. Do you have an example ?

>   billy> Have you ever used ML?  

> No.

ML functions have one and only one type.  However, ML's infix operators are
overloaded, and thus textually ambiguous.  Thus,

define square x :- x*x;

is of ambiguous type, and the compiler will refuse to accept it (is it float
or int?).  The solution is simple: the programmer provides a type annotation
at any point in the program where it helps.  For example, this:

define square:(int->int) x :- x*x;
define square x:int :- x*x;
define square x :- x*x:int;
define square x :- (x*x):int;

(I think caml may have the same characteristics, by the way.  I don't know,
having never used caml.)

Of course, the oddity here is the result of what I would consider a design
mistake -- overloading is a strange action in a type-inferenced language,
doubly so when you realise that in spite of the overloading you still have
to specify which version of the function you're going to use.  Perhaps a
language without overloading would not require typechecking.

>   billy> There, type annotations are often needed.  Yet it's always
>   billy> legal to use a type annotation -- unless, of course, your
>   billy> function cannot possibly produce that type.  In that case,
>   billy> you get an error, because you certainly made a mistake.



>   >> Anyway, all this does not prevent anyone to build a frontend that
>   >> integrates annotations with the code itself.

>   billy> But that makes everyone's life SO much harder.  

> I think that it remains to be seen. Make a frontend is not very
> difficult, and once it's done, it's done.

The frontend's no problem; no doubt it might be convenient under my system
to have a frontend which could do the inverse: visually stripped out type
annotations which were present in the source.

I don't understand the seperation, though.  Why?

>   billy> I don't understand why you're suggesting it.

> I think that separation of concerns is a very good principle. 

Drinking water is a good principle, too.  But that doesn't mean I do it
instead of designing a language.

> Proving
> that some code has some properties should not be mixed with
> interpreting that code.

But nobody's proving anything about the code -- these type annotations are
used to help the programmer write to the interface, and allow the compiler
to do typechecking.

I don't feel good about splitting these things, but would an acceptable
compromise be a C-style header file?  You lose a LOT of power that way
(since you can't place the annotations anywhere in the source), but at least
you get to document the interfaces.  And if you really want to place the
annotation in the middle of a definition, Joy and Forth make it trivial to
factor that part of the definition into a seperate word which can then have
its own interface.

> Laurent Martelli

-Billy