ScopedTypeVariables to fix type safety flaws

Recently I struggled to implement a simple converter from a type representing an integer number of seconds to NominalDiffTime from module Data.Time.Clock. For simplicity, let the original type be a simple Integer value counting a number of seconds. It felt like the solution was straightforward. Indeed, the module provides a dead simple conversion function secondsToNominalDiffTime of type Pico -> NominalDiffTime. Type Pico is a fixed-precision value from module Data.Fixed with twelve digits after the dot. Below is the original definition of conversion function toNominalDiffTime in GHCi REPL.

GHCi, version 8.10.2: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/lyokha/.ghci
Prelude> import Data.Fixed as F
Prelude F> import Data.Time.Clock as TC
Prelude F TC> toNominalDiffTime = secondsToNominalDiffTime . MkFixed . (resolution (undefined :: Pico) *)
Prelude F TC> :t toNominalDiffTime
toNominalDiffTime :: Integer -> NominalDiffTime
Prelude F TC> toNominalDiffTime 23
23s
Prelude F TC> toNominalDiffTime 2383747764736464646
2383747764736464646s

Notice that the original value must be multiplied by the resolution of Pico (i.e. 1000000000000), otherwise the converted value will be one picosecond.

Looks good, does it? Nope… This explicit type annotation of undefined is frustrating. What if I make a mistake and put another type instead?

Prelude F TC> toNominalDiffTime = secondsToNominalDiffTime . MkFixed . (resolution (undefined :: Nano) *)
Prelude F TC> toNominalDiffTime 23
0.023s

In many contexts, this is a catastrophe! How do I get rid of the explicit type declaration? Why did I put it here after all? The root of the problem is that resolution gets fed with an Integer value, while it requires a Fixed value. This is why we created an undefined object of type Pico which is a type synonym of Fixed E12. After getting the resolution from this object and multiplying this by the original value, the calibrated value gets piped to constructor MkFixed which expects an integer value calibrated with resolution of Pico because function secondsToNominalDiffTime requires this concrete type. At this moment, we cannot check correctness of the calibration because the temporary undefined object is already unreachable. In other words, the Fixed type context gets broken between resolution and MkFixed, which I would regard as a type safety flaw.

How can we fix this? Let’s first make a Fixed value and then get its resolution.

Prelude F TC> import Control.Arrow as A
Prelude F TC A> asIntegerPart = uncurry (*) . (MkFixed . (^2) . resolution &&& id) . MkFixed
Prelude F TC A> :t asIntegerPart 
asIntegerPart :: HasResolution a => Integer -> Fixed a
Prelude F TC A> toNominalDiffTime = secondsToNominalDiffTime . asIntegerPart 
Prelude F TC > :t toNominalDiffTime
toNominalDiffTime :: Integer -> NominalDiffTime
Prelude F TC A> toNominalDiffTime 23
23s

This works fine and is type safe. Except the algorithm has changed and become less clear. Here we created a fixed-precision value from the original Integer value. Say, if the original value was 23 then MkFixed must produce 0.000000000023 from this. Then we made a fixed-precision value from the quadratic resolution of Pico and multiplied this by value 0.000000000023. Is it clear why quadratic? The answer is simple: the single resolution would give us 1.000000000000 as the multiplier, while the quadratic gives 1000000000000.000000000000. Also notice that there are no explicit type annotations here because (*) expects two arguments of the same type and returns a value of this very same type.

Prelude F TC A> :t (*)
(*) :: Num a => a -> a -> a

As soon as secondsToNominalDiffTime expects Pico, all fixed-precision values in asIntegerPart must be Pico.

Let’s turn back to our simple algorithm and try to make it type safe. A solution could involve using wrapping type classes, GADTs, etc. However, surprisingly, there is a very simple and straightforward solution!

So, what do we want after all? Something like in the following snippet.

Prelude F TC A> :{
Prelude F TC A| asIntegerPart :: HasResolution a => Integer -> Fixed a
Prelude F TC A| asIntegerPart = MkFixed . (resolution (undefined :: Fixed a) *)
Prelude F TC A| :}

Sadly, this does not compile.

<interactive>:36:28: error:
    • Could not deduce (HasResolution a0)
        arising from a use of ‘resolution’
      from the context: HasResolution a
        bound by the type signature for:
                   asIntegerPart :: forall a. HasResolution a => Integer -> Fixed a
        at <interactive>:35:1-54
      The type variable ‘a0’ is ambiguous
      These potential instances exist:
        7 instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the first argument of ‘(*)’, namely
        ‘resolution (undefined :: Fixed a)’
      In the second argument of ‘(.)’, namely
        ‘(resolution (undefined :: Fixed a) *)’
      In the expression: MkFixed . (resolution (undefined :: Fixed a) *)

Obviously, type variables a in the signature and in the declaration of the function denote different entities, but we wanted them to be of the same type. This is where ScopedTypeVariables extension must help!

Prelude F TC A> :set -XScopedTypeVariables 
Prelude F TC A> :{
Prelude F TC A| asIntegerPart :: HasResolution a => Integer -> Fixed a
Prelude F TC A| asIntegerPart = MkFixed . (resolution (undefined :: Fixed a) *)
Prelude F TC A| :}

<interactive>:40:28: error:
    • Could not deduce (HasResolution a0)
        arising from a use of ‘resolution’
      from the context: HasResolution a
        bound by the type signature for:
                   asIntegerPart :: forall a. HasResolution a => Integer -> Fixed a
        at <interactive>:41:1-54
      The type variable ‘a0’ is ambiguous
      These potential instances exist:
        7 instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the first argument of ‘(*)’, namely
        ‘resolution (undefined :: Fixed a)’
      In the second argument of ‘(.)’, namely
        ‘(resolution (undefined :: Fixed a) *)’
      In the expression: MkFixed . (resolution (undefined :: Fixed a) *)

Hmm, no change. But we know that extension ScopedTypeVariables expects explicit forall quantifiers in the signature!

Prelude F TC A> :{
Prelude F TC A| asIntegerPart :: forall a. HasResolution a => Integer -> Fixed a
Prelude F TC A| asIntegerPart = MkFixed . (resolution (undefined :: Fixed a) *)
Prelude F TC A| :}
Prelude F TC A> toNominalDiffTime = secondsToNominalDiffTime . asIntegerPart
Prelude F TC A> :t toNominalDiffTime
toNominalDiffTime :: Integer -> NominalDiffTime
Prelude F TC A> toNominalDiffTime 23
23s
Prelude F TC A> toNominalDiffTime 73643545463262772
73643545463262772s

Finally, with ScopedTypeVariables, the algorithm gets working and type safe, while still being straightforward as in the first try.