Data.Finite

Provides a class of types isomorphic to some statically-known Fin n.

This comes with Generics-based generated instances, and can be used to generate instances of Enum and Bounded (for which the stock deriving only supports sum types with no fields).

Since this is all still represented by Int internally, things will start raising errors if your type has more values than can fit in positive Ints. It's not recommended to use this on large types, and there's not much reason to want to anyway, as its main uses are to derive Enum (which is also based on Int) and to make the type compatible with Table (which would be impractically large for a key type with too many values to represent as Int).

The most common way to get a Finite instance for a type is to tack on a deriving Finite via Wrapped Generic MyType clause, which results in an automatically-generated instance based on the type's ADT structure.

This also provides instances Enum (Wrapped Finite a) and Bounded (Wrapped Finite a), so some types that would otherwise not be compatible with derived Enum instances can get them by adding a deriving (Enum, Bounded) via Wrapped Finite MyType clause.

Finite Enumerations

class Finite a where

A typeclass of finite enumerable types.

These allow constructing Representable Functors using a simple Vec as the underlying storage, with constant-time lookup and efficient traversals.

Note that since Fin is (currently) represented by Int, any type with more values than Int can't have an instance. This means we can't have instances for 32- and 64-bit arithmetic types, since Int is only required to have 30 bits of precision.

Annoyingly, we also can't have an instance for Int and Word, because Fin wastes one bit of the Int by forbidding negative values. The cardinality of Int and Word would need to be twice as large as we can actually represent in a Fin. Another obstacle is that their cardinality varies between implementations and architectures; it's possible to work around this by making their Cardinality an irreducible type family application, and using 'Data.SInt.SI#' to plug in a value at runtime, but this makes the Fins related to Int and Word annoying to work with, since their bound is only known at runtime.

Fortunately, those instances are unlikely to be important, since a table of 2^32 elements is moderately impractical (32GiB of pointers alone), and a table of 2^64 elements is unrepresentable in current computer architectures.

toFin and fromFin shall be total functions and shall be the two sides of an isomorphism.

Associated Types

type Cardinality a :: Nat

Methods

cardinality' :: SC a (Cardinality a)

A witness that the cardinality is known at runtime.

This isn't part of the class context because we can only perform arithmetic on KnownNat instances in expression context; that is, we can't convince GHC that an instance with type Cardinality (Maybe a) = Cardinality a + 1 is valid if the KnownNat is in the class context. Instead, we use SInt to allow computing the cardinality at runtime.

toFin :: a -> Fin (Cardinality a)

fromFin :: Fin (Cardinality a) -> a

Instances

Finite Bool

Defined in Data.Finite

Associated Types

type Cardinality Bool :: Nat

Methods

cardinality' :: SC Bool (Cardinality Bool)

toFin :: Bool -> Fin (Cardinality Bool)

fromFin :: Fin (Cardinality Bool) -> Bool

Finite Char

Defined in Data.Finite

Associated Types

type Cardinality Char :: Nat

Methods

cardinality' :: SC Char (Cardinality Char)

toFin :: Char -> Fin (Cardinality Char)

fromFin :: Fin (Cardinality Char) -> Char

Finite Int8

Defined in Data.Finite

Associated Types

type Cardinality Int8 :: Nat

Methods

cardinality' :: SC Int8 (Cardinality Int8)

toFin :: Int8 -> Fin (Cardinality Int8)

fromFin :: Fin (Cardinality Int8) -> Int8

Finite Int16

Defined in Data.Finite

Associated Types

type Cardinality Int16 :: Nat

Methods

cardinality' :: SC Int16 (Cardinality Int16)

toFin :: Int16 -> Fin (Cardinality Int16)

fromFin :: Fin (Cardinality Int16) -> Int16

Finite Ordering

Defined in Data.Finite

Associated Types

type Cardinality Ordering :: Nat

Methods

cardinality' :: SC Ordering (Cardinality Ordering)

toFin :: Ordering -> Fin (Cardinality Ordering)

fromFin :: Fin (Cardinality Ordering) -> Ordering

Finite Word8

Defined in Data.Finite

Associated Types

type Cardinality Word8 :: Nat

Methods

cardinality' :: SC Word8 (Cardinality Word8)

toFin :: Word8 -> Fin (Cardinality Word8)

fromFin :: Fin (Cardinality Word8) -> Word8

Finite Word16

Defined in Data.Finite

Associated Types

type Cardinality Word16 :: Nat

Methods

cardinality' :: SC Word16 (Cardinality Word16)

toFin :: Word16 -> Fin (Cardinality Word16)

fromFin :: Fin (Cardinality Word16) -> Word16

Finite ()

Defined in Data.Finite

Associated Types

type Cardinality () :: Nat

Methods

cardinality' :: SC () (Cardinality ())

toFin :: () -> Fin (Cardinality ())

fromFin :: Fin (Cardinality ()) -> ()

Finite Void

Defined in Data.Finite

Associated Types

