Copyright | (C) Koz Ross 2019 |
---|---|

License | GPL version 3.0 or later |

Maintainer | koz.ross@retro-freedom.nz |

Stability | Experimental |

Portability | GHC only |

Safe Haskell | Trustworthy |

Language | Haskell2010 |

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

- 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 :: Alternative f => a -> f a
- previousSkipping :: Alternative f => Finite (Cardinality a) -> a -> f a
- next :: Alternative f => a -> f a
- nextSkipping :: Alternative f => Finite (Cardinality a) -> a -> f a
- enumerateFrom :: a -> [a]
- enumerateFromThen :: a -> a -> [a]
- enumerateFromTo :: a -> a -> [a]
- enumerateFromThenTo :: 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 _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.

Nothing

type Cardinality a :: Nat Source #

How many (non-`_|_`

) inhabitants `a`

has, as a typelevel natural number.

type Cardinality a = GCardinality (Rep a) Source #

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`

.