finitary-1.0.0.0: A better, more type-safe Enum.
Copyright(C) Koz Ross 2019
LicenseGPL version 3.0 or later
Maintainerkoz.ross@retro-freedom.nz
StabilityExperimental
PortabilityGHC only
Safe HaskellTrustworthy
LanguageHaskell2010

Data.Finitary

Description

This package provides the Finitary type class, as well as a range of useful 'base' instances for commonly-used finitary types.

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!

Synopsis

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 _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 i :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \; \texttt{nextSkipping} \; i = \underbrace{\texttt{next} \circ \ldots \circ \texttt{next}}_{i} \]
  • \[ \forall x :: a \; \texttt{start} \neq x \rightarrow \texttt{previous} \; x = (\texttt{fromFinite} \circ - 1 \circ \texttt{toFinite}) \; x \]
  • \[ \forall i :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \; \texttt{previousSkipping} \; i = \underbrace{\texttt{previous} \circ \ldots \circ \texttt{previous}}_{i} \]
  • \[ \forall x :: a \; \texttt{enumerateFrom} \; x = \texttt{fromFinite <\$> [toFinite} \; x \texttt{..]} \]
  • \[ \forall x, y :: a \; \texttt{enumerateFromThen} \; x y = \texttt{fromFinite <\$> [toFinite} \; x \texttt{, }\; y \texttt{..]} \]
  • \[ \forall x, y :: a \; \texttt{enumerateFromTo} \; x \; y = \texttt{fromFinite <\$> [toFinite} \; x \texttt{..} \; y \texttt{]} \]
  • \[ \forall x, y, z :: a \; \texttt{enumerateFromThenTo} \; x \; y \; z = \texttt{fromFinite <\$> [toFinite} \; x \texttt{,} \; y \texttt{..} \; z \texttt{]} \]

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 Source #

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

type Cardinality a = GCardinality (Rep a) Source #

Methods

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.

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

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

previousSkipping :: Alternative f => Finite (Cardinality a) -> a -> f a Source #

previousSkipping i x 'skips back' i index values from the index of x, then gives the inhabitant whose index precedes the result, or empty if no such index exists.

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

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

nextSkipping :: Alternative f => Finite (Cardinality a) -> a -> f a Source #

nextSkipping i x 'skips forward' i index values from the index of x, then gives the inhabitant whose index follows the result, or empty if no such index exists.

enumerateFrom :: a -> [a] Source #

enumerateFrom x gives a list of inhabitants, starting with x, followed by all other values whose indexes follow x, in index order.

enumerateFromThen :: a -> a -> [a] Source #

Like enumerateFrom, except in steps of toFinite y - toFinite x.

enumerateFromTo :: a -> a -> [a] Source #

enumerateFromTo x y gives a list of inhabitants, starting with x, ending with y, and containing all other values whose indices lie between those of x and y. The list is in index order.

enumerateFromThenTo :: a -> a -> a -> [a] Source #

Like enumerateFromTo, except in steps of toFinite y - toFinite x.

Instances

Instances details
Finitary Bool Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality Bool :: Nat Source #

Finitary Char Source #

Char has one inhabitant per Unicode code point.

Instance details

Defined in Data.Finitary

Associated Types

type Cardinality Char :: Nat Source #

Finitary Int Source #

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

Instance details

Defined in Data.Finitary

Associated Types

type Cardinality Int :: Nat Source #

Finitary Int8 Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality Int8 :: Nat Source #

Finitary Int16 Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality Int16 :: Nat Source #

Finitary Int32 Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality Int32 :: Nat Source #

Finitary Int64 Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality Int64 :: Nat Source #

Finitary Ordering Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality Ordering :: Nat Source #

Finitary Word Source #

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

Instance details

Defined in Data.Finitary

Associated Types

type Cardinality Word :: Nat Source #

Finitary Word8 Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality Word8 :: Nat Source #

Finitary Word16 Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality Word16 :: Nat Source #

Finitary Word32 Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality Word32 :: Nat Source #

Finitary Word64 Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality Word64 :: Nat Source #

