serokell / o-clock

:hourglass: Type-safe time units in Haskell
Mozilla Public License 2.0
49 stars 6 forks source link

Safe subtraction? #118

Open kindaro opened 3 years ago

kindaro commented 3 years ago

Since there is no Num instance (see #106), it is impossible to subtract times. But this is an important thing to be able to do. For example, consider animation. Suppose I wish to display a new frame every 10 milliseconds, but it takes variable time to compute the frame and the remaining time I must wait with threadDelay. I may save the time of the start x₀ and the end x₁ of the computation, but now I must calculate 10ms − (x₁ − x₀) and there is no way to do that!

An immediate objection is that there is no indication of sign for time values. We can amend this by returning 0 whenever the result of the subtraction would be negative.

Currently I have this function:

subtractTime
  ∷ forall α. (KnownRat α, KnownRat (DivRat α (1 :% 1000000000)), KnownRat (DivRat (1 :% 1000000000) α))
  ⇒ Time α → Time α → Time α
subtractTime x y = let δ = toNum @Nanosecond @Integer x - toNum @Nanosecond y in (toUnit @α ∘ time @Nanosecond ∘ fromIntegral) (max δ 0)

I have no idea how much it is wrong. To be honest, I do not even understand the type signature — GHC wrote it for me. I can only say that it seems to work.

kirelagin commented 3 years ago

There is (-:-) for subtraction. Unfortunately, it throws if the result is negative, but, IIUC, it should not be a problem in your use case. Alternatively, we could probably have a function that returns a Maybe.

kindaro commented 3 years ago

Thanks Kirill. I did not think to look at Time.Timestamp since I am not doing anything with time stamps. If the idea is that Timestamp represents a difference of time, then maybe I should be using it, but the interface does not seem well adapted to such case. (For example, timeDiff does not operate on Time.)

The arithmetic underflow exception will be a problem if the time it takes to compute the next frame is longer than 10 milliseconds. The graceful failure in this case is to render frames as fast as possible. And, as I understand, this exception cannot be caught in pure code.