A better, more type-safe Enum.
sheaf 9c097154d8 v 2.1.3.0 | 2 months ago | |
---|---|---|
src | 2 months ago | |
test | 4 years ago | |
.gitignore | 4 years ago | |
.nvimrc | 4 years ago | |
CHANGELOG.md | 2 months ago | |
LICENSE.md | 4 years ago | |
README.md | 3 years ago | |
Setup.hs | 4 years ago | |
cabal.project | 3 months ago | |
finitary.cabal | 2 months ago |
finitary
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.
Consider Enum
. It's not difficult to see that Enum
has issues:
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:
Int
I can feed to toEnum
?x
, is toEnum . (+ 1) . fromEnum $ x
safe (in that it'll give
us a value instead of blowing up)?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.
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:
a
has finitely-many non-_|_
inhabitantsn
, which is the cardinality of a
(how many inhabitants we have exactly)fromFinite :: Finite n ->
a
and toFinite :: a -> Finite n
Finitary
solve the issues behind Enum
?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.
Finitary
instanceAside from cardinality, we also inherently get the ability to:
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.
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.
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:
Monoid
under
intersectionlens
tricksIf 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.
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!
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.