Finitary () Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality () :: Nat Source #

Methods

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

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

start :: () Source #

end :: () Source #

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

previousSkipping :: Alternative f => Finite (Cardinality ()) -> () -> f () Source #

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

nextSkipping :: Alternative f => Finite (Cardinality ()) -> () -> f () Source #

enumerateFrom :: () -> [()] Source #

enumerateFromThen :: () -> () -> [()] Source #

enumerateFromTo :: () -> () -> [()] Source #

enumerateFromThenTo :: () -> () -> () -> [()] Source #

Finitary Void Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality Void :: Nat Source #

Finitary All Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality All :: Nat Source #

Finitary Any Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality Any :: Nat Source #

Finitary Bit Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality Bit :: Nat Source #

Finitary Bit Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality Bit :: Nat Source #

Finitary a => Finitary (Maybe a) Source #

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

Instance details

Defined in Data.Finitary

Associated Types

type Cardinality (Maybe a) :: Nat Source #

Finitary a => Finitary (Min a) Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality (Min a) :: Nat Source #

Finitary a => Finitary (Max a) Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality (Max a) :: Nat Source #

Finitary a => Finitary (First a) Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality (First a) :: Nat Source #

Finitary a => Finitary (Last a) Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality (Last a) :: Nat Source #

Finitary a => Finitary (Identity a) Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality (Identity a) :: Nat Source #

Finitary a => Finitary (Dual a) Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality (Dual a) :: Nat Source #

Finitary a => Finitary (Sum a) Source #

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

Instance details

Defined in Data.Finitary

Associated Types

type Cardinality (Sum a) :: Nat Source #

Finitary a => Finitary (Product a) Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality (Product a) :: Nat Source #

Finitary a => Finitary (Down a) Source #

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

Instance details

Defined in Data.Finitary

Associated Types

type Cardinality (Down a) :: Nat Source #

KnownNat n => Finitary (Finite n) Source #

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

Instance details

Defined in Data.Finitary

Associated Types

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.

Instance details

Defined in Data.Finitary

Associated Types

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.

Instance details

Defined in Data.Finitary

Associated Types

type Cardinality (a, b) :: Nat Source #

Methods

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

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

start :: (a, b) Source #

end :: (a, b) Source #

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

previousSkipping :: Alternative f => Finite (Cardinality (a, b)) -> (a, b) -> f (a, b) Source #

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

nextSkipping :: Alternative f => Finite (Cardinality (a, b)) -> (a, b) -> f (a, b) Source #

enumerateFrom :: (a, b) -> [(a, b)] Source #

enumerateFromThen :: (a, b) -> (a, b) -> [(a, b)] Source #

enumerateFromTo :: (a, b) -> (a, b) -> [(a, b)] Source #

enumerateFromThenTo :: (a, b) -> (a, b) -> (a, b) -> [(a, b)] Source #

Finitary (Proxy a) Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality (Proxy a) :: Nat Source #

(Finitary a, Unbox a, KnownNat n) => Finitary (Vector n a) Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality (Vector n a) :: Nat Source #

(Finitary a, Storable a, KnownNat n) => Finitary (Vector n a) Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality (Vector n a) :: Nat Source #

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

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).

Instance details

Defined in Data.Finitary

Associated Types

type Cardinality (Vector n a) :: Nat Source #

(Finitary a, Finitary b, Finitary c) => Finitary (a, b, c) Source # 
Instance details

Defined in Data.Finitary

Associated Types

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

Methods

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

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

start :: (a, b, c) Source #

end :: (a, b, c) Source #

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

previousSkipping :: Alternative f => Finite (Cardinality (a, b, c)) -> (a, b, c) -> f (a, b, c) Source #

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

nextSkipping :: Alternative f => Finite (Cardinality (a, b, c)) -> (a, b, c) -> f (a, b, c) Source #

enumerateFrom :: (a, b, c) -> [(a, b, c)] Source #

enumerateFromThen :: (a, b, c) -> (a, b, c) -> [(a, b, c)] Source #

