But the problem is deeper: do we really want to insist that every
finction is total (and use someting like Union(X, "failed") to turn
partial functions into total ones)?

At least I did not say so. And I consider a function with signature

  /: (%, %) -> Union(%, "failed")

as very impractical.

If not where to draw the line?  I personally am convinced that
functions should always return correct results (that is returning
garbage is not acceptable).

So we agree. All I want is to let the implementation respect the
interface. If the interface says that the result of division by zero is
undefined, then the implementation can return whatever it wants. It
could even crash the computer.

Where to draw the line is actually not a big issue, if there were a sane
exception system. Then it would be possible to catch errors of certain
type and let other errors be handled by functions higher in the call stack.

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.

I don't yet know whether that makes much sense. I would rather like that
there were a way to specify logical formulae that I can connect to the
type system.

It seems that you want a category, say 'NoRuntimeErrorPossible'
meaning that no opeation will raise errors and you want that every
(or most) domains have this category.

No, that's not my intent. All I want is that if the function raises an
exception it should be clear statically (at compile time) under which
conditions such an exception is raised (like DivisionByZero). And these
conditions are part of the interface of the function, i.e. its API. And
it would be clear which of the many exceptions is raised when.

Of course there might be other exceptions that you cannot foresee, like
defective memory chips.

Again, allowing partial functions means that we can use type system
in situations that otherwise would be hard to handle in typed way.

I agree that in some situations one has to be pragmatic, but still, my
goal goes to move as much information as possible to the type system.
(See the NonZero above.)

BTW: Java tries to "control" exceptions via type system, and this is
widely regarded as a failure.

What exactly is the failure? That there is a hierarchy of exceptions?

So good solution to problem of partial functions would be welcome,

Right. Currently, I would require that the specification is clear, but allow functions that may raise exceptions (or "error" in current SPAD)

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.

Reply via email to