Re: [Axiom-developer] B#

[Hans Peter Würmli]

On Sunday 20 November 2005 17.52, you wrote:
>
> I wonder if your colleague who said: "strong typing is for the
> weak of minds" really knows what "types" in computer programming

To be fair to him, he quoted another colleagues in the US who said that to 
him. The full quote went something like: "Weak typing is for the strong minds 
and ..." and reference in the discussion was made to C and Pascal.

> I think that a lot of work has already been done in Axiom to
> support the concept of a USER algebra domain - specifically in
> the Expression constructor. Expression implements many of the
> ideas that Jenks and Trager assume for the type USER. The other
> domain in the Axiom interpreter that implements some of these
> ideas is ANY. I think of the type USER as sort of a cross
> between these two.

Noted. But even if, it seems to be difficult to continue in the same spirit.

> > Let me give some examples of what I would consider nice
> > syntactic sugar, and it must be syntactic sugar as the
> > evaluation of any expression is ultimately extremely simple
> > as explained at the end of section 5 of the "Axiom as
> > Scratchpad" article.
> >
> > 1) TeX-like conventions: being able to define, say, variables
> > as x_{i,j} looks very handy. One should actually go further
> > and allow type annotations, like
> >
> > x_{i:NNI,j:PI}:POLY INT,
> >
> > or even further
>
> I think you are mixing sugar with semantics here. It does not
> make sense to me to associate types with superscirpts and
> subscripts if these are just symbols. But if they are not
> symbols then we need to decide what the use of subscript
> means, e.g. if x is a matrix then the subscripts might
> denote a reference to an element of a matrix. It is not
> clear to me what meaning might be associated with your
> example.

Let me explain, why I think it's a syntax problem: 

If a mathematician writes a_i, he thinks of a function 

a: Index -> Something, i |-> a(i).

Further, sometimes he writes sloppily f(x) for a function (domain and range to 
be guessed), some other times f_x. So if B# proposes TeX like conventions, it 
proposes an alternative syntax for Expressions (denoting "functions") which 
in the current implementation I think are called "kernel", having the form 
"f(x)", but could also be denoted with f_x, or, if it is a function of two 
variables, f_{x,y}.

So the meaning is: f_x `equal` f(x), or, f_{x,y} `equal` f(x,y).

I guess that the internal representation would coincide, whereas the 
"OutputForm" would differ.

The second form, which does not seem to be proposed, but that would equally 
well make sense are type annotations, which would express the intended type, 
i.e.

f_{x:INT}:NNI `equal` f: (x:INT) -> NNI `equal` f(x: INT):NNI

(where I am unsure whether the middle and last forms exist as a declaration). 
If anything this would probably help disambiguate Expressions.

> > and allow "operators" as syntactic elements, like defining a
> > few variables as (or the sum example in "Afterthoughts, ...")
> >
> > for i in 0..5 repeat x_i:POLY INT
>
> As I understand it, this syntax actually denotes 6 names,
> x_0 x_1 ... x_5 all of type POLY INT, is that right?

Yes, that is what would be meant, and I tried, also with declaring the 
variables global (i.e. free), but it did not seem to work.

> > This actually seems to be nothing else than polymorphism of
> > the function "for", if - as the manuals claim - types are
> > first class citizens.

> Could you explain how you think of "for" as a function in this
> example?

I didn't think much about this one, but assumed that a "for" would correspond 
to a construct with operational semantics, "for" being defined as a 
recursively defined Monad binder.

> > 2) Afterthoughts: if "==" generally would point to a rewrite
> > rule then exending eval to an eval ( expr, List 'Rewrite Rules' )
> > would semantically be the same as the "afterthoughts". It looks
> > to me that this is the regular evaluation mechanism of any
> > functional programming language.
>
> Could you please explain this a little more. I do not think
> of == as involving any type of evaluation.

I used the suggestion in the "Axiom as Scratchpad" paper to read "==" as 
rewrite operator. See the example in "Afterthoughts". It immediately appealed 
to me though, because functions in Axiom as well as in Haskell are defined 
that way, the left side representing the name and argument(s) and the right 
side the body of a (typed) lambda, where the body "evaluated" with further 
rewrite rules producing the value of the right type. Actually, I played a 
little bit with the idea to use the Axiom == in this way, but it didn't 
really work.

My question would be, to what extent the current "="-equation sign in Equation 
expressions serves that purpose and whether "=" could be overloaded?

Does this answer your question or did you mind my use of the term "eval"?

> > (Currently an expression like x==t has the type Void; I wonder
> > what would happen if this construct came under programming
> > control.)
>
> What type would you suggest?

RewriteRule PatternType BodyType

(PatternType and BodyType are inventions for the purpose of this email.)

> Axiom supports currying of functions. You might recall some
> discussion between myself and William Sit about this. 

I had seen it but no time at the time to follow it.

Regards, H.P.