Copyright  (C) Koz Ross 20192020 

License  GPL version 3.0 or later 
Maintainer  koz.ross@retrofreedom.nz 
Stability  Experimental 
Portability  GHC only 
Safe Haskell  Trustworthy 
Language  Haskell2010 
This package provides the Finitary
type class, a range of useful
'base' instances for commonlyused finitary types, and some helper
functions for enumerating values of types with Finitary
instances.
For your own types, there are three possible ways to define an instance of
Finitary
:
Via Generic
If your data type implements Generic
(and is finitary), you can
automatically derive your instance:
{# LANGUAGE DeriveAnyClass #} {# LANGUAGE DeriveGeneric #} {# LANGUAGE DerivingStrategies #} import Data.Finitary (Finitary) import Data.Word (Word8, Word16) import GHC.Generics (Generic) data Foo = Bar  Baz (Word8, Word8)  Quux Word16 deriving stock (Eq, Generic) deriving anyclass (Finitary)
This is the easiest method, and also the safest, as GHC will automatically
determine the cardinality of Foo
, as well as defining lawabiding methods.
It may be somewhat slower than a 'handrolled' method in some cases.
By defining only Cardinality
, fromFinite
and toFinite
If you want a manuallydefined instance, but don't wish to define every
method, only fromFinite
and toFinite
are needed, along with
Cardinality
. Cardinality
in particular must be defined with care, as
otherwise, you may end up with inconstructable values or indexes that don't
correspond to anything.
By defining everything
For maximum control, you can define all the methods. Ensure you follow all the laws!
Synopsis
 class (Eq a, KnownNat (Cardinality a)) => Finitary (a :: Type) where
 type Cardinality a :: Nat
 fromFinite :: Finite (Cardinality a) > a
 toFinite :: a > Finite (Cardinality a)
 start :: 1 <= Cardinality a => a
 end :: 1 <= Cardinality a => a
 previous :: a > Maybe a
 next :: a > Maybe a
 inhabitants :: forall (a :: Type). Finitary a => [a]
 inhabitantsFrom :: forall (a :: Type). Finitary a => a > NonEmpty a
 inhabitantsTo :: forall (a :: Type). Finitary a => a > NonEmpty a
 inhabitantsFromTo :: forall (a :: Type). Finitary a => a > a > [a]
Documentation
class (Eq a, KnownNat (Cardinality a)) => Finitary (a :: Type) where Source #
Witnesses an isomorphism between a
and some (KnownNat n) => Finite n
.
Effectively, a lawful instance of this shows that a
has exactly n
(non__
) inhabitants, and that we have a bijection with fromFinite
and
toFinite
as each 'direction'.
For any type a
with an instance of Finitary
, for every non__
x :: a
, we have
a unique index i :: Finite n
. We will also refer to any such x
as an
inhabitant of a
. We can convert inhabitants to indexes using toFinite
,
and also convert indexes to inhabitants with fromFinite
.
Laws
The main laws state that fromFinite
should be a bijection, with toFinite
as
its inverse, and Cardinality
must be a truthful representation of the
cardinality of the type. Thus:
 \[\texttt{fromFinite} \circ \texttt{toFinite} = \texttt{toFinite} \circ \texttt{fromFinite} = \texttt{id}\]
 \[\forall x, y :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \; \texttt{fromFinite} \; x = \texttt{fromFinite} \; y \rightarrow x = y\]
 \[\forall x :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \; \exists y :: a \mid \texttt{fromFinite} \; x = y\]
Furthermore, fromFinite
should be _orderpreserving_. Namely, if a
is an
instance of Ord
, we must have:
 \[\forall i, j :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \; \texttt{fromFinite} \; i \leq \texttt{fromFinite} \; j \rightarrow i \leq j \]
Lastly, if you define any of the other methods, these laws must hold:
 \[ a \neq \emptyset \rightarrow \texttt{start} :: a = \texttt{fromFinite} \; \texttt{minBound} \]
 \[ a \neq \emptyset \rightarrow \texttt{end} :: a = \texttt{fromFinite} \; \texttt{maxBound} \]
 \[ \forall x :: a \; \texttt{end} :: a \neq x \rightarrow \texttt{next} \; x = (\texttt{fromFinite} \circ + 1 \circ \texttt{toFinite}) \; x \]
 \[ \forall x :: a \; \texttt{start} :: a \neq x \rightarrow \texttt{previous} \; x = (\texttt{fromFinite} \circ  1 \circ \texttt{toFinite}) \; x \]
Together with the fact that Finite n
is wellordered whenever KnownNat n
holds, a lawabiding Finitary
instance for a type a
defines a constructive
wellorder, witnessed by
toFinite
and fromFinite
, which agrees with the Ord
instance for a
, if
any.
We strongly suggest that fromFinite
and toFinite
should have
time complexity \(\Theta(1)\), or, if that's not possible, \(O(\texttt{Cardinality} \; a)\).
The latter is the case for instances generated using
Generics
based derivation, but not for 'basic' types; thus, these
functions for your derived types will only be as slow as their 'structure',
rather than their 'contents', provided the contents are of these 'basic'
types.
Nothing
type Cardinality a :: Nat Source #
How many (non__
) inhabitants a
has, as a typelevel natural number.
type Cardinality a = GCardinality (Rep a)
fromFinite :: Finite (Cardinality a) > a Source #
Converts an index into its corresponding inhabitant.
default fromFinite :: (Generic a, GFinitary (Rep a), Cardinality a ~ GCardinality (Rep a)) => Finite (Cardinality a) > a Source #
toFinite :: a > Finite (Cardinality a) Source #
Converts an inhabitant to its corresponding index.
default toFinite :: (Generic a, GFinitary (Rep a), Cardinality a ~ GCardinality (Rep a)) => a > Finite (Cardinality a) Source #
start :: 1 <= Cardinality a => a Source #
The first inhabitant, by index, assuming a
has any inhabitants.
end :: 1 <= Cardinality a => a Source #
The last inhabitant, by index, assuming a
has any inhabitants.
Instances
Finitary Bool Source #  
Finitary Char Source # 

Finitary Int Source # 

Finitary Int8 Source #  
Finitary Int16 Source #  
Defined in Data.Finitary type Cardinality Int16 :: Nat Source #  
Finitary Int32 Source #  
Defined in Data.Finitary type Cardinality Int32 :: Nat Source #  
Finitary Int64 Source #  
Defined in Data.Finitary type Cardinality Int64 :: Nat Source #  
Finitary Ordering Source #  
Defined in Data.Finitary type Cardinality Ordering :: Nat Source #  
Finitary Word Source # 

Finitary Word8 Source #  
Defined in Data.Finitary type Cardinality Word8 :: Nat Source #  
Finitary Word16 Source #  
Defined in Data.Finitary type Cardinality Word16 :: Nat Source #  
Finitary Word32 Source #  
Defined in Data.Finitary type Cardinality Word32 :: Nat Source #  
Finitary Word64 Source #  
Defined in Data.Finitary type Cardinality Word64 :: Nat Source #  
Finitary () Source #  
Finitary Void Source #  
Finitary All Source #  
Finitary Any Source #  
Finitary Bit Source #  
Finitary Bit Source #  
Finitary a => Finitary (Maybe a) Source # 

Defined in Data.Finitary type Cardinality (Maybe a) :: Nat Source #  
Finitary a => Finitary (Min a) Source #  
Defined in Data.Finitary type Cardinality (Min a) :: Nat Source #  
Finitary a => Finitary (Max a) Source #  
Defined in Data.Finitary type Cardinality (Max a) :: Nat Source #  
Finitary a => Finitary (First a) Source #  
Defined in Data.Finitary type Cardinality (First a) :: Nat Source #  
Finitary a => Finitary (Last a) Source #  
Defined in Data.Finitary type Cardinality (Last a) :: Nat Source #  
Finitary a => Finitary (Identity a) Source #  
Defined in Data.Finitary type Cardinality (Identity a) :: Nat Source #  
Finitary a => Finitary (Dual a) Source #  
Defined in Data.Finitary type Cardinality (Dual a) :: Nat Source #  
Finitary a => Finitary (Sum a) Source #  For any 
Defined in Data.Finitary type Cardinality (Sum a) :: Nat Source #  
Finitary a => Finitary (Product a) Source #  
Defined in Data.Finitary type Cardinality (Product a) :: Nat Source #  
Finitary a => Finitary (Down a) Source #  Despite the 
Defined in Data.Finitary type Cardinality (Down a) :: Nat Source #  
KnownNat n => Finitary (Finite n) Source #  Since any type is isomorphic to itself, it follows that a 'valid' 
Defined in Data.Finitary type Cardinality (Finite n) :: Nat Source #  
(Finitary a, Finitary b) => Finitary (Either a b) Source #  The sum of two finite types will also be finite, with a cardinality equal to the sum of their cardinalities. 
Defined in Data.Finitary type Cardinality (Either a b) :: Nat Source #  
(Finitary a, Finitary b) => Finitary (a, b) Source #  The product of two finite types will also be finite, with a cardinality equal to the product of their cardinalities. 
Defined in Data.Finitary type Cardinality (a, b) :: Nat Source #  
Finitary (Proxy a) Source #  
Defined in Data.Finitary type Cardinality (Proxy a) :: Nat Source #  
(Finitary a, KnownNat n) => Finitary (Vector n a) Source #  A fixedlength vector over a type 
Defined in Data.Finitary type Cardinality (Vector n a) :: Nat Source #  
(Finitary a, Storable a, KnownNat n) => Finitary (Vector n a) Source #  
Defined in Data.Finitary type Cardinality (Vector n a) :: Nat Source #  
(Finitary a, Unbox a, KnownNat n) => Finitary (Vector n a) Source #  
Defined in Data.Finitary type Cardinality (Vector n a) :: Nat Source #  
(Finitary a, Finitary b, Finitary c) => Finitary (a, b, c) Source #  
Defined in Data.Finitary type Cardinality (a, b, c) :: Nat Source #  
Finitary a => Finitary (Const a b) Source #  
Defined in Data.Finitary type Cardinality (Const a b) :: Nat Source #  
(Finitary a, Finitary b, Finitary c, Finitary d) => Finitary (a, b, c, d) Source #  
Defined in Data.Finitary type Cardinality (a, b, c, d) :: Nat Source # fromFinite :: Finite (Cardinality (a, b, c, d)) > (a, b, c, d) Source # toFinite :: (a, b, c, d) > Finite (Cardinality (a, b, c, d)) Source # start :: (a, b, c, d) Source #  
(Finitary a, Finitary b, Finitary c, Finitary d, Finitary e) => Finitary (a, b, c, d, e) Source #  
Defined in Data.Finitary type Cardinality (a, b, c, d, e) :: Nat Source #  
(Finitary a, Finitary b, Finitary c, Finitary d, Finitary e, Finitary f) => Finitary (a, b, c, d, e, f) Source #  
Defined in Data.Finitary type Cardinality (a, b, c, d, e, f) :: Nat Source # fromFinite :: Finite (Cardinality (a, b, c, d, e, f)) > (a, b, c, d, e, f) Source # toFinite :: (a, b, c, d, e, f) > Finite (Cardinality (a, b, c, d, e, f)) Source # start :: (a, b, c, d, e, f) Source # end :: (a, b, c, d, e, f) Source # previous :: (a, b, c, d, e, f) > Maybe (a, b, c, d, e, f) Source # next :: (a, b, c, d, e, f) > Maybe (a, b, c, d, e, f) Source # 
Enumeration functions
inhabitants :: forall (a :: Type). Finitary a => [a] Source #
Produce every inhabitant of a
, in ascending order of indexes.
If you want descending order, use Down a
instead.
inhabitantsFrom :: forall (a :: Type). Finitary a => a > NonEmpty a Source #
Produce every inhabitant of a
, starting with the argument, in ascending
order of indexes.
If you want descending order, use Down a
instead.
inhabitantsTo :: forall (a :: Type). Finitary a => a > NonEmpty a Source #
Produce every inhabitant of a
, up to and including the argument, in
ascending order of indexes.
If you want descending order, use Down a
instead.
inhabitantsFromTo :: forall (a :: Type). Finitary a => a > a > [a] Source #
Produce every inhabitant of a
, starting with the first argument, up to
the second argument, in ascending order of indexes. inhabitantsFromTo x y
will produce the empty list if toFinite x > toFinite y
.
If you want descending order, use Down a
instead.