BTW, if X1 := Union(X,"failed") and X2 := Union(X1,"failed"), where in
current FriCAS is it specified that failed$X1 is different from failed$X2?
It probably is, but only by the general rule that no two domain have
elements in common. Even not NNI and Integer. We need coerce/retract (or
some special compiler knowledge in order to claim that 1$NNI is an
Integer. Internally they may have the same representation, but that does
not count on the surface.
Ralf
On 10/05/2017 07:09 AM, Ralf Hemmecke wrote:
> On 10/05/2017 02:32 AM, Bill Page wrote:
>>> I think current situation is a good compromise. We can
>>> say in documentation that all instances of Maybe share
>>> a common value of failed(), and nested usage of Maybe
>>> is not recommended, Maybe should not be used as Rep
>>> itself but can be part of Rep. Do you agree?
>
>> I value correctness much more than performance except in the most
>> extreme and special cases.
>
> There is no general "correctness". Code only behaves correctly
>
> with respect to a certain specification.
>
> As Qian said, the specification would claim Maybe to a very special
> case. There is a fixed value "failed()" and that is global over all
> domains and not element of any other domain than Maybe(X). Then Maybe(X)
> represensts
>
> X \cup \{failed()\}
>
> With that, of course, Maybe(Maybe(X)) must behave like Maybe(X). I don't
> see any (big) problem with that, just that Maybe(X) is not the same as
> extending the domain by some new element, but it stands for "adding
> failed() to the domain". I don't see any problem with "correctness".
>
> However, then I would really opt for another name. Otherwise one might
> think that Maybe behaves according to the type equation
>
> FX = 1 + X
>
> (see https://wiki.haskell.org/Maybe). Actually, I don't know whether
> "Nothing" in Haskell is a global value, but I guess, it it not.
>
> Ralf
>
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to fricas-devel+unsubscr...@googlegroups.com.
To post to this group, send email to fricas-devel@googlegroups.com.
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.
