Для простоты чтения я хотел бы использовать значения тактовой частоты в качестве моих индексов типов. Однако мне нужно будет проверить их на совместимость с тактовыми доменами, которые представляют их скорость в виде длительности периода.
Чтобы сделать это немного конкретнее, предположим, что у меня есть следующий тип данных, который для удобства чтения использует тактовую частоту (в Гц) в своем типе; в реальной программе это может быть, например, Время VGA:
data Rate (rate :: Nat) = MkRate
rate :: Rate 25175000
rate = MkRate
Однако мне нужно использовать его вместе с типами, которые представляют тактовый период (в пикосекундах); в настоящей программе CLaSH это был бы сам домен часов.
data Period (ps :: Nat) = MkPeriod
period :: Period 39721
period = MkPeriod
И теперь начинаются проблемы, поскольку один период на 25,175 МГц не является целым числом пикосекунд. Для начала попробуем использовать умножение:
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