# ``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?

```haskell
toEnum 3 :: Bool
```

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

```haskell
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'.

#### It gives us almost no information

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``:

```haskell
{-# 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][1]
* 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.

[1]: https://notabug.org/sheaf/finitary-derive