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?

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.

IMO this again reinforces my point: base's Prelude (+Haskell itself) already squats an uncomfortable number of identifiers. Another point is that I don't really like synonyms. I can basically never remember whether to use min or minimum for example, I'd have the same problems with succ and next. (Though TBF I've used succ so many times now that I'd recognize next as the newer identifier, but I think my point is clear.)

fpred / fsucc makes sense to me.

Thanks for the feedback and all the suggestions. I like to change it to nextElement and previousElement then, which I still consider intuitive and recognizable.

While fpred and fsucc are nice and short, they still might be mixed up with their Enum counterparts, which I'd prefer to avoid.

I agree with fpred/fsucc.

I changed the function names to before and after now, as I just didn't feel comfortable with the options discussed so far (except before and after, as suggested by @DigitalBrains1).

Thanks for the feedback and all the suggestions. I like to change it to nextElement and previousElement then, which I still consider intuitive and recognizable.

This suffers from the same synonym (min vs minimum) issue I mentioned.

Edit: didn't see your message after. Though before and after still do. I don't get what's so bad about fpred/fsucc? At least 3 people in this thread seem to be fine with it.

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

martijnbastiaan · 2024-12-30T20:18:16Z

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

+-- [Index Order]
+--   @ index '<$>' elements = 'indicesI' @
+-- [Forward Iterate]
+--   @ 'iterateI' ('>>=' next) (lowest \@a) = 'Just' '<$>' (elements \@a) @
+-- [Backward Iterate]
+--   @ 'iterateI' ('>>=' prev) (highest \@a) = 'Just' '<$>' (elements \@a) @
+-- [Index Isomorphism]
+--   @ith (index x) = x@
+-- [Minimum Predecessor]
+--   @ lowest '>>=' prev = 'Nothing' @
+-- [Maximum Successor]
+--   @ highest '>>=' next = 'Nothing' @
+-- [No Uninhabited Extremes]
+--   @ lowest \@a = 'Nothing' /and/ highest \@a = 'Nothing'
+--     /if and only if/ ElementCount a = 0 @


Would it be sensible to add hedgehog laws for this? Could these be added to the test suite for the types that derive / define an instance?

Definitely! It's just not necessary at the current code reviewing stage IMO. Hence, I considered it to be a nice addition for a later stage. I also tested all of the features in REPL already ™️.

I added the demanded tests.

Note that #2871 is required for the tests to run in a reasonable amount of time.

martijnbastiaan · 2024-12-30T20:21:10Z

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

+-- In general, the class can be considered as a more hardware-friendly
+-- alternative to 'Bounded' and 'Enum', utilizing 'Index' instead of
+-- 'Int' and vectors instead of lists.


Is there a reason that we don't provide FiniteEnum (or CEnum) directly? This would give developers an immediate intuition for what the classes are.

Related: I've wondered many times whether it would be sensible for Clash.Prelude to export a Clash-friendly version of all these Int/Integer based APIs. I.e., replace base's Enum (and friends) in favor of Clash ones.

I would not change the semantics of the classes that are already available in base, because this only leads to trouble and confusion. The right strategy should be to provide hardware-friendy alternatives, like Signed n is to be preferred over Int in hardware, which then can coexist with the software-friendly types.

Most of the design choices for this extension have been inspired by my finite library for sure, where I considered it more useful to have a single class covering all of the properties of a "finite" type, instead of breaking things up into multiple classes like Enum or Bounded, which definitely makes sense for types with infinitely many inhabitants.

I'd also like to avoid to make the interface here too similar to Enum and friends, because there still are some fundamental differences, which could be mixed up easily otherwise.

Most of the design choices for this extension have been inspired by my finite library for sure, where I considered it more useful to have a single class covering all of the properties of a "finite" type, instead of breaking things up into multiple classes like Enum or Bounded, which definitely makes sense for types with infinitely many inhabitants.

