| Copyright | (C) Koz Ross 2019 |
|---|---|
| License | GPL version 3.0 or later |
| Maintainer | koz.ross@retro-freedom.nz |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | Trustworthy |
| Language | Haskell2010 |
Data.Finitary
Description
This package provides the Finitary type class, as well as a range of useful
'base' instances for commonly-used finitary types.
For your own types, there are three possible ways to define an instance of
Finitary:
Via Generic
If your data type implements Generic (and is finitary), you can
automatically derive your instance:
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
import GHC.Generics
import Data.Word
data Foo = Bar | Baz (Word8, Word8) | Quux Word16
deriving (Eq, Generic, Finitary)This is the easiest method, and also the safest, as GHC will automatically
determine the cardinality of Foo, as well as defining law-abiding methods.
It may be somewhat slower than a 'hand-rolled' method in some cases.
By defining only Cardinality, fromFinite and toFinite
If you want a manually-defined instance, but don't wish to define every
method, only fromFinite and toFinite are needed, along with
Cardinality. Cardinality in particular must be defined with care, as
otherwise, you may end up with inconstructable values or indexes that don't
correspond to anything.
By defining everything
For maximum control, you can define all the methods. Ensure you follow all the laws!
Synopsis
- class (Eq a, KnownNat (Cardinality a)) => Finitary (a :: Type) where
- type Cardinality a :: Nat
- fromFinite :: Finite (Cardinality a) -> a
- toFinite :: a -> Finite (Cardinality a)
- start :: 1 <= Cardinality a => a
- end :: 1 <= Cardinality a => a
- previous :: Alternative f => a -> f a
- previousSkipping :: Alternative f => Finite (Cardinality a) -> a -> f a
- next :: Alternative f => a -> f a
- nextSkipping :: Alternative f => Finite (Cardinality a) -> a -> f a
- enumerateFrom :: a -> [a]
- enumerateFromThen :: a -> a -> [a]
- enumerateFromTo :: a -> a -> [a]
- enumerateFromThenTo :: a -> a -> a -> [a]
Documentation
class (Eq a, KnownNat (Cardinality a)) => Finitary (a :: Type) where Source #
Witnesses an isomorphism between a and some (KnownNat n) => Finite n.
Effectively, a lawful instance of this shows that a has exactly n
(non-_|_) inhabitants, and that we have a bijection with fromFinite and
toFinite as each 'direction'.
For any type a with an instance of Finitary, for every non-_|_ x :: a, we have
a unique index i :: Finite n. We will also refer to any such x as an
inhabitant of a. We can convert inhabitants to indexes using toFinite,
and also convert indexes to inhabitants with fromFinite.
Laws
The main laws state that fromFinite should be a bijection, with toFinite as
its inverse, and Cardinality must be a truthful representation of the
cardinality of the type. Thus:
- \[\texttt{fromFinite} \circ \texttt{toFinite} = \texttt{toFinite} \circ \texttt{fromFinite} = \texttt{id}\]
- \[\forall x, y :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \; \texttt{fromFinite} \; x = \texttt{fromFinite} \; y \rightarrow x = y\]
- \[\forall x :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \; \exists y :: a \mid \texttt{fromFinite} \; x = y\]
Furthermore, fromFinite should be _order-preserving_. Namely, if a is an
instance of Ord, we must have:
- \[\forall i, j :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \; \texttt{fromFinite} \; i \leq \texttt{fromFinite} \; j \rightarrow i \leq j \]
Lastly, if you define any of the other methods, these laws must hold:
- \[ a \neq \emptyset \rightarrow \texttt{start} = \texttt{fromFinite} \; \texttt{minBound} \]
- \[ a \neq \emptyset \rightarrow \texttt{end} = \texttt{fromFinite} \; \texttt{maxBound} \]
- \[ \forall x :: a \; \texttt{end} \neq x \rightarrow \texttt{next} \; x = (\texttt{fromFinite} \circ + 1 \circ \texttt{toFinite}) \; x \]
- \[ \forall i :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \; \texttt{nextSkipping} \; i = \underbrace{\texttt{next} \circ \ldots \circ \texttt{next}}_{i} \]
- \[ \forall x :: a \; \texttt{start} \neq x \rightarrow \texttt{previous} \; x = (\texttt{fromFinite} \circ - 1 \circ \texttt{toFinite}) \; x \]
- \[ \forall i :: \texttt{Finite} \; (\texttt{Cardinality} \; a) \; \texttt{previousSkipping} \; i = \underbrace{\texttt{previous} \circ \ldots \circ \texttt{previous}}_{i} \]
- \[ \forall x :: a \; \texttt{enumerateFrom} \; x = \texttt{fromFinite <\$> [toFinite} \; x \texttt{..]} \]
- \[ \forall x, y :: a \; \texttt{enumerateFromThen} \; x y = \texttt{fromFinite <\$> [toFinite} \; x \texttt{, }\; y \texttt{..]} \]
- \[ \forall x, y :: a \; \texttt{enumerateFromTo} \; x \; y = \texttt{fromFinite <\$> [toFinite} \; x \texttt{..} \; y \texttt{]} \]
- \[ \forall x, y, z :: a \; \texttt{enumerateFromThenTo} \; x \; y \; z = \texttt{fromFinite <\$> [toFinite} \; x \texttt{,} \; y \texttt{..} \; z \texttt{]} \]
Together with the fact that Finite n is well-ordered whenever KnownNat n
holds, a law-abiding Finitary instance for a type a defines a constructive
well-order, witnessed by
toFinite and fromFinite, which agrees with the Ord instance for a, if
any.
We strongly suggest that fromFinite and toFinite should have
time complexity \(\Theta(1)\), or, if that's not possible, \(O(\texttt{Cardinality} \; a)\).
The latter is the case for instances generated using
Generics-based derivation, but not for 'basic' types; thus, these
functions for your derived types will only be as slow as their 'structure',
rather than their 'contents', provided the contents are of these 'basic'
types.
Minimal complete definition
Nothing
Associated Types
type Cardinality a :: Nat Source #
How many (non-_|_) inhabitants a has, as a typelevel natural number.
type Cardinality a = GCardinality (Rep a) Source #
Methods
fromFinite :: Finite (Cardinality a) -> a Source #
Converts an index into its corresponding inhabitant.
default fromFinite :: (Generic a, GFinitary (Rep a), Cardinality a ~ GCardinality (Rep a)) => Finite (Cardinality a) -> a Source #
toFinite :: a -> Finite (Cardinality a) Source #
Converts an inhabitant to its corresponding index.
default toFinite :: (Generic a, GFinitary (Rep a), Cardinality a ~ GCardinality (Rep a)) => a -> Finite (Cardinality a) Source #
start :: 1 <= Cardinality a => a Source #
The first inhabitant, by index, assuming a has any inhabitants.
end :: 1 <= Cardinality a => a Source #
The last inhabitant, by index, assuming a has any inhabitants.
previous :: Alternative f => a -> f a Source #
previous x gives the inhabitant whose index precedes the index of x,
or empty if no such index exists.
previousSkipping :: Alternative f => Finite (Cardinality a) -> a -> f a Source #
previousSkipping i x 'skips back' i index values from the index of
x, then gives the inhabitant whose index precedes the result, or empty
if no such index exists.
next :: Alternative f => a -> f a Source #
next x gives the inhabitant whose index follows the index of x, or
empty if no such index exists.
nextSkipping :: Alternative f => Finite (Cardinality a) -> a -> f a Source #
nextSkipping i x 'skips forward' i index values from the index of
x, then gives the inhabitant whose index follows the result, or empty
if no such index exists.
enumerateFrom :: a -> [a] Source #
enumerateFrom x gives a list of inhabitants, starting with x,
followed by all other values whose indexes follow x, in index order.
enumerateFromThen :: a -> a -> [a] Source #
Like enumerateFrom, except in steps of toFinite y - toFinite x.
enumerateFromTo :: a -> a -> [a] Source #
enumerateFromTo x y gives a list of inhabitants, starting with x,
ending with y, and containing all other values whose indices lie between
those of x and y. The list is in index order.
enumerateFromThenTo :: a -> a -> a -> [a] Source #
Like enumerateFromTo, except in steps of toFinite y - toFinite x.