WIP: Clock Lines in Haskell

Ericson2314 commented 9 years ago

It once occurred to me that the propagation of SClocks matches the routing of clock lines [I brought this up on IRC a while back]. The match is exact if it is changed so SClocks cannot be synthesized so topLevel must have parameters for all SClock clock lines. I then thought that we could leverage that to avoid having to add the clock lines manually during the compilation process.

Of course, routing clock lines is boring chore, but implicit parameters can largely automate the process. This patch uses them to do just that, without messing with the templated functions so that it should work with today's clash-compiler.

I see two downsides:

Unlike Agda and Lean's implicit parameters, Haskell's use the name of the binding, rather than the type, to infer the arguments, and also provides no way to positional manually instantiate the parameter. This leads one to do things awkward things like let ?clk1 = wclk; ?clk2 = rclk in unsafeSynchronize rather than unsafeSynchronize ?wclk ?rclk or just unsafeSynchronize. [See CLaSH/Prelude/Synchronizer.hs for good examples of this.]
GHC might inline the SClocks it thinks are irelevant before clash gets a chance to leverage them.

I also see that with ghc8 branch it looks like you are trying to remove the need for SClocks in most code altogether. That might be a better route in the short term as it avoids the awkwardness that is my first downside. But that looses out on the ability to leverage them for simplifying compilation. I also wonder how hard it would be to change the way implicit parameters worked or make a new extension.

This is WIP because I have only tested that it type checks (with GHC 7.10), and haven't bothered to fix the docs / doc tests.

Ericson2314 commented 9 years ago

Oh, I forgot the bigger advantage over just removing SClock than just simplifying compilation: PLLs and other "clock functions" can be written like normal black-box templates:

