`finitary`

## What's all this about?

`finitary`

allows us to specify that a type is *finite* (that is, contains
finitely many inhabitants which are not `_|_`

), and have confirmation of this
fact by GHC. Additionally, it offers a `Generics`

-based auto-derivation
interface for this, as well as multiple helper functions that are enabled by all
this machinery.

### Why is this a big deal?

Consider `Enum`

. It's not difficult to see that `Enum`

has issues:

#### It's partial all over the place

What will this code do?

```
toEnum 3 :: Bool
```

The answer is 'a runtime error'. How about this?

```
succ True
```

The answer, again, is 'a runtime error'. Many of the methods provided by `Enum`

are partial like this, because many types that happen to be `Enum`

instances
have cardinalities (much) smaller than `Int`

, which necessitates leaving some
`Int`

values 'out'.

The converse is not much better: on some platforms, `Int`

has *smaller*
cardinality than some types with `Enum`

instances in `base`

. For example, on
a platform where `Int`

is 32 bits wide, the `Word64`

instance will definitely
cause problems, as it's 'too big'.

An `Enum`

instance says that a type can be munged to and from an `Int`

...
somehow. While `base`

and the Haskell Report certainly provide some limits
on its behaviour, a lot of questions remain unanswered, including:

- How many inhabitants does this type have?
- What are the 'safe' values of
`Int`

I can feed to `toEnum`

?
- For any
`x`

, is `toEnum . (+ 1) . fromEnum $ x`

safe (in that it'll give
us a value instead of blowing up)?

#### We don't have a (default) way to auto-derive it

Quoting `base`

:

Instances of `Enum`

may be derived for any enumeration type (types whose
constructors have no fields).

But what if your type has fields, especially when they're instances of `Enum`

?
Unfortunately, no auto-derivation for you. While this stance makes some sense,
it's still rather inconvenient.

## OK, so what are you offering instead?

The core of `finitary`

is the `Finitary`

type class. If we have an instance
of `Finitary`

for some type `a`

, we have a witness to an isomorphism between
`a`

and some `(KnownNat n) => Finite n`

. More precisely, we (together with GHC)
know:

* That `a`

has finitely-many non-`_|_`

inhabitants

- The value of
`n`

, which is the *cardinality* of `a`

(how many inhabitants we have exactly)
- Two functions to 'witness' the isomorphism, namely
```
fromFinite :: Finite n ->
a
```

and `toFinite :: a -> Finite n`

### How does `Finitary`

solve the issues behind `Enum`

?

#### Everything is total, forever

There is no way to call `fromFinite`

or `toFinite`

with an 'inappropriate'
argument. We always know - if you give me a `Finite n`

, I will give you back a
(unique) `a`

, guaranteed.

#### We learn a lot from a type having a `Finitary`

instance

Aside from cardinality, we also inherently get the ability to:

- Have a 'starting' and 'ending' value (assuming the cardinality of the type
isn't zero); and
- Get the 'next' or 'previous' value, or report that it doesn't exist.

All of this is safe, total and can be relied upon. Check out the documentation
for more details - all of this functionality is provided. We also have functions
to help enumerate values of `Finitary`

types.

#### But what about auto-derivation?

We have you covered. If you want to auto-derive an instance of
`Finitary`

for your type, you absolutely can, using the power of
`GHC.Generics`

:

```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
import Data.Finitary (Finitary)
import Data.Vector.Sized (Vector)
import Data.Word (Word8)
import GHC.Generics (Generic)
data Foo = Bar | Baz (Word8, Word8) | Quux (Vector 4 Bool)
deriving stock (Eq, Generic)
deriving anyclass (Finitary)
```

Furthermore, GHC will even calculate the cardinality for you. To assist in this,
we have provided as many instances of `Finitary`

for 'base' types as possible -
see the documentation for full details.

### That all seems rather cool - what else can I do with this?

Knowing that a type has finite cardinality is usable for many things - all of
which we plan to provide. Some examples (with links once we have working, tested
code) include:

- Automatic derivation of instances
- Type-safe refinement
- Random generation and stream sampling
- Efficient sets, allowing operations like complements and a
`Monoid`

under
intersection
- Efficient maps
- Various clever
`lens`

tricks

If there's something else interesting you think can be done with this, let us
know: it might make it onto this list, and into code.

## What will this work on?

Currently, we support GHC versions ranging from 8.6 to 9.0.

The library has been tested on x86_64, GNU/Linux and Windows.
If you have results on other platforms or architectures, please let us know too!

## License

This library is under the GNU General Public License, version 3 or later (SPDX
code `GPL-3.0-or-later`

). For more details, see the `LICENSE.md`

file.