Data.Finitary

This package provides the Finitary type class, a range of useful 'base' instances for commonly-used 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 #-}

import GHC.Generics
import Data.Word

data Foo = Bar | Baz (Word8, Word8) | Quux Word16
   deriving (Eq, Generic, Finitary)

This is the easiest method, and also the safest, as GHC will automatically determine the cardinality of Foo, as well as defining law-abiding methods. It may be somewhat slower than a 'hand-rolled' method in some cases.

By defining only Cardinality, fromFinite and toFinite

If you want a manually-defined 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!

Documentation

class (Eq a, KnownNat (Cardinality a)) => Finitary (a :: Type) where

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 _order-preserving_. 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} = \texttt{fromFinite} \; \texttt{minBound} \]
• \[ a \neq \emptyset \rightarrow \texttt{end} = \texttt{fromFinite} \; \texttt{maxBound} \]
• \[ \forall x :: a \; \texttt{end} \neq x \rightarrow \texttt{next} \; x = (\texttt{fromFinite} \circ + 1 \circ \texttt{toFinite}) \; x \]
• \[ \forall x :: a \; \texttt{start} \neq x \rightarrow \texttt{previous} \; x = (\texttt{fromFinite} \circ - 1 \circ \texttt{toFinite}) \; x \]

Together with the fact that Finite n is well-ordered whenever KnownNat n holds, a law-abiding Finitary instance for a type a defines a constructive well-order, 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.

Minimal complete definition

Nothing

Associated Types

type Cardinality a :: Nat

How many (non-_|_) inhabitants a has, as a typelevel natural number.

type Cardinality a = GCardinality (Rep a)

Methods

fromFinite :: Finite (Cardinality a) -> a

Converts an index into its corresponding inhabitant.

default fromFinite :: (Generic a, GFinitary (Rep a), Cardinality a ~ GCardinality (Rep a)) => Finite (Cardinality a) -> a

toFinite :: a -> Finite (Cardinality a)

Converts an inhabitant to its corresponding index.

default toFinite :: (Generic a, GFinitary (Rep a), Cardinality a ~ GCardinality (Rep a)) => a -> Finite (Cardinality a)

start :: 1 <= Cardinality a => a

The first inhabitant, by index, assuming a has any inhabitants.

end :: 1 <= Cardinality a => a

The last inhabitant, by index, assuming a has any inhabitants.

previous :: Alternative f => a -> f a

previous x gives the inhabitant whose index precedes the index of x, or empty if no such index exists.

next :: Alternative f => a -> f a

next x gives the inhabitant whose index follows the index of x, or empty if no such index exists.

Instances

Finitary Bool

Defined in Data.Finitary

Associated Types

type Cardinality Bool :: Nat

Methods

fromFinite :: Finite (Cardinality Bool) -> Bool

toFinite :: Bool -> Finite (Cardinality Bool)

start :: Bool

end :: Bool

previous :: Alternative f => Bool -> f Bool

next :: Alternative f => Bool -> f Bool

Finitary Char

Char has one inhabitant per Unicode code point.

Defined in Data.Finitary

Associated Types

type Cardinality Char :: Nat

Methods

fromFinite :: Finite (Cardinality Char) -> Char

toFinite :: Char -> Finite (Cardinality Char)

start :: Char

end :: Char

previous :: Alternative f => Char -> f Char

next :: Alternative f => Char -> f Char

Finitary Int

Int has a finite number of inhabitants, varying by platform. This instance will determine this when the library is built.

Defined in Data.Finitary

Associated Types

type Cardinality Int :: Nat

Methods

fromFinite :: Finite (Cardinality Int) -> Int

toFinite :: Int -> Finite (Cardinality Int)

start :: Int

end :: Int

previous :: Alternative f => Int -> f Int

next :: Alternative f => Int -> f Int

Finitary Int8

Defined in Data.Finitary

Associated Types

type Cardinality Int8 :: Nat

Methods

fromFinite :: Finite (Cardinality Int8) -> Int8

toFinite :: Int8 -> Finite (Cardinality Int8)

start :: Int8

end :: Int8

previous :: Alternative f => Int8 -> f Int8

next :: Alternative f => Int8 -> f Int8

Finitary Int16

Defined in Data.Finitary

Associated Types

type Cardinality Int16 :: Nat

Methods

