2

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
Cactus
  • 27,075
  • 9
  • 69
  • 149
  • I also don't see a good way of expressing it as "the difference is less than one ps" unless there's some absolute difference operator (since using just `Nat` subtraction won't reduce for the *smaller* - *larger* case) – Cactus Sep 08 '18 at 05:11
  • 1
    That `div` is a type variable. I think we might actually have type-level division though... – dfeuer Sep 08 '18 at 05:22
  • 1
    @dfeuer oh crap, you're absolutely right... that's what I get for hacking on Haskell, Idris and Agda in quick succession... – Cactus Sep 08 '18 at 05:23
  • 1
    Heh. Yeah, that's an easy one to mix up. I've always liked Haskell's case sensitivity, but a few days ago Ed Kmett mentioned that there are no Chinese characters recognized as "upper case", which really throws a wrench into the system. – dfeuer Sep 08 '18 at 05:25
  • @dfeuer: That sounds more like a feature... the last thing the programming world needs is fragmentation along NATURAL languages. – Cactus Sep 08 '18 at 05:28

1 Answers1

5

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.

Cactus
  • 27,075
  • 9
  • 69
  • 149