[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] [#263 ContinuedFraction returns incorrect types] s
From: |
Ralf Hemmecke |
Subject: |
Re: [Axiom-developer] [#263 ContinuedFraction returns incorrect types] static types |
Date: |
Tue, 07 Feb 2006 02:23:28 +0100 |
User-agent: |
Thunderbird 1.5 (X11/20051201) |
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();