fromFinite :: Finite (Cardinality Int16) -> Int16

toFinite :: Int16 -> Finite (Cardinality Int16)

start :: Int16

end :: Int16

previous :: Alternative f => Int16 -> f Int16

next :: Alternative f => Int16 -> f Int16

Finitary Int32

Defined in Data.Finitary

Associated Types

type Cardinality Int32 :: Nat

Methods

fromFinite :: Finite (Cardinality Int32) -> Int32

toFinite :: Int32 -> Finite (Cardinality Int32)

start :: Int32

end :: Int32

previous :: Alternative f => Int32 -> f Int32

next :: Alternative f => Int32 -> f Int32

Finitary Int64

Defined in Data.Finitary

Associated Types

type Cardinality Int64 :: Nat

Methods

fromFinite :: Finite (Cardinality Int64) -> Int64

toFinite :: Int64 -> Finite (Cardinality Int64)

start :: Int64

end :: Int64

previous :: Alternative f => Int64 -> f Int64

next :: Alternative f => Int64 -> f Int64

Finitary Ordering

Defined in Data.Finitary

Associated Types

type Cardinality Ordering :: Nat

Methods

fromFinite :: Finite (Cardinality Ordering) -> Ordering

toFinite :: Ordering -> Finite (Cardinality Ordering)

start :: Ordering

end :: Ordering

previous :: Alternative f => Ordering -> f Ordering

next :: Alternative f => Ordering -> f Ordering

Finitary Word

Word has a finite number of inhabitants, varying by platform. This instance will determine this when the library is built.

Defined in Data.Finitary

Associated Types

type Cardinality Word :: Nat

Methods

fromFinite :: Finite (Cardinality Word) -> Word

toFinite :: Word -> Finite (Cardinality Word)

start :: Word

end :: Word

previous :: Alternative f => Word -> f Word

next :: Alternative f => Word -> f Word

Finitary Word8

Defined in Data.Finitary

Associated Types

type Cardinality Word8 :: Nat

Methods

fromFinite :: Finite (Cardinality Word8) -> Word8

toFinite :: Word8 -> Finite (Cardinality Word8)

start :: Word8

end :: Word8

previous :: Alternative f => Word8 -> f Word8

next :: Alternative f => Word8 -> f Word8

Finitary Word16

Defined in Data.Finitary

Associated Types

type Cardinality Word16 :: Nat

Methods

fromFinite :: Finite (Cardinality Word16) -> Word16

toFinite :: Word16 -> Finite (Cardinality Word16)

start :: Word16

end :: Word16

previous :: Alternative f => Word16 -> f Word16

next :: Alternative f => Word16 -> f Word16

Finitary Word32

Defined in Data.Finitary

Associated Types

type Cardinality Word32 :: Nat

Methods

fromFinite :: Finite (Cardinality Word32) -> Word32

toFinite :: Word32 -> Finite (Cardinality Word32)

start :: Word32

end :: Word32

previous :: Alternative f => Word32 -> f Word32

next :: Alternative f => Word32 -> f Word32

Finitary Word64

Defined in Data.Finitary

Associated Types

type Cardinality Word64 :: Nat

Methods

fromFinite :: Finite (Cardinality Word64) -> Word64

toFinite :: Word64 -> Finite (Cardinality Word64)

start :: Word64

end :: Word64

previous :: Alternative f => Word64 -> f Word64

next :: Alternative f => Word64 -> f Word64

Finitary ()

Defined in Data.Finitary

Associated Types

type Cardinality () :: Nat

Methods

fromFinite :: Finite (Cardinality ()) -> ()

toFinite :: () -> Finite (Cardinality ())

start :: ()

end :: ()

previous :: Alternative f => () -> f ()

next :: Alternative f => () -> f ()

Finitary Void

Defined in Data.Finitary

Associated Types

type Cardinality Void :: Nat

Methods

fromFinite :: Finite (Cardinality Void) -> Void

toFinite :: Void -> Finite (Cardinality Void)

start :: Void

end :: Void

previous :: Alternative f => Void -> f Void

next :: Alternative f => Void -> f Void

Finitary All

Defined in Data.Finitary

Associated Types

type Cardinality All :: Nat

Methods

fromFinite :: Finite (Cardinality All) -> All

toFinite :: All -> Finite (Cardinality All)

start :: All

end :: All