type Cardinality Void :: Nat

Methods

cardinality' :: SC Void (Cardinality Void)

toFin :: Void -> Fin (Cardinality Void)

fromFin :: Fin (Cardinality Void) -> Void

Finite a => Finite (Maybe a)

Defined in Data.Finite

Associated Types

type Cardinality (Maybe a) :: Nat

Methods

cardinality' :: SC (Maybe a) (Cardinality (Maybe a))

toFin :: Maybe a -> Fin (Cardinality (Maybe a))

fromFin :: Fin (Cardinality (Maybe a)) -> Maybe a

Finite a => Finite (Min a)

Defined in Data.Finite

Associated Types

type Cardinality (Min a) :: Nat

Methods

cardinality' :: SC (Min a) (Cardinality (Min a))

toFin :: Min a -> Fin (Cardinality (Min a))

fromFin :: Fin (Cardinality (Min a)) -> Min a

Finite a => Finite (Max a)

Defined in Data.Finite

Associated Types

type Cardinality (Max a) :: Nat

Methods

cardinality' :: SC (Max a) (Cardinality (Max a))

toFin :: Max a -> Fin (Cardinality (Max a))

fromFin :: Fin (Cardinality (Max a)) -> Max a

Finite a => Finite (First a)

Defined in Data.Finite

Associated Types

type Cardinality (First a) :: Nat

Methods

cardinality' :: SC (First a) (Cardinality (First a))

toFin :: First a -> Fin (Cardinality (First a))

fromFin :: Fin (Cardinality (First a)) -> First a

Finite a => Finite (Last a)

Defined in Data.Finite

Associated Types

type Cardinality (Last a) :: Nat

Methods

cardinality' :: SC (Last a) (Cardinality (Last a))

toFin :: Last a -> Fin (Cardinality (Last a))

fromFin :: Fin (Cardinality (Last a)) -> Last a

Finite a => Finite (WrappedMonoid a)

Defined in Data.Finite

Associated Types

type Cardinality (WrappedMonoid a) :: Nat

Methods

cardinality' :: SC (WrappedMonoid a) (Cardinality (WrappedMonoid a))

toFin :: WrappedMonoid a -> Fin (Cardinality (WrappedMonoid a))

fromFin :: Fin (Cardinality (WrappedMonoid a)) -> WrappedMonoid a

Finite a => Finite (Identity a)

Defined in Data.Finite

Associated Types

type Cardinality (Identity a) :: Nat

Methods

cardinality' :: SC (Identity a) (Cardinality (Identity a))

toFin :: Identity a -> Fin (Cardinality (Identity a))

fromFin :: Fin (Cardinality (Identity a)) -> Identity a

KnownNat n => Finite (Fin n)

Defined in Data.Finite

Associated Types

type Cardinality (Fin n) :: Nat

Methods

cardinality' :: SC (Fin n) (Cardinality (Fin n))

toFin :: Fin n -> Fin (Cardinality (Fin n))

fromFin :: Fin (Cardinality (Fin n)) -> Fin n

(Finite a, 1 <= Cardinality a) => Bounded (Wrapped Finite a)

Defined in Data.Finite

Methods

minBound :: Wrapped Finite a

maxBound :: Wrapped Finite a

Finite a => Enum (Wrapped Finite a)

Defined in Data.Finite

Methods

succ :: Wrapped Finite a -> Wrapped Finite a

pred :: Wrapped Finite a -> Wrapped Finite a

toEnum :: Int -> Wrapped Finite a

fromEnum :: Wrapped Finite a -> Int

enumFrom :: Wrapped Finite a -> [Wrapped Finite a]

enumFromThen :: Wrapped Finite a -> Wrapped Finite a -> [Wrapped Finite a]

enumFromTo :: Wrapped Finite a -> Wrapped Finite a -> [Wrapped Finite a]

enumFromThenTo :: Wrapped Finite a -> Wrapped Finite a -> Wrapped Finite a -> [Wrapped Finite a]

(Finite a, Finite b) => Finite (Either a b)

Defined in Data.Finite

Associated Types

type Cardinality (Either a b) :: Nat

Methods

cardinality' :: SC (Either a b) (Cardinality (Either a b))

toFin :: Either a b -> Fin (Cardinality (Either a b))

fromFin :: Fin (Cardinality (Either a b)) -> Either a b

(Finite a, Finite b) => Finite (a, b)

Defined in Data.Finite

Associated Types

type Cardinality (a, b) :: Nat

Methods

cardinality' :: SC (a, b) (Cardinality (a, b))

toFin :: (a, b) -> Fin (Cardinality (a, b))

fromFin :: Fin (Cardinality (a, b)) -> (a, b)

(Generic a, GFinite (Rep a)) => Finite (Wrapped Generic a)

Defined in Data.Finite

Associated Types

type Cardinality (Wrapped Generic a) :: Nat

Methods

cardinality' :: SC (Wrapped Generic a) (Cardinality (Wrapped Generic a))

