RE: Promotion of bare decorations & comparisons

["Nathan T. Hayes" <nh@xxxxxxxxxxxxxxxxx>]

Michel Hack wrote: 
> Nate wrote (assuming a threshold of at least "dac"):
> >    [1,2] \subseteq floor([5,6])
> >        = [1,2] \subseteq ([5,6],def) // decorated result
> >        = [1,2] \subseteq def         // compress decorated result
> >                                         (throw away interval part)
> >        = [1,2] \subseteq Entire      // promote def to Entire for
comparison
> >        = true
> >
> >That is a false positive, no?
> 
> Compressed intervals have to be used carefully, in a context where they
> make sense, namely arithmetic expressions.  The promotion rules are there
> to complete the picture, but programs have to be written to take these
> into account.
> 
> > IMO, it is much better to have the bare decoration promote to Empty
> > to avoid this situation.
> 
> You can construct an equally silly example with that alternative:
>      [1,2] \subseteq floor([0,6])
>          ...
>          = [1,2] \subseteq Empty
>          = false
> 
> Now we have a false negative.

I don't agree it is a false negative.

Compressing the decorated interval ([0,6],def) into the bare decoration def
means the user has explicitly indicated anything less than dac is an error.

So returning false in this example is exactly what the user expects, since
[1,2] cannot be a subset of any defined and continuous interval range of
floor([0,6]).

Nate