Add Finite class #2858

kleinreact · 2024-12-30T12:56:16Z

The PR adds the Finite class as well as supplemental instances for most of the standard types.

Finite is a class for types with only finitely many inhabitants and can be considered a more hardware-friendly alternative to Bounded and Enum, utilizing Index instead of Int and vectors instead of lists.

Have a look at the haddock documentation for further insights.

Requires

Linear Clash.Sized.Vector.reverse #2871

Still TODO:

Write a changelog entry (see changelog/README.md)
Check copyright notices are up to date in edited files

martijnbastiaan

Couple of questions! Mostly wondering whether it would make sense to provide an Index-based Enum instead.

martijnbastiaan · 2024-12-30T20:06:27Z

clash-prelude/src/Clash/Explicit/Prelude.hs

+    res  = x :> prev'
+    prev' = case natVal (asNatProxy prev') of
             0 -> repeat def
-             _ -> let next = x +>> prev
-                  in  registerB clk rst en (repeat def) next
+             _ -> let next' = x +>> prev'
+                  in  registerB clk rst en (repeat def) next'


The fact that you have to do this is a pretty strong hint these names shouldn't be in Clash.Prelude. Grepping my projects for prev and next also reveals a number of uses.

That's kind of unavoidable. Every new name we choose might already be picked up in existing user code and I doubt that it's in the interest of the user, if we choose artificially unintuitive names just because of that.

So yes, the user might experience some new warnings about "clashing" names after a Clash update, which are always easy to fix via renaming or hiding the new stuff from Clash.Prelude, in case they are not desired.

Please note that finding a good (and intuitive) naming scheme that doesn't clash with basic existing libraries (in particular base) is a challenge already, especially if the offered primitives are quire fundamental. I also tried to improve the situation here based on some prior experience I had with the finite library, which comes with a similar interface.

I think the point is we write many state machines in Clash and there prev and next are very intuitive local names. Of course you can't avoid all name clashes, but there are some words that are very common in Clash code and prev and next are two examples of that specific category. So I agree with Martijn that trying to come up with an alternative is worthwhile in this specific case.

[edit]
Also, I believe we felt we wanted to move away from primes as a suffix in our code, instead using numeric suffixes to disambiguate. So I believe it'd be better to do that instead of introducing new uses of prime in our code base.
[/edit]

before/after?

prior/later?

back/forward?

Did not think them through much, just throwing it out there.

fpred / fsucc for finite versions of Enum functions?

succ :: a -> a

Successor of a value. For numeric types, succ adds 1.

pred :: a -> a

Predecessor of a value. For numeric types, pred subtracts 1.

I think that if they wanted to enforce that, then they would have added a law. But yeah, those two sentences are kind of misleading indeed.

If the Haddock of a class definition is not normative, what is? They usually use the word law in these cases, but there's no wiggle room in the doc that I see. If they wanted to document something that is common but not normative, I believe they would at the least add the word usually.

[edit]
My point is that these sentences are not misleading. Can you point me to an authoritative text that says otherwise? They are laws. They just didn't use the word law.
[/edit]

[edit 2]
satSucc and satPred are based on Enum. Enum says they should add and subtract one. So the doc for satSucc and satPred says they should add and subtract one.

Originally satSucc and satPred weren't even part of SaturatingNum. But we found that this lead to undesired behaviour of specific instances, so we moved them into the class because they're related enough to justify that.
[/edit 2]

My point is that these sentences are not misleading. Can you point me to an authoritative text that says otherwise? They are laws. They just didn't use the word law.

I'm not aware of any authoritative text, but the style of class requirement descriptions in base and ghc-prim varies a lot, so it doesn't look to me like they have a strict enforcement on wording at this point. I gave some examples below. According to those you need to take the Applicative laws very seriously for example, while the equality laws are more kind of a nice-to-have 🙃.

Eq

The Haskell Report defines no laws for Eq. However, == is customarily expected to implement an equivalence relationship where two values comparing equal are indistinguishable by "public" functions, with a "public" function being one not allowing to see implementation details. For example, for a type representing non-normalised natural numbers modulo 100, a "public" function doesn't make the difference between 1 and 201. It is expected to have the following properties:

Ord

The Haskell Report defines no laws for Ord. However, <= is customarily expected to implement a non-strict partial order and have the following properties:

Applicative

Further, any definition must satisfy the following:

Monad

