Add Clash.Class.Convert

[martijnbastiaan]

Utilities for safely converting between various Clash number types.

To discuss / investigate (but maybe not for this PR?)

• The instances add 1 <= n constraints to every result where the result is Index n
  • This makes sense from a perspective of: Index 0 has no inhabitants, so we cannot create it. On the other hand, we can of course just call errorX "foo". I'm not sure whether I would say this violates the "guaranteed to succeed" rule.
• The instances add 1 <= n constraints to every argument where the argument is Index n
  • This is similar to the first point, but differs in that we shove the responsibility for creating these values to the caller.
• convert and maybeConvert will always return XException if given an XException.
  • Does this make sense for converting BitVector 0 to Index/Unsigned/Signed? The HDL will happily do it, why wouldn't Clash simulation? Similarly, any BitVector n could be repacked to be partially undefined if converted to another BitVector m where m > n.

I'd push for kicking these questions to after this PR, because:

• We can always relax constraints (but not introduce them)
• We can always relax XException behavior (but not introduce it).
• Having a safe way of converting between Clash types is way more important than dropping a minor constraint.
• It's a fairly delicate thing I don't think we have a proper/consistent view on yet across clash-prelude.

Still TODO:

• Write a changelog entry (see changelog/README.md)
• Check copyright notices are up to date in edited files
• Decide whether to call it Clash.Class.Convert or Clash.Class.Convertible. The latter has some buy-in (?) from the community, given that covertible already exists. On the other hand, this might make users think it is convertible, but it isn't.

[DigitalBrains1]

I'd vote against naming it Convertible, since I think GHC will by default not qualify the class name in an error message of the form No instance for ‘Convertible A B’, which might be very misleading.

_{(I really want to make the silly pun No instance for ‘Convertible Coupé Roadster’ but it seems confusing... X-D)}

[martijnbastiaan]

To change because it isn't a separate package

[martijnbastiaan]

"safe and total" is not terminology introduced earlier

[DigitalBrains1]

Also, we usually mean something else by total in the Haskell world. We mean the function always returns a value, there is no input value for which it bottoms. But resize . bitCoerce and bitCoerce . resize are both total functions for most types in that sense! I think only Resize Index does not.

resize is not injective, though. But in the interest of clarity to users who are not very used to mathematical language, I feel a description is more useful than just saying injective.

But I would recommend dropping the use of the term total for that other group of users, the ones who do know what it usually means for a Haskell function and might misinterpret.

[martijnbastiaan]

I don't like the word "safe" here.

[DigitalBrains1]

In addition, the laws don't mention this property that is in the module documentation:

Utilities for converting between Clash number types in a safe way.

You define what safe means in the laws, but then only require the property in the module documentation, not directly in the laws. I'd like to add a law such that the set of laws does not depend on the module documentation.

[kleinreact]

LGTM overall.

I'm going to accept this, because I cannot see anything really controversial in the sense that it would be hard to fix it later on.

Regarding the Convert vs Convertible question: I don't like either name, as they both suggest much freedom in terms of which types could be converted with the classes. Your documentation clearly restricts the setting to number types, which is in contrast to Convertible for example, which is also open for conversion between custom non-number types. So maybe we should keep the users of that package happy by not producing any name clash at this point.

A name like changeNumType would make it more clear to me what the purpose of this function is. Convert, Convertible, and convert are just super generic names!

I still find it strange to consider BitVector a number type. If we are going to have a discussion about this at some point, then I'd suggest to keep it out here for the time being. Adding it later is easy and the user still can define the instance locally, if necessary.

I don't like the fact that we need to have two classes in the end, but I get the point that the need for individual selection of constraints per instance introduces that requirement.

[kleinreact]

Is there a particular reason for mixing maybeConvert and convert in a single law? Wouldn't it make more sense to have a separate law per class, as a type not necessarily needs to be an instance of both?

[martijnbastiaan]

Hmm, well it isn't imposed by anything, but it seems natural to me that everything that defines a Convert also defines a MaybeConvert. I get that that makes laws like these a bit iffy -- I'm happy to add a superclass constraint if that makes more sense to you. I'm not sure how to rephrase this law properly to just talk about convert.

[kleinreact]

