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

* What is the cardinality of this type?
* 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 DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeInType #-}

import GHC.Generics
import GHC.TypeNats
import Data.Word

import qualified Data.Vector.Sized as VS

data Foo = Bar | Baz (Word8, Word8) | Quux (VS.Vector 4 Bool)
  deriving (Eq, Generic, 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 have tested ``finitary`` (meaning 'run tests, not just compiled')
on GHCs 8.2.2, 8.4.4, 8.6.5 and 8.8.1. If you would like any additional versions 
supported, please let us know.

So far, the tests have all been on x86_64 GNU/Linux. 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/koz.ross/finitary-derive