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