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

Question

为了便于阅读,我想使用时钟频率值作为我的类型索引.但是,我需要检查这些与时钟域的兼容性,时钟域代表它们作为周期长度的速度.

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

data Rate (rate :: Nat) = MkRate

rate :: Rate 25175000
rate = MkRate

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

data Period (ps :: Nat) = MkPeriod

period :: Period 39721
period = MkPeriod

现在问题开始了,因为25.175 MHz的一个周期不是整数皮秒.首先,让我们尝试使用乘法:

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

Answer 1

原来的ghc-typelits-extra包 具有分裂这降低; 这让我写了

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

test = connect rate period

它确定了.