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
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.