enumerateFromTo :: (a, b, c) -> (a, b, c) -> [(a, b, c)] Source #

enumerateFromThenTo :: (a, b, c) -> (a, b, c) -> (a, b, c) -> [(a, b, c)] Source #

Finitary a => Finitary (Const a b) Source # 
Instance details

Defined in Data.Finitary

Associated Types

type Cardinality (Const a b) :: Nat Source #

Methods

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

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

start :: Const a b Source #

end :: Const a b Source #

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

previousSkipping :: Alternative f => Finite (Cardinality (Const a b)) -> Const a b -> f (Const a b) Source #

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

nextSkipping :: Alternative f => Finite (Cardinality (Const a b)) -> Const a b -> f (Const a b) Source #

enumerateFrom :: Const a b -> [Const a b] Source #

enumerateFromThen :: Const a b -> Const a b -> [Const a b] Source #

enumerateFromTo :: Const a b -> Const a b -> [Const a b] Source #

enumerateFromThenTo :: Const a b -> Const a b -> Const a b -> [Const a b] Source #

(Finitary a, Finitary b, Finitary c, Finitary d) => Finitary (a, b, c, d) Source # 
Instance details

Defined in Data.Finitary

Associated Types

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

Methods

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 #

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

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

previousSkipping :: Alternative f => Finite (Cardinality (a, b, c, d)) -> (a, b, c, d) -> f (a, b, c, d) Source #

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

nextSkipping :: Alternative f => Finite (Cardinality (a, b, c, d)) -> (a, b, c, d) -> f (a, b, c, d) Source #

enumerateFrom :: (a, b, c, d) -> [(a, b, c, d)] Source #

enumerateFromThen :: (a, b, c, d) -> (a, b, c, d) -> [(a, b, c, d)] Source #

enumerateFromTo :: (a, b, c, d) -> (a, b, c, d) -> [(a, b, c, d)] Source #

enumerateFromThenTo :: (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d) -> [(a, b, c, d)] Source #

(Finitary a, Finitary b, Finitary c, Finitary d, Finitary e) => Finitary (a, b, c, d, e) Source # 
Instance details

Defined in Data.Finitary

Associated Types

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

Methods

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

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

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

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

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

previousSkipping :: Alternative f => Finite (Cardinality (a, b, c, d, e)) -> (a, b, c, d, e) -> f (a, b, c, d, e) Source #

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

nextSkipping :: Alternative f => Finite (Cardinality (a, b, c, d, e)) -> (a, b, c, d, e) -> f (a, b, c, d, e) Source #

enumerateFrom :: (a, b, c, d, e) -> [(a, b, c, d, e)] Source #

enumerateFromThen :: (a, b, c, d, e) -> (a, b, c, d, e) -> [(a, b, c, d, e)] Source #

enumerateFromTo :: (a, b, c, d, e) -> (a, b, c, d, e) -> [(a, b, c, d, e)] Source #

enumerateFromThenTo :: (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) -> [(a, b, c, d, e)] Source #

(Finitary a, Finitary b, Finitary c, Finitary d, Finitary e, Finitary f) => Finitary (a, b, c, d, e, f) Source # 
Instance details

Defined in Data.Finitary

Associated Types

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

Methods

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 :: Alternative f0 => (a, b, c, d, e, f) -> f0 (a, b, c, d, e, f) Source #

previousSkipping :: Alternative f0 => Finite (Cardinality (a, b, c, d, e, f)) -> (a, b, c, d, e, f) -> f0 (a, b, c, d, e, f) Source #

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

nextSkipping :: Alternative f0 => Finite (Cardinality (a, b, c, d, e, f)) -> (a, b, c, d, e, f) -> f0 (a, b, c, d, e, f) Source #

enumerateFrom :: (a, b, c, d, e, f) -> [(a, b, c, d, e, f)] Source #

enumerateFromThen :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> [(a, b, c, d, e, f)] Source #

enumerateFromTo :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> [(a, b, c, d, e, f)] Source #

enumerateFromThenTo :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> [(a, b, c, d, e, f)] Source #