{-# NOINLINE pll #-}
pll :: forall num denom sym1 sym2 x y
    .  x * num / donom ~ y
    => SNat num
    -> SNat denom
    -> SClock sym1 x
    -> SClock sym2 y
pll _ _ _ _ = sclock

christiaanb commented 9 years ago

Just some initial comments:

I like:

Getting to drop the whole "hidden ports" story that we currently have in the CLaSH compiler
Having clock manipulators as CLaSH functions, even if they have to be marked NOINLINE

I don't like:

"Inlining SClock might break everything". It's annoying and error-prone to add exceptions in the CLaSH compiler as to what may not be inlined. It's worse for the GHC frontend, as we have little control over it.
Type-signatures either have to mention the implicit params, or explicit SClock arguments. Although implicit params make passing clocks "free" at the term-level, you trade it for passing it explicitly at the type-level.

A potential solution for "don't like" 1 is to make constructing SClocks a very hard thing to do. For example by putting it in a scary Internal module, and putting in the documentation that SClock creating functions must only be put in functions marked by NOINLINE. As a consequence, none of the current prelude functions should have explicit SClock arguments, they must all be made implicit params.

Ericson2314 commented 8 years ago

Yeah, for 1 there is a tension in that the easiest thing to do to make sure users don't instantiate SClocks is make them uninhabited, but the GHC is more likely to see them as irrelevant.

I'm thinking in the manner of https://hackage.haskell.org/package/base-4.8.1.0/docs/Text-Printf.html#t:PrintfType we can write so that users won't need an access a sclock value at all for trying things at the repl--basically a higher order function to eliminate an initial chain of clock line arguments. I'll try to add a commit demonstrating it soon.

Yeah, 2 is annoying. Hopefully partial type signatures or a type alias like

type WithSystemClock a = (?clk :: SystemClock) => a

can lesson the blow, but the latter might require RankNTypes.

Ericson2314 commented 8 years ago

Oh I forgot that pushing a commit doesn't make a notification.

christiaanb commented 8 years ago

First on the helper utility: ok, that looks good for explicit clock arguments, but how would we handle the implicit param clock arguments?

In general: I wonder if the increase in complexity is worth getting {-# NOINLINE #-} clock primitives in CLaSH. Especially as a barrier to entry into CLaSH, and existing users having to update many of their type signatures. Given that you are calling this PR a WIP, what are your intentions in terms of getting this merged? is it just a proof concepts? or do you want it to actually be merged? and if you want to get it merged, when? I'm asking because I feel such a large change to CLaSH should no longer just be decided/commented on by just me. Perhaps before if/when this gets merged, we should first ask for feedback on the CLaSH mailing list.

Ericson2314 commented 8 years ago

But how would we handle the implicit param clock arguments?

I have no idea unfortunately, that implicit parameters are constraints is quite inconvenient here.

Given that you are calling this PR a WIP, what are your intentions in terms of getting this merged?

Well I opened the PR in the first place to just get something concrete to talk about. I would ask the mailing list if you are tentatively interested, and if there is a consensus to actually do this, then fix the tests. At that point, this could actually be merged.

Oh, and one final benefit is that I could imagine some escape hatch for clock gating:

clockToWire :: (?clk :: SClock (Clock s (2 * p))) => Signal (Clock s p) Bit
clockToWire = 1 :- 0 :- clockToWire

Not sure why one would use this, but it does represent something that is expressible in Verilog but not Clash at the moment.

christiaanb commented 8 years ago

This Rank2 function sorta does what provideClocks do, but then for the IP clock named ?clk:

provideIClock :: (KnownSymbol nm, KnownNat r) => ((?clk :: SClock ('Clk nm r)) => a) -> a
provideIClock x = let ?clk = sclock in x

So all the implicity clocked functions would then be called in GHCi using provideIClock, and all explicityly clocked functions would be called using provideClocks. This would mean that unsafeSynchronizer should have normal SClock arguments again, not IP ones.

We can then also provide the beginner friendly simulate function:

simulate :: ((?clk :: SClock SystemClock) => Signal a -> Signal b)
         -> [a] -> [b]
simulate f xs = let ?clk = systemClock in toList (f (fromList xs))

All of this is making me see the IP approach in a much more favourable light.

christiaanb commented 8 years ago

I also noticed that in normal GHCi I need to disable the MonomorphismRestriction in order to get type inference for function definitions involving IPs, such as:

-- counter :: (?clk :: SClock clk, Num a) => Signal' clk a
counter = let s = register 0 (s + 1) in s

With the MonomorphismRestriction enabled, I need to add the type signature in the comment. I don't think this is a problem for the CLaSH interpreter, because I think I disabled the MonomorphismRestriction by default.

Ericson2314 commented 8 years ago

provideIClock and simulate look great!

This would mean that unsafeSynchronizer should have normal SClock arguments again, not IP ones.

Yeah every time I used unsafeSynchronizer is used in clash-prelude, I had to effectively manually apply the arguments anyways, because of the stupid by-name not by-type inference. Maybe a good rule is that function get IP clocks iff they only need a single clock, and it is always called ?clk :: .... Even if inferring implicit params was smarter, it could be considered be too spooky to infer multiple different clocks.

I also noticed that in normal GHCi I need to disable the MonomorphismRestriction...

Hmm, I did cabal repl with ghc 7.10, then did

:set -XImplicitParams
let counter = let s = register 0 (s + 1) in s
:t counter

and got back

counter
  :: (Num a, ?clk::CLaSH.Signal.Internal.SClock clk) =>
     CLaSH.Signal.Internal.Signal' clk a

christiaanb commented 8 years ago

Ah, sorry, what I meant to say is that: if I create Test.hs:

module Test where

import CLaSH.Prelude

counter = let s = register 0 (s+1) in s

and load it in GHCi, I get an error.

Ericson2314 commented 8 years ago

Ah gotcha. Well, that's unfortunate, but maybe fixable upstream someday.

christiaanb commented 8 years ago

I noticed that I didn't mention it yet: with the addition of provideIClock and the new simulate function, I'm in favour of this change.

I would like it to happen simultaneously with the changes in the ghc8 branch though, given that they both affect clock handling in a major way. Once GHC 8.0.1 is actually released, I will finish the ghc8 branch, and then you can base your patches on top of the ghc8 branch?

Ericson2314 commented 8 years ago

Excellent—glad this is working out! I'll be happy to do rebase/redo that when we're ready.

christiaanb commented 8 years ago

@Ericson2314 Im trying some new definitions for Signal/Clock/Reset over here: https://gist.github.com/christiaanb/8298743add74e5c566ecfca354ba6a76

Ericson2314 commented 8 years ago

Oh cool! Sorry for being AWAL, but after I graduate this week I'll have time (and interest) to take a big stab at all this. And GHC 8 is finally out!

christiaanb commented 8 years ago

@Ericson2314 no problem at all, and congrats on graduating!! Also, I've started a wiki page: https://github.com/clash-lang/clash-prelude/wiki/Clock-and-reset-modelling about modelling clocks/resets, and its flaws, in the current version of CLaSH; and also proposals on how to fix those flaws in the next version.

christiaanb commented 7 years ago

Superseded by #115

clash-lang / clash-prelude

WIP: Clock Lines in Haskell #36