Instances of Monad should satisfy the following:

satSucc and satPred are based on Enum.

Sure satSucc has a default implementation, which is satSucc s n = satAdd s n 1, but there is no requirement that I cannot chose a different implementation for my own type instances at this point.

It's also a questionable, whether just because of that every class instance should depend on having a Num instance as well. It would be much more user-friendly to have a default signature that requires Num, so the constraint is only required if the user wants to use the default in the first place, e.g.,

satSucc :: SaturationMode -> a -> a -- Default method suitable for types that can represent the number 1 default satSucc :: Num a => SaturationMode -> a -> a satSucc s n = satAdd s n 1 {-# INLINE satSucc #-}

This would elide the requirement on Num for every class instance.

Regarding satSucc and satPred I have primarily not been talking about documentation or implementation, I'm talking about invisible things like design and intent. And also how they changed once we noticed deficiencies.

Sure satSucc has a default implementation, which is satSucc s n = satAdd s n 1, but there is no requirement that I cannot chose a different implementation for my own type instances at this point.

We mean our documentation to be normative. So yes, I definitely interpret it as a requirement that they should add/subtract 1.¹ You yourself argued this above:

Do I miss something fundamental here? I read that like satSucc is equivalent to (+ 1), except for the boundary cases, where the behavior might differ. That's what I consider by "to compatible with each other".

I'd strongly argue that even in the boundary cases the behaviour matches adding/subtracting 1, it's just that (+ 1) does not actually add 1 in those cases.

(continuing with quote from your latest message)

It's also a questionable, whether just because of that every class instance should depend on having a Num instance as well.

I think discussing creating another class for satSucc and satPred is out-of-scope here.

¹ Unless you're talking about boundary cases where the default implementation does not actually satisfy the laws, but then I don't understand why you bring it up.

clash-prelude/src/Clash/Class/Finite/Internal.hs

clash-prelude/src/Clash/Num/Zeroing.hs

clash-prelude/src/Clash/Num/Wrapping.hs

clash-prelude/src/Clash/Num/Saturating.hs

clash-prelude/src/Clash/Class/Finite/Internal.hs

martijnbastiaan · 2025-01-01T20:43:18Z

Another thing to consider: there is at least some overlap with Counter I believe. Perhaps Counter's superclass should be Finite?

kleinreact · 2025-01-02T07:24:22Z

Another thing to consider: there is at least some overlap with Counter I believe. Perhaps Counter's superclass should be Finite?

Good point. Making Finite a superclass would be a recognizable API change tough. Also, you technically can have a Counter instance for a type with infinitely many inhabitants, so adding the superclass requirement here would introduce a limitation.

How about adding another deriving strategy for Counter via FiniteDerive instead, like already present for Enum? Then the users can decide on their own, whether counting via the implicit index order of the Finite instance is exactly what they want.

martijnbastiaan · 2025-01-02T12:08:26Z

Making Finite a superclass would be a recognizable API change tough.

I think however we slice it this PR will be an API change, unless we decide to not export it from Prelude. So that's fine with me (provided that there wouldn't be runtime changes).

How about adding another deriving strategy for Counter via FiniteDerive instead, like already present for Enum? Then the users can decide on their own, whether counting via the implicit index order of the Finite instance is exactly what they want.

I think Finite would count the same as Enum for sum-types right? In that case I don't see the benefit of offering both, but I'm also not opposed to it.

clash-prelude/src/Clash/Class/Finite/Internal.hs

clash-prelude/src/Clash/Class/Finite/Internal/TH.hs

clash-prelude/src/Clash/Class/Finite/Internal/Dictionaries.hs

clash-prelude/src/Clash/Class/Finite/Internal/TH.hs

clash-prelude/src/Clash/Class/Finite/Internal.hs

clash-prelude/tests/Clash/Tests/Laws/Finite.hs

DigitalBrains1 · 2025-01-10T19:42:24Z

Could you hide the three internal modules from the Haddock?

Also, I think we should have instances for Clash.Sized.Fixed. I don't know if there are any more instances that were overlooked, but that one occurred to me.

[edit]
That would also give an elegant way to get the next or previous representable value for Fixed. I changed Fixed's Enum instance to be lawful quite some time ago, so it adds or subtracts one on pred or succ. I've come to regret that; we should have documented the deviation, like they subsequently also did with Data.Fixed. Now you have to do stuff like sf . succ . unSF to get the next representable value.
[/edit]