You mention synthesizable HDL in Clash.Class.Convert. I'd suggest to keep the wording consistent.

[martijnbastiaan]

Agreed

[kleinreact]

The classical wording in legal specification documents usually is "must be guaranteed to succeed", as it is a user requirement, in case you like to stick with that.

[kleinreact]

I would either not add any instances for Word and Int, as their sizes are machine dependent, or the source of the respective conversions should be restricted to at most 32 bit, as this is what base fixes independently from the underlying machine.

[martijnbastiaan]

Oh woops. I think this just fails to compile on any platform that is not 32-bit, as the bitCoerce would type error. This did cross my mind, but I never followed up on it -- I'll add some CPP foo.

[kleinreact]

The RHS parenthesis are redundant here.

Just noting this, as hlint won't complain about that, in case you prefer them being removed.

[martijnbastiaan]

Yeah.. this is something fourmolu does by default

[kleinreact]

As you have instances covering BitVector, it might be also desirable to have instances converting from Bit (Bool). Something like a Bit to Word8 conversion sounds reasonable to me.

On the other hand, we should ask ourselves whether BitVector should be considered a number type? I'm still struggling with conceptual separation here, as if BitVector is a number type, what distinguishes it from Unsigned then in the end?

[martijnbastiaan]

Bit/Bool: yes good point.

Num: I've got two answers:

