Re: [Axiom-developer] Axisp news

[Stephen Wilson]

Martin Rubey <address@hidden> writes:
> Dear Stephen,
> 
> many thanks for your detailed answer.  I must admit however, that I dislike
> your idea writing
> 
>    D(P : Polynomial (R : Ring)) : ... == ...
> 
> for
> 
>    D(R : Ring, P : Polynomial R) : ... == ...
> 
> Isn't this just syntactic sugar?  My feeling (!) is that this will pose more
> questions than answers.  Enforcing case sensitivity on values, domains and
> categories also does not look very appealing to me, sorry.

It may be syntactic sugar for the sake of a function definition, but it
implies a handling of types which diverges from how things are
currently done.

Case sensitivity is not a requirement for this to work.  For example,
you could just as well have a binding operator which matches values to
domains, and another which matches domains to categories

Big difference is that with a parametrized type, the parametrization
forms a part of the `public interface' to the type.  No
domain/category should be allowed to `hide' their parametrization,
nor should they ever need to explicitly `export' them, as you
mentioned RectangularMatrixCategory does.

> In any case, I'd like to point you again to Christian Aistleitner, who seems 
> to
> have thought a lot about issues about Aldor semantics.
> 
> To look at OBJ is probably a good idea, though.
> 
> > Another shortcoming relates to `first class types'.  One can generate a new
> > type at run time, but there is no elegant mechanism in place to recover the
> > exact type.  Consider:
> > 
> >           mkMod(n : Integer) : IntegerMod( ? ) ==
> >                                    IntegerMod(compute(n))
> 
> I'm not absolutely sure what you mean here, since IntegerMod(compute(n)) is
> certainly not of type IntegerMod( ? ), no matter what the ? will be.
> 

Ah, sorry. Should have been something like:

       mkMod(n : Integer) : IntegerMod( ? ) ==
                                foo(n)::IntegerMod(compute(n))


The point is that types can be instantiated dynamically,  but there is
no way to state what the type is outside the dynamic context.  This is
compounded by the fact that, in Aldor, when you write IntegerMod(n +
1), to compare that type with any other the test for equality basicly
boils down to comparison of (typed) AST's.  Clearly, that is not
sufficient, as there is no way to `lift' those AST's from the context
of a callee to a caller. 

The notion of pattern matching over a parametrized domain/category
would allow type variables to be made abstract, and then reified
according to some (hopefully) sound rules.

> > In addition, IIRC (its been a while since I played with aldor), there
> > are real problems with how constants are treated.  In short, they are
> > not really constants.  I remeber seeing code such as:
> > 
> >         add!(r: %, s: %, t: %) : % == 
> >                  if one? % or zero? % then s + t else ...
> 
> I could not find code like that -- apart from the typo, you probably meant
> 
>          add!(r: %, s: %, t: %) : % == 
>                   if one? r or zero? r then s + t else ...

Again, sorry for the typo.  Your rendition is exactly what I meant.

Im not sure why you could not find code like that. I took a quick
look, and found a few examples in about a minute.  I also probably
found a bug too.  Check alg_sup0 in libalgebra and sal_intgmp in
libaldor.  Note that sal_fltgmp does not consistently check.  You may
want to test that calling add!(0, 1) on a gmp float actually changes
the value of `0' to `1'.  (Note that I could be wrong, I dont have
Aldor so I cant check myself). 

> > To work around the fact that the destructive add would modify the constants
> > `0' or `1', leading to predictable surprises.  The imperative aspect of the
> > language needs to be more carefully considered, IMHO, especially w.r.t the
> > semantics of a types parametrized over (possibly mutable) values.
> 
> Yes, constants may contain mutable data.  But that's just as in other
> languages.  It is true that you can say
> 
> l: List Integer == [1,2,3];
> l.1 := 4;
> 
> but in my opinion, you are not really modifying l, but rather l.1, and that's 
> a
> different story.

Yes.  I understand the distinction.  The issue is how this plays with
a type parametrized over a mutable value.  There are three
alternatives that I see off hand:
    
      1) Dont worry about it, but make sure its written down that the
         consequences are undefined if an object which is used in type
         context is subsequently modified.

      2) At the level of implementation, ensure the property of
         `constantness' is checked at runtime before destructive
         update.

      3) Inject the notion of `constantness' into the type system.

I do not consider either of the above ideal, but option 1) is probably
the most pragmatic.  Option 2) gives safety but at some (small)
runtime cost. Option 3) is just there for its own sake.

> > > * certain difficulties transforming Tuples
> > 
> > I assume your talking about the issues raised in the article I mentioned
> > above?
> 
> possibly, but Ralf knows better.  Maybe you want to join our discussion on how
> to implement multisort species in Aldor?  There, we are pushing the limits of
> Aldor, I guess.  Also, the parser and domain generator I wrote shows some
> features one may want to have.

I am afraid I would not be able to contribute much to that
discussion.  I also have few free cycles to spare, unfortunately.

> 
> Martin


Thanks,
Steve