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:
- 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
- Get the 'next' or 'previous' value, or report that it doesn't exist
- Enumerate ranges of these values
All of this is safe, total and can be relied upon. Check out the documentation
for more details - all of this functionality is provided.
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 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 (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
Unbox instances
- 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 GHC 8.4.4 and GHC 8.6.5. GHC 8.8.1 is still in the pipeline, as some of our
dependencies don't support it yet, but as soon as they do, we plan to test with
it also. 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.