I'd also like to avoid to make the interface here too similar to Enum and friends, because there still are some fundamental differences, which could be mixed up easily otherwise.

Could you please elaborate? Both Enum and Bounded are mentioned in the documentation, but their relation (or rather differences) aren't clear to me. What makes them good classes for "infinite" types, but not for "finite" types?

Enum

Already the type of succ, pred :: Enum a => a -> a assumes that every element has successor and predecessor, which makes perfect sense for infinite types, but requires finite types to error on certain inputs. Note that wrapping behavior is disallowed according to the documentation of base.

As a consequence, Enum instances must ship partial functions for most finite types.

The same way, using Int as the index type creates a natural mismatch between the number of inhabitants of the index type with the ones of the indexed type. For infinite types, that's "kind of ok", because here the practical assumption is that Int ~ Integer, i.e., we never enumerate stuff that won't fit into into an Int anyway, but that's just an efficiency trade off in the end.

Generic deriving for Enum is only supported for sum data types, but they cannot contain any products (because that doesn't work out with infinite types), which is kind of a strange conceptual mix between the two worlds.

Bounded

The class is often used to identify the bounds of finite types, but just having a minBound and a maxBound does not automatically make your type finite, e.g. the interval [0,1] over the reals has a minBound and maxBound too, but is infinite.

The Bounded class doesn't support uninhabited types like Void or Index 0, which makes it kind of incomplete for me. Though, I think it depends on how you look at it. Nevertheless, having to exclude the Index 0 case just because of that turns out to be non-elegant in then end.

Gotcha, I think some of this should make it into the documentation. I'm not opposed to "large" classes btw.

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.

leonschoorl · 2025-01-07T12:47:54Z

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

+  index f  = index (f . ith <$> indicesI)
+
+-- | A newtype wrapper, which reverses the index order used by the
+-- finite instance of the inner type.


Suggested change

-- finite instance of the inner type.

-- 'Finite' instance of the inner type.

leonschoorl · 2025-01-07T13:49:08Z

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

+#if MIN_VERSION_base(4,16,0)
+  DecsQ
+deriveFiniteTuples finiteName = do
+  let finite = ConT finiteName
+  allNames <- replicateM maxTupleSize $ newName "a"
+
+  forM [3..maxTupleSize] $ \tupleNum -> do
+    let names = take tupleNum allNames
+        vs = case map VarT names of
+                (z:zs) -> (z:zs)
+                _ -> error "maxTupleSize < 3"
+        tuple xs = foldl' AppT (TupleT $ length xs) xs
+
+        -- Instance declaration
+        context = AppT finite . VarT <$> names
+        instTy = AppT finite $ tuple vs
+
+    return $ InstanceD Nothing context instTy []
+#else


I was confused why there was this difference between version.
And why there was a difference for the 2-tuple instance.

I guess for the older base you ran into problems that the Generic instances only go up to 7-tuples.
But even for the latest base Generic instances only seem to be defined up to 15-tuples.
So I think that means we need the more complex version even on newer version if maxTuplesSize is increased past 15 by enabling large-tuples.

leonschoorl · 2025-01-07T16:34:34Z

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

+powGTZero ::
+  forall (n :: Nat) (m :: Nat).
+  Dict (1 <= n^m)
+powGTZero = unsafeCoerce (Dict :: Dict (0 <= 0))


This isn't true when n = 0:
0^m = 0 (for every m /= 0)

leonschoorl · 2025-01-07T18:17:26Z

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

+  highestName beforeName afterName ithName indexName = do
+    let finite = ConT finiteName
+        elementCount = ConT elementCountName
+        times = ConT $ mkName "*"


Suggested change

times = ConT $ mkName "*"

times = ConT ''(*)

Along with import GHC.TypeNats (type (*))

leonschoorl · 2025-01-07T18:38:38Z

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

+  elements = to <$> gElements
+
+  -- | Just the @0@ indexed element. Nothing if @ElementCount a = 0@.
+  lowest :: Maybe a


I'm a bit conflicted about the Maybe on lowest and highest.
As in practice it seems a bit annoying.
And I'm unsure how useful Finite instances for empty types are.
But it is cool that elements @(Either (Maybe Bool) Void) is just a vector with only Lefts and no Rights.

leonschoorl · 2025-01-07T18:51:11Z

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

+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}
+


