{-# LANGUAGE TypeInType #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
module Data.Finitary.Finiteness
(
Finiteness(..)
) where
import GHC.TypeNats
import Data.Typeable (Typeable)
import Data.Data (Data)
import Data.Finitary (Finitary(..))
import Data.Ord (comparing)
import Control.DeepSeq (NFData(..))
import Data.Hashable (Hashable(..))
import Data.Binary (Binary(..))
newtype Finiteness a = Finiteness { forall a. Finiteness a -> a
unFiniteness :: a }
deriving (Finiteness a -> Finiteness a -> Bool
(Finiteness a -> Finiteness a -> Bool)
-> (Finiteness a -> Finiteness a -> Bool) -> Eq (Finiteness a)
forall a. Eq a => Finiteness a -> Finiteness a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Finiteness a -> Finiteness a -> Bool
$c/= :: forall a. Eq a => Finiteness a -> Finiteness a -> Bool
== :: Finiteness a -> Finiteness a -> Bool
$c== :: forall a. Eq a => Finiteness a -> Finiteness a -> Bool
Eq, Int -> Finiteness a -> ShowS
[Finiteness a] -> ShowS
Finiteness a -> String
(Int -> Finiteness a -> ShowS)
-> (Finiteness a -> String)
-> ([Finiteness a] -> ShowS)
-> Show (Finiteness a)
forall a. Show a => Int -> Finiteness a -> ShowS
forall a. Show a => [Finiteness a] -> ShowS
forall a. Show a => Finiteness a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Finiteness a] -> ShowS
$cshowList :: forall a. Show a => [Finiteness a] -> ShowS
show :: Finiteness a -> String
$cshow :: forall a. Show a => Finiteness a -> String
showsPrec :: Int -> Finiteness a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Finiteness a -> ShowS
Show, ReadPrec [Finiteness a]
ReadPrec (Finiteness a)
Int -> ReadS (Finiteness a)
ReadS [Finiteness a]
(Int -> ReadS (Finiteness a))
-> ReadS [Finiteness a]
-> ReadPrec (Finiteness a)
-> ReadPrec [Finiteness a]
-> Read (Finiteness a)
forall a. Read a => ReadPrec [Finiteness a]
forall a. Read a => ReadPrec (Finiteness a)
forall a. Read a => Int -> ReadS (Finiteness a)
forall a. Read a => ReadS [Finiteness a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Finiteness a]
$creadListPrec :: forall a. Read a => ReadPrec [Finiteness a]
readPrec :: ReadPrec (Finiteness a)
$creadPrec :: forall a. Read a => ReadPrec (Finiteness a)
readList :: ReadS [Finiteness a]
$creadList :: forall a. Read a => ReadS [Finiteness a]
readsPrec :: Int -> ReadS (Finiteness a)
$creadsPrec :: forall a. Read a => Int -> ReadS (Finiteness a)
Read, Typeable, Typeable (Finiteness a)
Typeable (Finiteness a)
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Finiteness a -> c (Finiteness a))
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Finiteness a))
-> (Finiteness a -> Constr)
-> (Finiteness a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Finiteness a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Finiteness a)))
-> ((forall b. Data b => b -> b) -> Finiteness a -> Finiteness a)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Finiteness a -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Finiteness a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Finiteness a -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> Finiteness a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Finiteness a -> m (Finiteness a))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Finiteness a -> m (Finiteness a))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Finiteness a -> m (Finiteness a))
-> Data (Finiteness a)
Finiteness a -> Constr
Finiteness a -> DataType
(forall b. Data b => b -> b) -> Finiteness a -> Finiteness a
forall {a}. Data a => Typeable (Finiteness a)
forall a. Data a => Finiteness a -> Constr
forall a. Data a => Finiteness a -> DataType
forall a.
Data a =>
(forall b. Data b => b -> b) -> Finiteness a -> Finiteness a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Finiteness a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> Finiteness a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Finiteness a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Finiteness a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Finiteness a -> m (Finiteness a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Finiteness a -> m (Finiteness a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Finiteness a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Finiteness a -> c (Finiteness a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Finiteness a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Finiteness a))
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Finiteness a -> u
forall u. (forall d. Data d => d -> u) -> Finiteness a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Finiteness a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Finiteness a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Finiteness a -> m (Finiteness a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Finiteness a -> m (Finiteness a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Finiteness a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Finiteness a -> c (Finiteness a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Finiteness a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Finiteness a))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Finiteness a -> m (Finiteness a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Finiteness a -> m (Finiteness a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Finiteness a -> m (Finiteness a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Finiteness a -> m (Finiteness a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Finiteness a -> m (Finiteness a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Finiteness a -> m (Finiteness a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Finiteness a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Finiteness a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Finiteness a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> Finiteness a -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Finiteness a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Finiteness a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Finiteness a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Finiteness a -> r
gmapT :: (forall b. Data b => b -> b) -> Finiteness a -> Finiteness a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Finiteness a -> Finiteness a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Finiteness a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Finiteness a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Finiteness a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Finiteness a))
dataTypeOf :: Finiteness a -> DataType
$cdataTypeOf :: forall a. Data a => Finiteness a -> DataType
toConstr :: Finiteness a -> Constr
$ctoConstr :: forall a. Data a => Finiteness a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Finiteness a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Finiteness a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Finiteness a -> c (Finiteness a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Finiteness a -> c (Finiteness a)
Data, (forall a b. (a -> b) -> Finiteness a -> Finiteness b)
-> (forall a b. a -> Finiteness b -> Finiteness a)
-> Functor Finiteness
forall a b. a -> Finiteness b -> Finiteness a
forall a b. (a -> b) -> Finiteness a -> Finiteness b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Finiteness b -> Finiteness a
$c<$ :: forall a b. a -> Finiteness b -> Finiteness a
fmap :: forall a b. (a -> b) -> Finiteness a -> Finiteness b
$cfmap :: forall a b. (a -> b) -> Finiteness a -> Finiteness b
Functor, NonEmpty (Finiteness a) -> Finiteness a
Finiteness a -> Finiteness a -> Finiteness a
(Finiteness a -> Finiteness a -> Finiteness a)
-> (NonEmpty (Finiteness a) -> Finiteness a)
-> (forall b. Integral b => b -> Finiteness a -> Finiteness a)
-> Semigroup (Finiteness a)
forall b. Integral b => b -> Finiteness a -> Finiteness a
forall a. Semigroup a => NonEmpty (Finiteness a) -> Finiteness a
forall a.
Semigroup a =>
Finiteness a -> Finiteness a -> Finiteness a
forall a b.
(Semigroup a, Integral b) =>
b -> Finiteness a -> Finiteness a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: forall b. Integral b => b -> Finiteness a -> Finiteness a
$cstimes :: forall a b.
(Semigroup a, Integral b) =>
b -> Finiteness a -> Finiteness a
sconcat :: NonEmpty (Finiteness a) -> Finiteness a
$csconcat :: forall a. Semigroup a => NonEmpty (Finiteness a) -> Finiteness a
<> :: Finiteness a -> Finiteness a -> Finiteness a
$c<> :: forall a.
Semigroup a =>
Finiteness a -> Finiteness a -> Finiteness a
Semigroup, Semigroup (Finiteness a)
Finiteness a
Semigroup (Finiteness a)
-> Finiteness a
-> (Finiteness a -> Finiteness a -> Finiteness a)
-> ([Finiteness a] -> Finiteness a)
-> Monoid (Finiteness a)
[Finiteness a] -> Finiteness a
Finiteness a -> Finiteness a -> Finiteness a
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall {a}. Monoid a => Semigroup (Finiteness a)
forall a. Monoid a => Finiteness a
forall a. Monoid a => [Finiteness a] -> Finiteness a
forall a. Monoid a => Finiteness a -> Finiteness a -> Finiteness a
mconcat :: [Finiteness a] -> Finiteness a
$cmconcat :: forall a. Monoid a => [Finiteness a] -> Finiteness a
mappend :: Finiteness a -> Finiteness a -> Finiteness a
$cmappend :: forall a. Monoid a => Finiteness a -> Finiteness a -> Finiteness a
mempty :: Finiteness a
$cmempty :: forall a. Monoid a => Finiteness a
Monoid)
instance (Finitary a) => Finitary (Finiteness a) where
type Cardinality (Finiteness a) = Cardinality a
{-# INLINE fromFinite #-}
fromFinite :: Finite (Cardinality (Finiteness a)) -> Finiteness a
fromFinite = a -> Finiteness a
forall a. a -> Finiteness a
Finiteness (a -> Finiteness a)
-> (Finite (Cardinality a) -> a)
-> Finite (Cardinality a)
-> Finiteness a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (Cardinality a) -> a
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite
{-# INLINE toFinite #-}
toFinite :: Finiteness a -> Finite (Cardinality (Finiteness a))
toFinite = a -> Finite (Cardinality a)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite (a -> Finite (Cardinality a))
-> (Finiteness a -> a) -> Finiteness a -> Finite (Cardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finiteness a -> a
forall a. Finiteness a -> a
unFiniteness
{-# INLINE start #-}
start :: (1 <= Cardinality (Finiteness a)) => Finiteness a
start = a -> Finiteness a
forall a. a -> Finiteness a
Finiteness a
forall a. (Finitary a, 1 <= Cardinality a) => a
start
{-# INLINE end #-}
end :: (1 <= Cardinality (Finiteness a)) => Finiteness a
end = a -> Finiteness a
forall a. a -> Finiteness a
Finiteness a
forall a. (Finitary a, 1 <= Cardinality a) => a
end
{-# INLINE previous #-}
previous :: Finiteness a -> Maybe (Finiteness a)
previous = (a -> Finiteness a) -> Maybe a -> Maybe (Finiteness a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Finiteness a
forall a. a -> Finiteness a
Finiteness (Maybe a -> Maybe (Finiteness a))
-> (Finiteness a -> Maybe a)
-> Finiteness a
-> Maybe (Finiteness a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finitary a => a -> Maybe a
previous (a -> Maybe a) -> (Finiteness a -> a) -> Finiteness a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finiteness a -> a
forall a. Finiteness a -> a
unFiniteness
{-# INLINE next #-}
next :: Finiteness a -> Maybe (Finiteness a)
next = (a -> Finiteness a) -> Maybe a -> Maybe (Finiteness a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Finiteness a
forall a. a -> Finiteness a
Finiteness (Maybe a -> Maybe (Finiteness a))
-> (Finiteness a -> Maybe a)
-> Finiteness a
-> Maybe (Finiteness a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. Finitary a => a -> Maybe a
next (a -> Maybe a) -> (Finiteness a -> a) -> Finiteness a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finiteness a -> a
forall a. Finiteness a -> a
unFiniteness
instance (Finitary a) => Ord (Finiteness a) where
{-# INLINE compare #-}
compare :: Finiteness a -> Finiteness a -> Ordering
compare (Finiteness a
x) (Finiteness a
y) = (a -> Finite (Cardinality a)) -> a -> a -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing a -> Finite (Cardinality a)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite a
x a
y
instance (Finitary a, 1 <= Cardinality a) => Bounded (Finiteness a) where
{-# INLINE minBound #-}
minBound :: Finiteness a
minBound = a -> Finiteness a
forall a. a -> Finiteness a
Finiteness a
forall a. (Finitary a, 1 <= Cardinality a) => a
start
{-# INLINE maxBound #-}
maxBound :: Finiteness a
maxBound = a -> Finiteness a
forall a. a -> Finiteness a
Finiteness a
forall a. (Finitary a, 1 <= Cardinality a) => a
end
instance (Finitary a) => NFData (Finiteness a) where
{-# INLINE rnf #-}
rnf :: Finiteness a -> ()
rnf = Finite (Cardinality a) -> ()
forall a. NFData a => a -> ()
rnf (Finite (Cardinality a) -> ())
-> (Finiteness a -> Finite (Cardinality a)) -> Finiteness a -> ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Finite (Cardinality a)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite (a -> Finite (Cardinality a))
-> (Finiteness a -> a) -> Finiteness a -> Finite (Cardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finiteness a -> a
forall a. Finiteness a -> a
unFiniteness
instance (Finitary a) => Hashable (Finiteness a) where
{-# INLINE hashWithSalt #-}
hashWithSalt :: Int -> Finiteness a -> Int
hashWithSalt Int
salt = Int -> Integer -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt (Integer -> Int)
-> (Finiteness a -> Integer) -> Finiteness a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Integer (Finite (Cardinality a) -> Integer)
-> (Finiteness a -> Finite (Cardinality a))
-> Finiteness a
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Finite (Cardinality a)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite (a -> Finite (Cardinality a))
-> (Finiteness a -> a) -> Finiteness a -> Finite (Cardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finiteness a -> a
forall a. Finiteness a -> a
unFiniteness
instance (Finitary a) => Binary (Finiteness a) where
{-# INLINE put #-}
put :: Finiteness a -> Put
put = Integer -> Put
forall t. Binary t => t -> Put
put (Integer -> Put)
-> (Finiteness a -> Integer) -> Finiteness a -> Put
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral @_ @Integer (Finite (Cardinality a) -> Integer)
-> (Finiteness a -> Finite (Cardinality a))
-> Finiteness a
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Finite (Cardinality a)
forall a. Finitary a => a -> Finite (Cardinality a)
toFinite (a -> Finite (Cardinality a))
-> (Finiteness a -> a) -> Finiteness a -> Finite (Cardinality a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finiteness a -> a
forall a. Finiteness a -> a
unFiniteness
{-# INLINE get #-}
get :: Get (Finiteness a)
get = a -> Finiteness a
forall a. a -> Finiteness a
Finiteness (a -> Finiteness a) -> (Integer -> a) -> Integer -> Finiteness a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite (Cardinality a) -> a
forall a. Finitary a => Finite (Cardinality a) -> a
fromFinite (Finite (Cardinality a) -> a)
-> (Integer -> Finite (Cardinality a)) -> Integer -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral @Integer (Integer -> Finiteness a) -> Get Integer -> Get (Finiteness a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get Integer
forall t. Binary t => Get t
get