previous :: Alternative f => All -> f All

next :: Alternative f => All -> f All

Finitary Any

Defined in Data.Finitary

Associated Types

type Cardinality Any :: Nat

Methods

fromFinite :: Finite (Cardinality Any) -> Any

toFinite :: Any -> Finite (Cardinality Any)

start :: Any

end :: Any

previous :: Alternative f => Any -> f Any

next :: Alternative f => Any -> f Any

Finitary Bit

Defined in Data.Finitary

Associated Types

type Cardinality Bit :: Nat

Methods

fromFinite :: Finite (Cardinality Bit) -> Bit

toFinite :: Bit -> Finite (Cardinality Bit)

start :: Bit

end :: Bit

previous :: Alternative f => Bit -> f Bit

next :: Alternative f => Bit -> f Bit

Finitary Bit

Defined in Data.Finitary

Associated Types

type Cardinality Bit :: Nat

Methods

fromFinite :: Finite (Cardinality Bit) -> Bit

toFinite :: Bit -> Finite (Cardinality Bit)

start :: Bit

end :: Bit

previous :: Alternative f => Bit -> f Bit

next :: Alternative f => Bit -> f Bit

Finitary a => Finitary (Maybe a)

Maybe a introduces one additional inhabitant (namely, Nothing) to a.

Defined in Data.Finitary

Associated Types

type Cardinality (Maybe a) :: Nat

Methods

fromFinite :: Finite (Cardinality (Maybe a)) -> Maybe a

toFinite :: Maybe a -> Finite (Cardinality (Maybe a))

start :: Maybe a

end :: Maybe a

previous :: Alternative f => Maybe a -> f (Maybe a)

next :: Alternative f => Maybe a -> f (Maybe a)

Finitary a => Finitary (Min a)

Defined in Data.Finitary

Associated Types

type Cardinality (Min a) :: Nat

Methods

fromFinite :: Finite (Cardinality (Min a)) -> Min a

toFinite :: Min a -> Finite (Cardinality (Min a))

start :: Min a

end :: Min a

previous :: Alternative f => Min a -> f (Min a)

next :: Alternative f => Min a -> f (Min a)

Finitary a => Finitary (Max a)

Defined in Data.Finitary

Associated Types

type Cardinality (Max a) :: Nat

Methods

fromFinite :: Finite (Cardinality (Max a)) -> Max a

toFinite :: Max a -> Finite (Cardinality (Max a))

start :: Max a

end :: Max a

previous :: Alternative f => Max a -> f (Max a)

next :: Alternative f => Max a -> f (Max a)

Finitary a => Finitary (First a)

Defined in Data.Finitary

Associated Types

type Cardinality (First a) :: Nat

Methods

fromFinite :: Finite (Cardinality (First a)) -> First a

toFinite :: First a -> Finite (Cardinality (First a))

start :: First a

end :: First a

previous :: Alternative f => First a -> f (First a)

next :: Alternative f => First a -> f (First a)

Finitary a => Finitary (Last a)

Defined in Data.Finitary

Associated Types

type Cardinality (Last a) :: Nat

Methods

fromFinite :: Finite (Cardinality (Last a)) -> Last a

toFinite :: Last a -> Finite (Cardinality (Last a))

start :: Last a

end :: Last a

previous :: Alternative f => Last a -> f (Last a)

next :: Alternative f => Last a -> f (Last a)

Finitary a => Finitary (Identity a)

Defined in Data.Finitary

Associated Types

type Cardinality (Identity a) :: Nat

Methods

fromFinite :: Finite (Cardinality (Identity a)) -> Identity a

toFinite :: Identity a -> Finite (Cardinality (Identity a))

start :: Identity a

end :: Identity a

previous :: Alternative f => Identity a -> f (Identity a)

next :: Alternative f => Identity a -> f (Identity a)

Finitary a => Finitary (Dual a)

Defined in Data.Finitary

Associated Types

type Cardinality (Dual a) :: Nat

Methods

fromFinite :: Finite (Cardinality (Dual a)) -> Dual a

toFinite :: Dual a -> Finite (Cardinality (Dual a))

start :: Dual a

end :: Dual a

previous :: Alternative f => Dual a -> f (Dual a)

next :: Alternative f => Dual a -> f (Dual a)

Finitary a => Finitary (Sum a)

