Convenience operators?

[dmcclean]

Would it help in implementing rounded intervals with tighter bounds (instead of always rounding the inf down and sup up) if there were convenience operators like these?

(+↑) :: Double -> Double -> Double
a +↑ b = toDouble (a' + b')
  where
    a' = (fromDouble a) :: Rounded TowardInf Double
    b' = (fromDouble b) :: Rounded TowardInf Double

(+↓), (+↕), (+₀) :: Double -> Double -> Double
...

(*↑), (*↓), (*↕), (*₀) :: Double -> Double -> Double
...

And so forth ad nauseam (or ad TH-eam)?

(There are several possible choices for the character to indicate "towards zero". I couldn't find one that has a downwards arrow and an upwards arrow meeting in the middle, which would probably be ideal. I don't think that subscript 0 is a legal operator identifier character, either...)

[ekmett]

I was leaning towards just adding 'towardZero' etc. and having those, instead of working on Double, use coerce to switch rounding modes.

towardZero :: Rounded r p -> Rounded TowardZero p
towardZero = coerce

[dmcclean]

I think I see.

To me it is opaque what this does:

instance Precision p => Num (Interval p) where
  I a b + I a' b' = I (a + a') (b + b')
  _ + _ = Empty
  I a b - I a' b' = I (a - coerce b') (b - coerce a')
  _ - _ = Empty
  negate (I a b) = I (coerce (negate b)) (coerce (negate a))
  negate Empty = Empty
  I a b * I a' b' =
    I (minimum [a * a', a * coerce b', coerce b * a', coerce b * coerce b'])
      (maximum [coerce a * coerce a', coerce a * b', b * coerce a', b * b'])
  _ * _ = Empty
  abs x@(I a b)
    | a >= 0 = x
    | b <= 0 = negate x
    | otherwise = I 0 (max (negate (coerce a)) b)
  abs Empty = Empty

because the logic of how things are rounded is encoded in which operands are coerced and which aren't. (I think, I may not even be understanding that correctly.)

So this line I a b - I a' b' = I (a - coerce b') (b - coerce a') means a - b' rounded down, and b - a' rounded up, because how how the type of I is.

I'm not sure I see how towardZero would be used, because while you could write I a b - I a' b' = I (towardNegInf $ a - coerce b') (towardInf $ b - coerce a') as a way of inline documentation that has no runtime existence you still need to put the coerce in the right place.

Now that I think about it, though, it may be that the rounded interval type is sufficiently magical that it takes almost all of the other sites where manipulations like this have to happen and makes them obsolete. I know I have some C code that has comments all over the place that deal with this, so I was thinking as if I needed to litter the Haskell version with operators that explicitly round, but now that I look at it more it seems like just switching those things to interval arithmetic deals with at least 95% of it. (With the leftovers being places that are written in a strange way for numerical reasons or places where the nature of the function you are implementing means you know of a tighter bound.)

[dmcclean]

Semi-relatedly, could you help me understand the difference between the roles nominal and phantom?

[ekmett]

The coerces there are to swap rounding modes to match whatever arg they have to. They literally go in exactly the places they need to to typecheck and this does the right thing.

Re representational nominal and phantom:

If you had something like

newtype Age = Age Int

You can infer Coercible Age Int and Coercible Int Age

coerce :: Coercible a b => a -> b

because we have

type role [] representational

and had a [Int] you should be able to coerce it to [Age] safely.

On the other hand nominal says you can't lift a Coercible instance over that argument. This is useful for things like Set where doing so would violate internal invariants. (If say, the Ord instance for Age behaved differently)

phantom says you don't even need Coercible a b to derive Coercible (f a) (f b)! You can always coerce that argument.

type role Const representational phantom
newtype Const m a = Const m

[dmcclean]

Oh, OK, I get the nominal thing now, thanks very much. For some reason I couldn't think of any examples and so I got confused.

Back on the original topic, that as you said "The coerces there are to swap rounding modes to match whatever arg they have to. They literally go in exactly the places they need to to typecheck and this does the right thing."

Couldn't they go everywhere? I'm assuming there's an instance Coercible a a where coerce = id.

I think the heart of the matter might be that when we are introducing intervals with I we need I :: Rounded TowardNegInf p -> Rounded TowardInf p -> Interval p. But when we are eliminating them, we can view each of the endpoints as being of type forall r.Rounded r p, right? (For two separate rs, one for the left and one for the right.)

With the right ViewPatterns and PatternSynonyms pattern, I think nearly all the coerces would disappear without anything bad happening. I'm not sure about the ones on line 56, but almost all of the others.

-- -- | lift a monotone decreasing function over a given interval
decreasing :: (forall r. Rounding r => Rounded r a -> Rounded r b) -> Interval a -> Interval b
decreasing f (I a b) = I (coerce (f b)) (coerce (f a))
decreasing _ Empty = Empty

While I was checking to see which ones would disappear I found something else that I will make another issue about, since it's not really related.

[ekmett]

What I meant is that if you tried to coerce the wrong way then it'd fail and if you put in too many of them in most cases the intermediate values would be ambiguous and you'd need to solve it with type signatures.

I actually don't mind the 'coerce's. They force me to think about the rounding modes I need to use as I go, but importantly, if I try to do a dumb thing the argument I don't coerce will yell at me.

The current approach catches more errors than the rank-2 eliminators would.

On Mon, Apr 21, 2014 at 8:58 PM, Douglas McClean notifications@github.comwrote:

Oh, OK, I get the nominal thing now, thanks very much. For some reason I couldn't think of any examples and so I got confused.

Back on the original topic, that as you said "The coerces there are to swap rounding modes to match whatever arg they have to. They literally go in exactly the places they need to to typecheck and this does the right thing."

Couldn't they go everywhere? I'm assuming there's an instance Coercible a a where coerce = id.

I think the heart of the matter might be that when we are introducing intervals with I we need I :: Rounded TowardNegInf p -> Rounded TowardInf p -> Interval p. But when we are eliminating them, we can view each of the endpoints as being of type forall r.Rounded r p, right? (For two separate rs, one for the left and one for the right.)

With the right ViewPatterns and PatternSynonyms pattern, I think nearly all the coerces would disappear without anything bad happening. I'm not sure about the ones on line 56, but almost all of the others.

-- -- | lift a monotone decreasing function over a given interval decreasing :: (forall r. Rounding r => Rounded r a -> Rounded r b) -> Interval a -> Interval b decreasing f (I a b) = I (coerce (f b)) (coerce (f a)) decreasing _ Empty = Empty

While I was checking to see which ones would disappear I found something else that I will make another issue about, since it's not really related.

— Reply to this email directly or view it on GitHubhttps://github.com/ekmett/rounded/issues/16#issuecomment-40993618 .

[dmcclean]

OK, sounds good to me.