Suggested change

{-# OPTIONS_HADDOCK not-home #-}

Adding this should result in haddock links going to Clash.Class.Finite instead, where you have the nice extra module documentation.

leonschoorl · 2025-01-07T18:57:31Z

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

+-- Any definition must satisfy the following laws (automatically
+-- ensured when generic deriving the instance):
+--
+-- [Index Order]
+--   @ index '<$>' elements = 'indicesI' @
+-- [Forward Iterate]
+--   @ 'iterateI' ('>>=' after) (lowest \@a) = 'Just' '<$>' (elements \@a) @
+-- [Backward Iterate]
+--   @ 'iterateI' ('>>=' before) (highest \@a)
+--      = 'Just' '<$>' 'reverse' (elements \@a) @
+-- [Index Isomorphism]
+--   @ith (index x) = x@
+-- [Minimum Predecessor]
+--   @ lowest '>>=' before = 'Nothing' @
+-- [Maximum Successor]
+--   @ highest '>>=' after = 'Nothing' @
+-- [No Uninhabited Extremes]
+--   @ lowest \@a = 'Nothing' /and/ highest \@a = 'Nothing'
+--     /if and only if/ ElementCount a = 0 @


I wonder if it makes sense to add something like:

-- If this type is also a `Bounded` instance, it should satisfy: -- @ lowest = Just minBound @ -- @ highest = Just maxBound @

This would make the current instance of Down unlawful.

But maybe that's a good thing.
The whole thing of Down is that it flips things like Ord,Bounded,Enum, so it probably makes sense that it flips the Finite ordering too.
You could derive the Down instance via ReversedIndexOrder, or alternatively drop ReversedIndexOrder and rely on Down instead.

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 2 times, most recently from a0517a0 to decaec3 Compare January 6, 2025 09:23

kleinreact added 2 commits January 7, 2025 08:53

Add Finite class

9dc2bcb

Add tests for Finite laws

c8821c4

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

leonschoorl reviewed Jan 7, 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

martijnbastiaan Jan 1, 2025

kleinreact Jan 1, 2025

DigitalBrains1 Jan 1, 2025

kleinreact Jan 1, 2025 •

edited

Loading

martijnbastiaan Jan 1, 2025 •

edited

Loading

martijnbastiaan Dec 30, 2024

kleinreact Dec 31, 2024

kleinreact Jan 6, 2025

martijnbastiaan Dec 30, 2024

kleinreact Dec 31, 2024

martijnbastiaan Jan 1, 2025

kleinreact Jan 1, 2025

martijnbastiaan Jan 1, 2025

martijnbastiaan commented Jan 1, 2025

kleinreact commented Jan 2, 2025

martijnbastiaan commented Jan 2, 2025

leonschoorl Jan 7, 2025

leonschoorl Jan 7, 2025

leonschoorl Jan 7, 2025

leonschoorl Jan 7, 2025

leonschoorl Jan 7, 2025

leonschoorl Jan 7, 2025

leonschoorl Jan 7, 2025

	-- finite instance of the inner type.
	-- 'Finite' instance of the inner type.

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kleinreact Jan 1, 2025 • edited Loading

Choose a reason for hiding this comment

martijnbastiaan Jan 1, 2025 • 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

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

martijnbastiaan commented Jan 1, 2025

kleinreact commented Jan 2, 2025

martijnbastiaan commented Jan 2, 2025

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

kleinreact Jan 1, 2025 •

edited

Loading

martijnbastiaan Jan 1, 2025 •

edited

Loading