kleinreact · 2025-01-10T19:53:39Z

Could you hide the three internal modules from the Haddock?

👍

[edit]

Also, I think we should have instances for Clash.Sized.Fixed. I don't know if there are any more instances that were overlooked, but that one occurred to me.

I never have used Fixed and don't have much insights into the concept. Maybe we can add that in a later PR.
[/edit]

DigitalBrains1 · 2025-01-10T20:02:35Z

Okay, when this is merged, could you create an issue that we should add the instance?

clash-prelude/src/Clash/Class/Finite/Internal.hs

DigitalBrains1

I had another pass over the Haddock and feel there's still some needed changes.

DigitalBrains1 · 2025-01-31T15:47:45Z

clash-prelude/src/Clash/Class/Finite.hs

+'Bounded' instance) such that 'Enum' instances must ship partial
+functions for most finite types. Likewise, the number of inhabitants
+does not align with the number of indices offered by 'Int' for most
+types, which 'Finite' resolves by using 'Index n' instead.


Suggested change

types, which 'Finite' resolves by using 'Index n' instead.

types, which 'Finite' resolves by using @'Index' n@ instead.

Please check if that fixes the rendering of the Haddock. I think it does, but I'm not sure.

DigitalBrains1 · 2025-01-31T16:01:32Z

clash-prelude/src/Clash/Class/Finite/Internal.hs

+    ) => Vec (ElementCount a) a
+  elements = to <$> gElements
+
+  -- | The @0@ indexed element.


Suggested change

-- | The @0@ indexed element.

-- | The element at index 0.

Just a suggestion... it's just that to me it feels a zero-indexed something is something that has indexes starting at 0, like most arrays and stuff in computer science.

DigitalBrains1 · 2025-01-31T16:02:26Z

clash-prelude/src/Clash/Class/Finite/Internal.hs

+    ) => Maybe a
+  lowestMaybe = to <$> gLowestMaybe
+
+  -- | The @(ElementCount a - 1)@ indexed element


Suggested change

-- | The @(ElementCount a - 1)@ indexed element

-- | The element at index @(ElementCount a - 1)@

At 0 I said "just a suggestion" but I changed my mind. I think

The (ElementCount a - 1) indexed element

is an odd sentence, and I would like it changed. That also means it makes complete sense to change the 0-indexed phrasing.

DigitalBrains1 · 2025-01-31T16:07:52Z

clash-prelude/src/Clash/Class/Finite/Internal.hs

+-- | A newtype wrapper that reverses the index order, which normally
+-- would be used by the 'Finite' instance of the inner type via
+-- 'Generic' deriving. The newtype is only intended be used with the
+#if MIN_VERSION_base(4,15,0)


