On Thu, Jul 17, 2008 at 2:47 AM, Ralf Hemmecke <[EMAIL PROTECTED]> wrote: >>>> The behaviour is controlled by $useIntegerSubDomain. >>>> If you like dpeendent types you should like it! >>> >>> Why do you say that has to do with dependent types? >> >> well, clearly the behaviour of the interpreter is that the type of the >> result >> in this case has to depend on the value of the result, not the type >> recorded by >> the domain of computation. > > Aha, but I think, I would not be able to express that in SPAD (or Aldor).
I agree, but Spad or Aldor do not exhaust the space of conceivable dependent types :-) > If > I simply say > > /: (Integer, Integer) -> Union(Integer, Fraction Integer) > > I don't think, I would call the type of / a dependent type even with the > semantics that the result is Integer if the denominator of the fraction is > 1. No, It isn't. But I would think /: (n: Integer, m: Integer) -> effectiveTypeOf(n/m) where effectiveTypeOf is a fictitious type operator that returns the effective type of the operation, would be. But I think the whole question is ill-posed. > > Interesting, interesting... > > Ralf > ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel