Copyright | (C) 2024-2025 Felix Klein |
---|---|
License | MIT (see the file LICENSE) |
Maintainer | Felix Klein <felix@qbaylogic.com> |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Clash.Class.Finite
Description
The class of types holding only a finite number of elements. The
Finite
class offers type level access to the number of elements n
and defines a total order on the elements via indexing them from 0
to n-1
. Therewith, it gives access to the vector of all inhabitants
of the type and allows to iterate over them in order or to map them back
and forth between their associated indices.
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.
In comparison, Finite
is well suited for types holding finitely many
elements, while the Enum
class is better suited for types with
infinitely many inhabitants. The type of
clearly reflects this design choice, as it assumes that
every element has a successor and predecessor, which makes perfect
sense for infinite types, but requires finite types to error on
certain inputs. Wrapping behavior is forbidden according to the
documentation of succ
, pred
:: Enum
a
=> a -> aEnum
(assuming that finite types usually have a
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
instead.Index
n
Synopsis
- class KnownNat (ElementCount a) => Finite a where
- type ElementCount a :: Nat
- elements :: Vec (ElementCount a) a
- lowest :: 1 <= ElementCount a => a
- lowestMaybe :: Maybe a
- highest :: 1 <= ElementCount a => a
- highestMaybe :: Maybe a
- predMaybe :: a -> Maybe a
- succMaybe :: a -> Maybe a
- ith :: Index (ElementCount a) -> a
- index :: a -> Index (ElementCount a)
- elementsFrom :: (n + 1) <= ElementCount a => SNat n -> Vec (ElementCount a - n) a
- elementsFromTo :: ((n + 1) <= ElementCount a, n <= m, (m + 1) <= ElementCount a) => SNat n -> SNat m -> Vec ((m - n) + 1) a
- class KnownNat (GElementCount rep) => GFinite rep where
- type GElementCount rep :: Nat
- gElements :: Vec (GElementCount rep) (rep a)
- gLowest :: 1 <= GElementCount rep => rep a
- gLowestMaybe :: Maybe (rep a)
- gHighest :: 1 <= GElementCount rep => rep a
- gHighestMaybe :: Maybe (rep a)
- gPredMaybe :: rep a -> Maybe (rep a)
- gSuccMaybe :: rep a -> Maybe (rep a)
- gIth :: Index (GElementCount rep) -> rep a
- gIndex :: rep a -> Index (GElementCount rep)
- newtype GenericReverse a = GenericReverse {
- getGenericReverse :: a
- newtype WithUndefined a = WithUndefined {
- getWithUndefined :: a
- newtype FiniteDerive a = FiniteDerive {
- getFiniteDerive :: a
- newtype BoundedEnumEq (n :: Nat) a = BoundedEnumEq {
- getBoundedEnumEq :: a
Finite Class
class KnownNat (ElementCount a) => Finite a where Source #
The class of types holding only a finite number of elements.
The class supports generic deriving, i.e., for custom types the
class instances can be derived via derive (Generic, Finite)
requiring that all inner types of the type declaration have
Finite
instances as well.
>>>
data T = B Bit | D (Index 2) (Signed 1) deriving (Generic, Finite, Show)
>>>
natToNum @(ElementCount T)
6>>>
elements @T
B 0 :> B 1 :> D 0 -1 :> D 0 0 :> D 1 -1 :> D 1 0 :> Nil>>>
lowestMaybe @T
Just (B 0)>>>
highestMaybe @T
Just (D 1 0)>>>
succMaybe (B 1)
Just (D 0 -1)>>>
predMaybe (B 0)
Nothing>>>
index (D 0 0)
3>>>
ith @T 5
D 1 0
Any definition must satisfy the following laws (automatically ensured when generic deriving the instance):
- Index Order
index
<$>
elements =indicesI
- Forward Iterate
iterateI
(>>=
succMaybe) (lowestMaybe @a) =Just
<$>
(elements @a)- Backward Iterate
iterateI
(>>=
predMaybe) (highestMaybe @a) =Just
<$>
reverse
(elements @a)- Index Isomorphism
ith (index x) = x
- Minimum Predecessor
lowestMaybe
>>=
predMaybe =Nothing
- Maximum Successor
highestMaybe
>>=
succMaybe =Nothing
- Extremes
ElementCount a = 0: lowestMaybe @a =
Nothing
, highestMaybe @a =Nothing
ElementCount a > 0: lowestMaybe @a =
Just
lowest, highestMaybe @a =Just
highest
If a
has a Bounded
instance, it further must satisfy:
If a
has an Enum
instance, it further must satisfy:
Minimal complete definition
Nothing
Associated Types
type ElementCount a :: Nat Source #
The number of elements of the type.
type ElementCount a = GElementCount (Rep a)
Methods
elements :: Vec (ElementCount a) a Source #
The elements of the type.
default elements :: (Generic a, GFinite (Rep a), ElementCount a ~ GElementCount (Rep a)) => Vec (ElementCount a) a Source #
lowest :: 1 <= ElementCount a => a Source #
The element at index 0
.
default lowest :: (Generic a, GFinite (Rep a), ElementCount a ~ GElementCount (Rep a)) => 1 <= ElementCount a => a Source #
lowestMaybe :: Maybe a Source #
Just the element at index 0. Nothing, if ElementCount a = 0
.
highest :: 1 <= ElementCount a => a Source #
The element at index (ElementCount a - 1)
.
default highest :: (Generic a, GFinite (Rep a), ElementCount a ~ GElementCount (Rep a)) => 1 <= ElementCount a => a Source #
highestMaybe :: Maybe a Source #
Just the element at index (ElementCount a - 1)
. Nothing, if
ElementCount a = 0
.
predMaybe :: a -> Maybe a Source #
Just the element before the given one according to the associated index order with the lowest one being the only element that has no predecessor.
succMaybe :: a -> Maybe a Source #
Just the element after the given one according to the associated index order with the highest one being the only element that has no successor.
ith :: Index (ElementCount a) -> a Source #
Maps from an index to the associated element.
default ith :: (Generic a, GFinite (Rep a), ElementCount a ~ GElementCount (Rep a)) => Index (ElementCount a) -> a Source #
index :: a -> Index (ElementCount a) Source #
Maps an element of the type to it's associated index.
default index :: (Generic a, GFinite (Rep a), ElementCount a ~ GElementCount (Rep a)) => a -> Index (ElementCount a) Source #
elementsFrom :: (n + 1) <= ElementCount a => SNat n -> Vec (ElementCount a - n) a Source #
Returns the suffix slice of elements
starting at the index
provided via the SNat
argument.
elementsFromTo :: ((n + 1) <= ElementCount a, n <= m, (m + 1) <= ElementCount a) => SNat n -> SNat m -> Vec ((m - n) + 1) a Source #
Returns the infix slice of elements
from the index provided
via the first SNat
argument to the index provided via the
second one.
Instances
class KnownNat (GElementCount rep) => GFinite rep where Source #
Associated Types
type GElementCount rep :: Nat Source #
Methods
gElements :: Vec (GElementCount rep) (rep a) Source #
gLowest :: 1 <= GElementCount rep => rep a Source #
gLowestMaybe :: Maybe (rep a) Source #
gHighest :: 1 <= GElementCount rep => rep a Source #
gHighestMaybe :: Maybe (rep a) Source #
gPredMaybe :: rep a -> Maybe (rep a) Source #
gSuccMaybe :: rep a -> Maybe (rep a) Source #
gIth :: Index (GElementCount rep) -> rep a Source #
gIndex :: rep a -> Index (GElementCount rep) Source #
Instances
Extensions
newtype GenericReverse a Source #
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
DerivingVia
strategy and custom data types, while you should use
Down
in any other case introducing equivalent behavior.
The reason why we introduce an additional newtype to
Down
here results from how generics play together with
via deriving strategies. For example, if you like to have an
with a reversed index order, then you can introduce a
newtype for that and derive the Signed
nFinite
instance via
Down
, e.g.,
newtype DownSigned n = DownSigned (Signed n) deriving newtype (Generic) deriving via Down (Signed n) instance KnownNat n => Finite (DownSigned)
However, if you create your own new data type T
, then it might be
desirable to use a reversed order right for that type T
and not
. However, the following does not workDown
T
data T = A (DownSigned 3) | B Bool deriving (Generic) deriving via Down T instance Finite T
as in this case the deriving strategy already requires an Finite
instance for T
. The issue is resolved by using
GenericReverse
instead.
deriving via GenericReverse T instance Finite T
Constructors
GenericReverse | |
Fields
|
Instances
newtype WithUndefined a Source #
The elements of the Bit
and BitVector
types may have
undefined bits, which are not in scope when using their default
Finite
class instances. The default instances only consider the
synthesizable fragment of the types, while for simulation or
testing purposes, it may be useful to have access to the range of
undefined inhabitants as well.
The Finite
instances of WithUndefined Bit
and WithUndefined
(BitVector n)
also add the elements containing undefined bits, but
are not synthesizable as a consequence. They make use of a
special index order, that first enumerates all well-defined values,
i.e., those that have no undefined bits, and then continues with
the non-well-defined ones.
>>>
elements @(BitVector 2)
0b00 :> 0b01 :> 0b10 :> 0b11 :> Nil
>>>
elements @(WithUndefined (BitVector 2))
0b00 :> 0b01 :> 0b10 :> 0b11 :> 0b0. :> 0b1. :> 0b.0 :> 0b.1 :> 0b.. :> Nil
Constructors
WithUndefined | |
Fields
|
Instances
Deriving Helpers
newtype FiniteDerive a Source #
A newtype wrapper for implementing deriving strategies of classes
whose implementation may follow from Finite
, e.g., the Enum
class.
Constructors
FiniteDerive | |
Fields
|
Instances
(Finite a, 1 <= ElementCount a) => Bounded (FiniteDerive a) Source # | |
Defined in Clash.Class.Finite.Internal | |
Finite a => Enum (FiniteDerive a) Source # | |
Defined in Clash.Class.Finite.Internal Methods succ :: FiniteDerive a -> FiniteDerive a # pred :: FiniteDerive a -> FiniteDerive a # toEnum :: Int -> FiniteDerive a # fromEnum :: FiniteDerive a -> Int # enumFrom :: FiniteDerive a -> [FiniteDerive a] # enumFromThen :: FiniteDerive a -> FiniteDerive a -> [FiniteDerive a] # enumFromTo :: FiniteDerive a -> FiniteDerive a -> [FiniteDerive a] # enumFromThenTo :: FiniteDerive a -> FiniteDerive a -> FiniteDerive a -> [FiniteDerive a] # |
newtype BoundedEnumEq (n :: Nat) a Source #
A newtype wrapper for deriving Finite instances from existing
instances of Bounded
, Enum
, and Eq
, where Eq
is only
utilized for efficiency reasons although it is not strictly
necessary.
Constructors
BoundedEnumEq | |
Fields
|