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 | None |

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 (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 values of ```
Finite
(Cardinality YourType)
```

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 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
- next :: Alternative f => a -> f a
- enumerateFrom :: a -> [a]
- enumerateFromThen :: a -> a -> [a]
- enumerateFromTo :: a -> a -> [a]
- enumerateFromThenTo :: a -> a -> a -> [a]

# Documentation

class KnownNat (Cardinality a) => Finitary (a :: Type) where Source #

Witnesses an isomorphism between `a`

and `(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} \; n \; \texttt{fromFinite} \; x = \texttt{fromFinite} \; y \rightarrow x = y\]
- \[\forall x :: \texttt{Finite} \; n \; \exists y :: a \mid \texttt{fromFinite} \; x = y\]

Additionally, if you define any of the other methods, these laws must hold:

- \[ a \neq \emptyset \rightarrow \texttt{start} = \texttt{fromFinite} \; 0 \]
- \[ a \neq \emptyset \rightarrow \texttt{end} = \texttt{fromFinite} \; (n - 1)) \]
- \[ \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{prev} \; x = (\texttt{fromFinite} \circ - 1 \circ \texttt{toFinite}) \; x \]
- \[ \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{]} \]

The default definitions follow these laws. Additionally, if you derive via
`Generic`

, these are also followed for you.

Lastly, we *strongly* suggest that `fromFinite`

and `toFinite`

should have
time complexity \(\Theta(1)\), or, if that's not possible, \(O(\texttt{n})\), where `n`

is the
cardinality of `a`

. The latter is in effect 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.

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

Converts an index into its corresponding inhabitant.

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

Converts an index into its corresponding inhabitant.

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

Converts an inhabitant to its corresponding index.

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

Converts an inhabitant to its corresponding index.

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.

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.

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 #

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 #