周期长度和频率之间的类型级转换

为了更具体一点,假设我有以下数据类型,出于可读性的目的,它在类型中使用时钟频率(以Hz为单位);在实际程序中,这可能是例如VGA计时:

data Rate (rate :: Nat) = MkRate

rate :: Rate 25175000
rate = MkRate

但是,我需要将它与表示时钟周期(以皮秒为单位)的类型一起使用;在真正的CLaSH程序中,这将是时钟域本身。

data Period (ps :: Nat) = MkPeriod

period :: Period 39721
period = MkPeriod

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

test1 :: ()
test1 = connect1 rate period

这以预期的方式失败:

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

我们可以尝试的另一个方法是类型级别划分:

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

test2 :: ()
test2 = connect2 rate period

但这似乎并没有减少:

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