For any newtype-esque thing over a type with a Finitary instance, we can just 'inherit' the behaviour of a.

Defined in Data.Finitary

Associated Types

type Cardinality (Sum a) :: Nat

Methods

fromFinite :: Finite (Cardinality (Sum a)) -> Sum a

toFinite :: Sum a -> Finite (Cardinality (Sum a))

start :: Sum a

end :: Sum a

previous :: Alternative f => Sum a -> f (Sum a)

next :: Alternative f => Sum a -> f (Sum a)

Finitary a => Finitary (Product a)

Defined in Data.Finitary

Associated Types

type Cardinality (Product a) :: Nat

Methods

fromFinite :: Finite (Cardinality (Product a)) -> Product a

toFinite :: Product a -> Finite (Cardinality (Product a))

start :: Product a

end :: Product a

previous :: Alternative f => Product a -> f (Product a)

next :: Alternative f => Product a -> f (Product a)

Finitary a => Finitary (Down a)

Despite the newtype-esque nature of Down, due to the requirement that fromFinite is order-preserving, the instance for Down a reverses the indexing.

Defined in Data.Finitary

Associated Types

type Cardinality (Down a) :: Nat

Methods

fromFinite :: Finite (Cardinality (Down a)) -> Down a

toFinite :: Down a -> Finite (Cardinality (Down a))

start :: Down a

end :: Down a

previous :: Alternative f => Down a -> f (Down a)

next :: Alternative f => Down a -> f (Down a)

KnownNat n => Finitary (Finite n)

Since any type is isomorphic to itself, it follows that a 'valid' Finite n (meaning that n is a KnownNat) has finite cardinality.

Defined in Data.Finitary

Associated Types

type Cardinality (Finite n) :: Nat

Methods

fromFinite :: Finite (Cardinality (Finite n)) -> Finite n

toFinite :: Finite n -> Finite (Cardinality (Finite n))

start :: Finite n

end :: Finite n

previous :: Alternative f => Finite n -> f (Finite n)

next :: Alternative f => Finite n -> f (Finite n)

(Finitary a, Finitary b) => Finitary (Either a b)

The sum of two finite types will also be finite, with a cardinality equal to the sum of their cardinalities.

Defined in Data.Finitary

Associated Types

type Cardinality (Either a b) :: Nat

Methods

fromFinite :: Finite (Cardinality (Either a b)) -> Either a b

toFinite :: Either a b -> Finite (Cardinality (Either a b))

start :: Either a b

end :: Either a b

previous :: Alternative f => Either a b -> f (Either a b)

next :: Alternative f => Either a b -> f (Either a b)

(Finitary a, Finitary b) => Finitary (a, b)

The product of two finite types will also be finite, with a cardinality equal to the product of their cardinalities.

Defined in Data.Finitary

Associated Types

type Cardinality (a, b) :: Nat

Methods

fromFinite :: Finite (Cardinality (a, b)) -> (a, b)

toFinite :: (a, b) -> Finite (Cardinality (a, b))

start :: (a, b)

end :: (a, b)

previous :: Alternative f => (a, b) -> f (a, b)

next :: Alternative f => (a, b) -> f (a, b)

Finitary (Proxy a)

Defined in Data.Finitary

Associated Types

type Cardinality (Proxy a) :: Nat

Methods

fromFinite :: Finite (Cardinality (Proxy a)) -> Proxy a

toFinite :: Proxy a -> Finite (Cardinality (Proxy a))

start :: Proxy a

end :: Proxy a

previous :: Alternative f => Proxy a -> f (Proxy a)

next :: Alternative f => Proxy a -> f (Proxy a)

(Finitary a, Unbox a, KnownNat n) => Finitary (Vector n a)

Defined in Data.Finitary

Associated Types

type Cardinality (Vector n a) :: Nat

Methods

fromFinite :: Finite (Cardinality (Vector n a)) -> Vector n a

toFinite :: Vector n a -> Finite (Cardinality (Vector n a))

start :: Vector n a

end :: Vector n a

previous :: Alternative f => Vector n a -> f (Vector n a)

next :: Alternative f => Vector n a -> f (Vector n a)

(Finitary a, Storable a, KnownNat n) => Finitary (Vector n a)

Defined in Data.Finitary

Associated Types

type Cardinality (Vector n a) :: Nat

Methods

