My dream would actually be something like
/: (%, NonZero %) -> %
Which would mean that the zero test would be at the time when one has to
coerce an element from % to NonZero(%). An implementation of / would be
certain that it never gets 0 as its second argument.
This is fine if we can statically prove NonZero. But typically
this has to be done by runtime test. And then I prefer test
inside '/'. Namely, if test is done in other places then it
is erorr prone or at least leads to code bloat (if typesystem
automatically introduces checks). And if NonZero(%) is a
real type, then it may be quite hard to optimize space usage
by moving check into '/'. And at philosopical level, why
is x::NonZero(Integer) raising error better than '/' raising
error?
The type system is not supposed to do any checking. This NonZero is
basically like CommutativeRing. So to state a definition.
NonZeroCat: Category == with {}
NonZero(T: with zero?: % -> Boolean): NonZeroCat with {
nonZero: T -> %
coerce: % -> T
} == add {
Rep == T
nonZero(t: T): % == {zero? t => throw ZeroException; per t}
coerce(x: %): T == rep x;
}
Since T and NonZero(T) have the same representation, I don't understand
what you mean by space usage.
And why would I (philosophically) move the test out of any function?
Because one could imagine something like.
r: Integer := f(...);
n := r :: NonZero(Integer);
[k/n for k in 1..10000];
Would a compiler be able to remove the repeated zero? checks if this
check were insided the /-function?
Of course the coercion itself is a runtime check, but one can be sure at
compile time that n is non-zero.
Except for the last part you describe Java exceptions. The problem
is that in Java looking at API you can not say if exception is
really raised or that it is specified just to satisfy formal
rules. Consider:
y := x^2 + 1
z := x/y
in real domains exception is impossible, but normal typesystem
will force you to say that this snippet may raise DivisionByZero
exception.
I agree that it would be counterproductive if the type system tries to
stupidly follow rules and cannot be overruled by means of other proofs.
As for the above, one would have to wrap that with a
try...catch DivisionByZero
in order to have the surrounding function definition freed from
declaring that it may raise DivisionByZero.
All would be well, if we could reason about the program code. Ehm, not
"we", but a "automated proofer", of course. In fact, I would already be
happy if such simple cases as your code chunk above could be dealt with
and avoid the try...catch construction. On the other hand, this
try..catch also is some hint for other people that read the code and
want to figure out why the respective function will never end up in a
DivisionByZero.
Unfortunately, I have no idea how much code is needed for such a
try...catch. What time is additionally spend to run code inside
try..catch if this code does not raise an exception, i.e. what is the
overhead of try...catch?
3) Since exceptions are part of API there are serious limitations
which functions may be passed as arguments. Think about
functions like 'map': in 'map(f, l)' normally 'map' itself does
not raise any exceptions, but it calls 'f' and it is useful to
have 'f' which may raise exceptions.
Good example. In Aldor you would probably define
map: (X -> Y, List X) -> List Y
without any "throw" clause. According to AUG 11.4, the function may
raise any exception.
That is somehow hiding all the possible exceptions that might be thrown,
but in such situations, I'd find that more practical than carrying
around all the specific listings of exceptions.
I don't know whether the following would be possible...
map: E -> (X -> Y throw E, List X) -> List Y throw E
where E would be a tuple of possible exceptions than can be thrown.
But then one would have to call
map(DivisionByZero)(a +-> 1/a, somelist).
Looks a bit too cumbersome to me at the moment.
Ralf
--
You received this message because you are subscribed to the Google Groups "FriCAS -
computer algebra system" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en.