This does not appear to work. CPP and Haddock do not play nice. I think it works better with the {- construction, but still, you'll have to jump through some hoops and you're probably better off with a little duplication. Otherwise you'll get CPP-generated markers as part of your Haddock.

Please test with GCC versions both matching the #if and the #else.

Note how your documentation ends at "used with the" in the Haddock generated in CI:
https://clash-lang.gitlab.io/-/clash-compiler/-/jobs/8839034866/artifacts/hadocs/clash-prelude/clash-prelude/Clash-Class-Finite.html#t:GenericReverse

DigitalBrains1 · 2025-01-31T16:18:26Z

clash-prelude/src/Clash/Class/Finite.hs

+    -- * Extensions
+  , GenericReverse(..)
+  , WithUndefined(..)


Shouldn't this also list BoundedEnumEq? Right now the only mention of that is at the

(Bounded a, Enum a, Eq a, KnownNat n, 1 <= n) => Finite (BoundedEnumEq n a)

instance, and if you then click

see BoundedEnumEq

you're taken to the Internal module. I don't think we should ever say "see the internal module" in our doc.

kleinreact added enhancement needs-review labels Dec 30, 2024

kleinreact force-pushed the finite-class branch 5 times, most recently from 540afcf to 4d3695c Compare December 30, 2024 18:54

martijnbastiaan reviewed Dec 30, 2024

View reviewed changes

kleinreact force-pushed the finite-class branch 8 times, most recently from 7a1399a to 1130232 Compare January 1, 2025 19:16

kleinreact force-pushed the finite-class branch 2 times, most recently from 9564261 to 80dc978 Compare January 2, 2025 07:17

kleinreact force-pushed the finite-class branch 3 times, most recently from decaec3 to c8821c4 Compare January 7, 2025 07:55

leonschoorl reviewed Jan 7, 2025

View reviewed changes

kleinreact force-pushed the finite-class branch from c8821c4 to 042a148 Compare January 8, 2025 07:26

martijnbastiaan reviewed Jan 8, 2025

View reviewed changes

clash-prelude/tests/Clash/Tests/Laws/Finite.hs Outdated Show resolved Hide resolved

kleinreact force-pushed the finite-class branch 3 times, most recently from cb4795a to 8aeab59 Compare January 10, 2025 08:36

kleinreact force-pushed the finite-class branch 3 times, most recently from 645d9fa to 2752731 Compare January 10, 2025 17:01

kleinreact force-pushed the finite-class branch 2 times, most recently from ce12c7a to 3719e4a Compare January 10, 2025 19:52

kleinreact force-pushed the finite-class branch from 3719e4a to de1af6f Compare January 11, 2025 02:56

DigitalBrains1 reviewed Jan 13, 2025

View reviewed changes

clash-prelude/src/Clash/Class/Finite/Internal.hs Show resolved Hide resolved

DigitalBrains1 reviewed Jan 13, 2025

View reviewed changes

clash-prelude/src/Clash/Class/Finite/Internal.hs Show resolved Hide resolved

kleinreact force-pushed the finite-class branch from de1af6f to e8cf2ec Compare January 13, 2025 16:45

kleinreact added 2 commits January 13, 2025 18:25

Add Finite class

461310b

Add tests for Finite laws

bbf0415

kleinreact force-pushed the finite-class branch from e8cf2ec to bbf0415 Compare January 13, 2025 17:25

DigitalBrains1 requested changes Jan 31, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add Finite class #2858

Add Finite class #2858

kleinreact commented Dec 30, 2024 •

edited

Loading

martijnbastiaan left a comment

martijnbastiaan Dec 30, 2024

kleinreact Dec 31, 2024

DigitalBrains1 Dec 31, 2024 •

edited

Loading

DigitalBrains1 Dec 31, 2024

gergoerdi Dec 31, 2024

kleinreact Jan 10, 2025

DigitalBrains1 Jan 10, 2025 •

edited

Loading

kleinreact Jan 10, 2025

kleinreact Jan 10, 2025 •

edited

Loading

DigitalBrains1 Jan 10, 2025

martijnbastiaan commented Jan 1, 2025

kleinreact commented Jan 2, 2025

martijnbastiaan commented Jan 2, 2025

DigitalBrains1 commented Jan 10, 2025 •

edited

Loading

kleinreact commented Jan 10, 2025 •

edited

Loading

DigitalBrains1 commented Jan 10, 2025

DigitalBrains1 left a comment

DigitalBrains1 Jan 31, 2025

DigitalBrains1 Jan 31, 2025

DigitalBrains1 Jan 31, 2025

DigitalBrains1 Jan 31, 2025

DigitalBrains1 Jan 31, 2025

DigitalBrains1 Jan 31, 2025

	types, which 'Finite' resolves by using 'Index n' instead.
	types, which 'Finite' resolves by using @'Index' n@ instead.

	-- \| The @(ElementCount a - 1)@ indexed element
	-- \| The element at index @(ElementCount a - 1)@

Add Finite class #2858

Are you sure you want to change the base?

Add Finite class #2858

Conversation

kleinreact commented Dec 30, 2024 • edited Loading

Requires

Still TODO:

martijnbastiaan left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

DigitalBrains1 Dec 31, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

DigitalBrains1 Jan 10, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kleinreact Jan 10, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

martijnbastiaan commented Jan 1, 2025

kleinreact commented Jan 2, 2025

martijnbastiaan commented Jan 2, 2025

DigitalBrains1 commented Jan 10, 2025 • edited Loading

kleinreact commented Jan 10, 2025 • edited Loading

DigitalBrains1 commented Jan 10, 2025

DigitalBrains1 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kleinreact commented Dec 30, 2024 •

edited

Loading

DigitalBrains1 Dec 31, 2024 •

edited

Loading

DigitalBrains1 Jan 10, 2025 •

edited

Loading

kleinreact Jan 10, 2025 •

edited

Loading

DigitalBrains1 commented Jan 10, 2025 •

edited

Loading

kleinreact commented Jan 10, 2025 •

edited

Loading