Type-level conversion between period length and frequency

Question

For ease of reading, I'd like to use clock frequency values as my type indices. However, I'll need to then check these for compatibility with clock domains, which represent their speed as period lengths.

To make this a bit more concrete, suppose I have the following datatype which, for readability purposes, uses the clock rate (in Hz) in its type; in a real program, this could be e.g. VGA timings:

data Rate (rate :: Nat) = MkRate

rate :: Rate 25175000
rate = MkRate

However, I need to use it together with types that represent the clock period (in picoseconds); in a real CLaSH program, that would be the clock domain itself.

data Period (ps :: Nat) = MkPeriod

period :: Period 39721
period = MkPeriod

And now the problems start, since one period at 25.175 MHz is not an integer number of picoseconds. First, let's try using multiplication:

connect1 :: ((rate * ps) ~ 1000000000000) => Rate rate -> Period ps -> ()
connect1 _ _ = ()

test1 :: ()
test1 = connect1 rate period

This fails in the expected way:

../clash-sandbox/lib/src-clash/Cactus/Clash/VGA.hs:79:9: error:
    • Couldn't match type ‘999976175000’ with ‘1000000000000’
        arising from a use of ‘connect1’
    • In the expression: connect1 rate period
      In an equation for ‘test1’: test1 = connect1 rate period
   |
79 | test1 = connect1 rate period
   |         ^^^^^^^^^^^^^^^^^^^^

Another thing we could try is type-level division:

connect2 :: (ps ~ (1000000000000 `div` rate)) => Rate rate -> Period ps -> ()
connect2 _ _ = ()

test2 :: ()
test2 = connect2 rate period

but that doesn't seem to reduce:

../clash-sandbox/lib/src-clash/Cactus/Clash/VGA.hs:85:9: error:
    • Couldn't match type ‘39721’ with ‘div0 1000000000000 25175000’
        arising from a use of ‘connect2’
    • In the expression: connect2 rate period
      In an equation for ‘test2’: test2 = connect2 rate period

Answer 1

Turns out the ghc-typelits-extra package has division which reduces; this allowed me to write

connect :: (ps ~ (1000000000000 `Div` rate)) => Rate rate -> Period ps -> ()

test = connect rate period

and it typechecks OK.