fromFinite :: Finite (Cardinality (Vector n a)) -> Vector n a

toFinite :: Vector n a -> Finite (Cardinality (Vector n a))

start :: Vector n a

end :: Vector n a

previous :: Alternative f => Vector n a -> f (Vector n a)

next :: Alternative f => Vector n a -> f (Vector n a)

(Finitary a, KnownNat n) => Finitary (Vector n a)

A fixed-length vector over a type a with an instance of Finitary can be thought of as a fixed-length word over an alphabet of size Cardinality a. Since there are only finitely-many of these, we can index them in lex order, with the ordering determined by the Finitary a instance (thus, the 'first' such Vector is the one where each element is start :: a, and the 'last' is the one where each element is end :: a).

Defined in Data.Finitary

Associated Types

type Cardinality (Vector n a) :: Nat

Methods

fromFinite :: Finite (Cardinality (Vector n a)) -> Vector n a

toFinite :: Vector n a -> Finite (Cardinality (Vector n a))

start :: Vector n a

end :: Vector n a

previous :: Alternative f => Vector n a -> f (Vector n a)

next :: Alternative f => Vector n a -> f (Vector n a)

(Finitary a, Finitary b, Finitary c) => Finitary (a, b, c)

Defined in Data.Finitary

Associated Types

type Cardinality (a, b, c) :: Nat

Methods

fromFinite :: Finite (Cardinality (a, b, c)) -> (a, b, c)

toFinite :: (a, b, c) -> Finite (Cardinality (a, b, c))

start :: (a, b, c)

end :: (a, b, c)

previous :: Alternative f => (a, b, c) -> f (a, b, c)

next :: Alternative f => (a, b, c) -> f (a, b, c)

Finitary a => Finitary (Const a b)

Defined in Data.Finitary

Associated Types

type Cardinality (Const a b) :: Nat

Methods

fromFinite :: Finite (Cardinality (Const a b)) -> Const a b

toFinite :: Const a b -> Finite (Cardinality (Const a b))

start :: Const a b

end :: Const a b

previous :: Alternative f => Const a b -> f (Const a b)

next :: Alternative f => Const a b -> f (Const a b)

(Finitary a, Finitary b, Finitary c, Finitary d) => Finitary (a, b, c, d)

Defined in Data.Finitary

Associated Types

type Cardinality (a, b, c, d) :: Nat

Methods

fromFinite :: Finite (Cardinality (a, b, c, d)) -> (a, b, c, d)

toFinite :: (a, b, c, d) -> Finite (Cardinality (a, b, c, d))

start :: (a, b, c, d)

end :: (a, b, c, d)

previous :: Alternative f => (a, b, c, d) -> f (a, b, c, d)

next :: Alternative f => (a, b, c, d) -> f (a, b, c, d)

(Finitary a, Finitary b, Finitary c, Finitary d, Finitary e) => Finitary (a, b, c, d, e)

Defined in Data.Finitary

Associated Types

type Cardinality (a, b, c, d, e) :: Nat

Methods

fromFinite :: Finite (Cardinality (a, b, c, d, e)) -> (a, b, c, d, e)

toFinite :: (a, b, c, d, e) -> Finite (Cardinality (a, b, c, d, e))

start :: (a, b, c, d, e)

end :: (a, b, c, d, e)

previous :: Alternative f => (a, b, c, d, e) -> f (a, b, c, d, e)

next :: Alternative f => (a, b, c, d, e) -> f (a, b, c, d, e)

(Finitary a, Finitary b, Finitary c, Finitary d, Finitary e, Finitary f) => Finitary (a, b, c, d, e, f)

Defined in Data.Finitary

Associated Types

type Cardinality (a, b, c, d, e, f) :: Nat

Methods

fromFinite :: Finite (Cardinality (a, b, c, d, e, f)) -> (a, b, c, d, e, f)

toFinite :: (a, b, c, d, e, f) -> Finite (Cardinality (a, b, c, d, e, f))

start :: (a, b, c, d, e, f)

end :: (a, b, c, d, e, f)

previous :: Alternative f0 => (a, b, c, d, e, f) -> f0 (a, b, c, d, e, f)

next :: Alternative f0 => (a, b, c, d, e, f) -> f0 (a, b, c, d, e, f)

Enumeration functions

inhabitants :: forall (a :: Type). Finitary a => [a]

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

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

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]

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.