Re: [Axiom-developer] [#263 ContinuedFraction returns incorrect types] static types

[Ralf Hemmecke]

On 02/06/2006 05:38 PM, Bill Page wrote:
> Changes 
> http://wiki.axiom-developer.org/263ContinuedFractionReturnsIncorrectTypes/diff
> --
> Ralf, do you think you could provide some example code that
> does this and actually works? I remain a little sceptical.
> --
> forwarded from http://wiki.axiom-developer.org/address@hidden

Maybe I should put that code somewhere on the AxiomWike (where?) so that
is is not forgotten inside the archive.

I did not bother to try to write it in SPAD. With Aldor it seemed so
much easier to me.

Bill, I hope you like it.

> I think Axiom's two-level type system is going to get in
> the way. Although it is true that types in Axiom are "first
> order objects" in the sense that we can assign them to variables
> etc., the kind of things that we can actually do with them is
> very limited. For example, I see no way in Axiom, SPAD or Aldor
> to have::
>
>   FRAC FRAC INT = FRAC INT
>
> since 'FRAC INT' is  static type and 'FRAC FRAC INT' is another
> static type.

Well the reason for not having equality is not that FRAC INT and
FRAC FRAC INT are different, but just the lac of a function "=" of the 
right type that does the right thing.

For frac.as below, one would need a function:

=: (Field, Field) -> Boolean

Note that Field is a category and not a domain.
The problem is that I have no idea how to implement such a function.
I even guess that at the moment the runtime system does not provide 
anything nice that could be used to check whether two domains are, in 
fact, the same. (Maybe Peter Broadbery knows a bit more about the 
internals.) In principle, however, I think that should be doable just by 
comparing two appropriate pointers.

> In Axiom there is no way to write a function which
> returns different types depending on it's parameters::
>
>   fType(x) ==
>      x=0 ==> Integer
>      Float
>
>   t:fType(1):=1.0
>
> because types like 'Integer' and 'Float' are not members of some
> domain in the same since in which '1' and '-1' are members of
> 'Integer'. And further there is no equality defined over types.

Clearly, a compiler would have to know
a) what is the type of x, and
b) what is the return type of fType.

The return type in that case could be figured out by the intersection of 
the signatures of the type of Integer (ie, its category Integer belongs 
to) and the type of Float.

But let's make things more concrete. Add the following definition
IDom(b: Boolean): IntegralDomain == {
        if b then MyInteger else MyRational
}
to the code below and also add

        j0: IDom false  := 1;
        j1: IDom true   := 1;
        
        stdout << "IDom false: " << j0 + j0 << newline;
        stdout << "IDom true : " << j1 + j1 << newline;

into the function "main". Then compile and run again.

You will see the output:

IDom false: (2)/(1)
IDom true : 2

But, of course, IDom(true) and IDom(false) have the same type, namely 
IntegralDomain. So, true, Axiom/Spad/Aldor does not let you return you 
something of different types. Well, there are dependent types... but 
that is another story.

The line

>   t:fType(1):=1.0

cannot work since fType(1) and Float are not the same. A compiler has to 
figure out a common return type for the function fType. And clearly, 
that will not be the same as the category of Float.

Even if one writes

MyInt: with {1: %} == Integer

MyInt and Integer are not the same since they belong to different 
categories. For example, there is no addition in MyInt.

Ralf


--------- FILE frac.as ---------------------------------------
-- Compile with
--   aldor -mno-mactext -fx -laldor frac.as
-- results in

--: "frac.as", line 51: Fraction(R: IntegralDomain): FractionField R == {
--:                     .........^
--: [L51 C10] #1 (Warning) Function returns a domain that might not be
constant (which may cause problems if it is used in a dependent type).

-- Ignore this warning.

-- Then running the program gives

--: Integer:   2
--: Rational:  (2)/(1)
--: Rational1: (2)/(1)
--: Rational2: ((2)/(1))/((1)/(1))

-- which shows that the domain constructor "Fraction" does not construct
-- another representation in case its argument is already a field.

#include "aldor"

define IntegralDomain: Category == OutputType with {
        0: %;
        1: %;
        +: (%, %) -> %;
        -: % -> %;
        *: (%, %) -> %;
}

define Field: Category == with {
        IntegralDomain;
        inv: % -> %;
}

define FractionField(R: IntegralDomain): Category == with {
        Field;
        numerator: % -> R;
        denominator: % -> R;
}

Fraction0(R: IntegralDomain): FractionField R == add {
        Rep == Record(num: R, den: R);
        import from Rep;
        0: % == per [0, 1];
        1: % == per [1, 1];
        numerator(x: %): R == rep(x).num;
        denominator(x: %): R == rep(x).den;
        -(x: %): % == per [- numerator x, denominator x];
        inv(x: %): % == per [denominator x, numerator x];
        (x: %) + (y: %): % == {
                n := numerator x * denominator y + denominator x * numerator y;
                d := denominator x * denominator y;
                per [n, d];
        }
        (x: %) * (y: %): % == {
                n := numerator x * numerator y;
                d := denominator x * denominator y;
                per [n, d];
        }
        (tw: TextWriter) << (x: %): TextWriter == {
                import from String;
                tw << "(" << numerator x << ")/(" << denominator x << ")";
        }
}
Fraction1(F: Field): FractionField F == F add {
        numerator(x: %): F == x pretend F;
        denominator(x: %): F == 1$F;
}

Fraction(R: IntegralDomain): FractionField R == {
        if R has Field then Fraction1(R pretend Field) else Fraction0 R;
}

MyInteger:   IntegralDomain == Integer add;
MyRational:  FractionField MyInteger  == Fraction  MyInteger;
MyRational1: FractionField MyRational == Fraction  MyRational;
MyRational2: FractionField MyRational == Fraction0 MyRational;

main(): () == {
        import from TextWriter, String, Character;
        i: MyInteger    := 1;
        r0: MyRational  := 1;
        r1: MyRational1 := 1;
        r2: MyRational2 := 1;
        stdout << "Integer:   " << i  + i  << newline;
        stdout << "Rational:  " << r0 + r0 << newline;
        stdout << "Rational1: " << r1 + r1 << newline;
        stdout << "Rational2: " << r2 + r2 << newline;
}

main();