toFin :: Wrapped Generic a -> Fin (Cardinality (Wrapped Generic a))

fromFin :: Fin (Cardinality (Wrapped Generic a)) -> Wrapped Generic a

(Finite a, Finite b, Finite c) => Finite (a, b, c)

Defined in Data.Finite

Associated Types

type Cardinality (a, b, c) :: Nat

Methods

cardinality' :: SC (a, b, c) (Cardinality (a, b, c))

toFin :: (a, b, c) -> Fin (Cardinality (a, b, c))

fromFin :: Fin (Cardinality (a, b, c)) -> (a, b, c)

(Finite a, Finite b, Finite c, Finite d) => Finite (a, b, c, d)

Defined in Data.Finite

Associated Types

type Cardinality (a, b, c, d) :: Nat

Methods

cardinality' :: SC (a, b, c, d) (Cardinality (a, b, c, d))

toFin :: (a, b, c, d) -> Fin (Cardinality (a, b, c, d))

fromFin :: Fin (Cardinality (a, b, c, d)) -> (a, b, c, d)

(Finite a, Finite b, Finite c, Finite d, Finite e) => Finite (a, b, c, d, e)

Defined in Data.Finite

Associated Types

type Cardinality (a, b, c, d, e) :: Nat

Methods

cardinality' :: SC (a, b, c, d, e) (Cardinality (a, b, c, d, e))

toFin :: (a, b, c, d, e) -> Fin (Cardinality (a, b, c, d, e))

fromFin :: Fin (Cardinality (a, b, c, d, e)) -> (a, b, c, d, e)

cardinality :: forall a. Finite a => SInt (Cardinality a)

A witness that the cardinality of a is known at runtime.

enumerate :: forall a. Finite a => [a]

Generate a list containing every value of a.

asFin :: Finite a => Iso' a (Fin (Cardinality a))

An Iso between a and the corresponding Fin type.

Implementation Details

data SC a n

A wrapper type around Cardinality a to support DerivingVia on GHC 8.6.

Instance methods that don't mention the instance head outside of type families / aliases don't work with DerivingVia on GHC 8.6 because it uses type signatures rather than TypeApplications to choose the instance to call into.

class GFinite a where

The derived Finite implementation of a generic representation type.

Methods

gcardinality :: SInt (GCardinality a)

gtoFin :: a p -> Fin (GCardinality a)

gfromFin :: Fin (GCardinality a) -> a p

Instances

GFinite (U1 :: k -> Type)

Defined in Data.Finite

Methods

gcardinality :: SInt (GCardinality U1)

gtoFin :: forall (p :: k0). U1 p -> Fin (GCardinality U1)

gfromFin :: forall (p :: k0). Fin (GCardinality U1) -> U1 p

GFinite (V1 :: k -> Type)

Defined in Data.Finite

Methods

gcardinality :: SInt (GCardinality V1)

gtoFin :: forall (p :: k0). V1 p -> Fin (GCardinality V1)

gfromFin :: forall (p :: k0). Fin (GCardinality V1) -> V1 p

(GFinite f, GFinite g) => GFinite (f :*: g :: k -> Type)

Defined in Data.Finite

Methods

gcardinality :: SInt (GCardinality (f :*: g))

gtoFin :: forall (p :: k0). (f :*: g) p -> Fin (GCardinality (f :*: g))

gfromFin :: forall (p :: k0). Fin (GCardinality (f :*: g)) -> (f :*: g) p

(GFinite f, GFinite g) => GFinite (f :+: g :: k -> Type)

Defined in Data.Finite

Methods

gcardinality :: SInt (GCardinality (f :+: g))

gtoFin :: forall (p :: k0). (f :+: g) p -> Fin (GCardinality (f :+: g))

gfromFin :: forall (p :: k0). Fin (GCardinality (f :+: g)) -> (f :+: g) p

Finite a => GFinite (K1 i a :: k -> Type)

Defined in Data.Finite

Methods

gcardinality :: SInt (GCardinality (K1 i a))

gtoFin :: forall (p :: k0). K1 i a p -> Fin (GCardinality (K1 i a))

gfromFin :: forall (p :: k0). Fin (GCardinality (K1 i a)) -> K1 i a p

GFinite f => GFinite (M1 i c f :: k -> Type)

Defined in Data.Finite

Methods

gcardinality :: SInt (GCardinality (M1 i c f))

gtoFin :: forall (p :: k0). M1 i c f p -> Fin (GCardinality (M1 i c f))

gfromFin :: forall (p :: k0). Fin (GCardinality (M1 i c f)) -> M1 i c f p

type family GCardinality a where ...

The derived cardinality of a generic representation type.

Equations

GCardinality V1 = 0

GCardinality U1 = 1

GCardinality (K1 i a) = Cardinality a

GCardinality (M1 i c f) = GCardinality f

GCardinality (f :+: g) = GCardinality f + GCardinality g

GCardinality (f :*: g) = GCardinality f * GCardinality g