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

Reply via email to