• For this PR specifically: IMO this class shouldn't take a stance on that -- anything that has a Num is a number type for its sake.
• Zooming out a bit I feel that BitVector should be an "unstructured collection of bits". (In practice it probably isn't truly unstructured, but for the domain that it is being handled in it is.) From a theoretical POV this makes the Num instance for BitVector icky IMO. However, I also feel that the convenience of being able to use literals (e.g., 0xFFAA) to construct them and do basic arithmetic on them trumps my theoretical concerns (not to mention what a massive API changes it would be to remove the instance). In practice I just end up using it to signal to developers that bits are unstructured.

[kleinreact]

I personally prefer the convention to call this function convertMaybe (similar to readMaybe in base), as the name then denotes the order of operation: "first convert and then put the potential result into the Maybe container". maybeConvert suggests to me that the function converts from a Maybe as the input.

Another advantage of convertMaybe is that TAB completion in the REPL will display both: convert and convertMaybe, as soon as you started typing c o n ... .

[martijnbastiaan]

I'm fine with either as far as naming schemes go. I do think we've already set a precedent in clash-prelude, i.e.:

martijn@volthe:~/code/clash-compiler$ egrep -r '^maybe[A-Z].*::'  clash-prelude/src | wc -l
7
martijn@volthe:~/code/clash-compiler$ egrep -r '^.*Maybe ::'  clash-prelude/src | wc -l
1

so I think we should continue that. (Or change that, but that's for another PR.)

[martijnbastiaan]

Thanks for the comments @kleinreact, I'll get to them, though I'm fairly time constrained at the moment :(.

I think your comment about the name convert makes a lot of sense. Maybe convertNum? You're right that the class really constrains it to just number types. (Maybe that is an issue?)

[DigitalBrains1]

Somehow I feel NumConvert feels more natural than ConvertNum for the class name... But not so for the function name.

Also, we could rewrite the laws such that the class can also be used for non-numbers. I think that would work?

[DigitalBrains1]

I also feel Convert is too generic a name and squats too much, except if it is only to be used qualified. I'm personally leaning towards renaming it NumConvert, numConvert, MaybeNumConvert and maybeNumConvert as the names used, and exporting them from Prelude. Note that you currently to not export them from Prelude, I'd like that to be added.

Something I noticed is that for Convert, you seem to put a bang pattern only on the instances that need one to preserve the XException, yet on MaybeConvert you just bang almost everything. Was this intended? I'm not against it, I'm just wondering.

[DigitalBrains1]

Also, we usually mean something else by total in the Haskell world. We mean the function always returns a value, there is no input value for which it bottoms. But resize . bitCoerce and bitCoerce . resize are both total functions for most types in that sense! I think only Resize Index does not.

resize is not injective, though. But in the interest of clarity to users who are not very used to mathematical language, I feel a description is more useful than just saying injective.

But I would recommend dropping the use of the term total for that other group of users, the ones who do know what it usually means for a Haskell function and might misinterpret.

[DigitalBrains1]

Suggested change

	if an instance exist, but the constraints cannot be satisfied, then
	if an instance exists, but the constraints cannot be satisfied, then

[DigitalBrains1]

Suggested change

	'Clash.Class.Convert.convertMaybe' should return 'Nothing' for one or more values in
	'maybeConvert' should return 'Nothing' for one or more values in

This is a dead link.

The qualification is not necessary; the function is documented in this module. If it's unqualified, our Haddock CI check will notice the dead link, unlike in the qualified situation.

But regarding this whole paragraph: I found it hard to understand because I misinterpreted what it means for an instance to exist. Because to me, if the constraints are not satisfied, an instance does not exist. So I'd say that there is no instance for Convert (Unsigned 8) (Unsigned 4), whereas the language in this paragraph says the instance exists, but its constraints can't be satisfied. I hope we can rephrase it to avoid this pitfall.

[DigitalBrains1]

Suggested change

	For the time being, if the input is an @XException@, then the output is too. This
	For the time being, if the input is an 'XException', then the output is too. This

I didn't check it is in scope.

[DigitalBrains1]

As per earlier comment: let's get rid of the word total here.

[DigitalBrains1]

This seems unnecessary? We know the Signed n is positive, so we can, without loss of semantics, bitCoerce @_ @(Index (2 ^ n), right? It's basically casting Signed n to Unsigned n. We could even have reduced that to Unsigned (n-1) because we know the MSB of the Signed n is 0, but this gives us natural-number-headaches, so I'm not suggesting that. But the n + 1 is really overly broad if I'm not terribly mistaken.

[DigitalBrains1]

bitCoerce loses the message and back trace of an XException (meaning, it throws a new one). I'd prefer the original XException being preserved (with a bang pattern).

[DigitalBrains1]

Did you forget

instance (MaybeConvert a (Signed 64)) => MaybeConvert a Int64
instance (MaybeConvert a (Signed 32)) => MaybeConvert a Int32
instance (MaybeConvert a (Signed 16)) => MaybeConvert a Int16
instance (MaybeConvert a (Signed 8)) => MaybeConvert a Int8

?

[DigitalBrains1]

So this test completes in two cases:

1. There's a Nothing in the results
2. results is not empty

Condition 1 is no longer relevant, as condition 2 already captures all cases where condition 1 is true. This just tests results is not empty!

I feel this would capture the stated behaviour:

convertLaw3 _ _ = L.any isNothing results || L.null results

but that L.null results never actually has an effect, and it still makes the tests fail for:

convert @(Index 1) @(Signed 0)
convert @(Unsigned 0) @(Signed 0)
convert @(BitVector 0) @(Signed 0)

The problem is that

>>> L.map (maybeConvert @(Index 1) @(Signed 0)) [minBound ..]
[Just 0]
>>> L.map (maybeConvert @(Unsigned 0) @(Signed 0)) [minBound ..]
[Just 0]
>>> L.map (maybeConvert @(BitVector 0) @(Signed 0)) [minBound ..]
[Just 0]

[DigitalBrains1]

Let me be a bit more explicit:

The L.null results branch of the test never helps you. I think this case simply never occurs, but it is clear you can remove it and not affect the outcome: convertLaw3 _ _ = L.any isNothing results works just as well.

The three problematic tests are precisely those of which you already note:

Note: Conversion from Index 1 to Signed 0 is total, but not within the constraints of the instance.

So your test correctly tests the law, it just needs some exceptions for the cases where you document a deviation from the laws. I think in your Python script you actually already flag these cases with constraints[(a, b)][0], but you never use this boolean, you only use the second element of the tuple. I suspect that you should use that flag to generate

assertBool (show (n, m))
  (convertLaw3 (Proxy @(Index (n + 1))) (Proxy @(Signed m)) || (n == 0 && m == 0))

instead of the current

assertBool (show (n, m)) (convertLaw3 (Proxy @(Index (n + 1))) (Proxy @(Signed m)))

[DigitalBrains1]

If you make it so that the original XException is always preserved, you could make this test stricter by testing that the message of the original XException is also the message of the ouput XException (same for the Convert tests).

[DigitalBrains1]

Ah skipped one. As per earlier comment: let's get rid of the word total here.