Safe Haskell	None
Language	Haskell2010

Exinst.Singletons

Contents

1 type index
2 type indexes
3 type indexes
4 type indexes
Re-exports

Description

See the README file for documentation: https://hackage.haskell.org/package/exinst#readme

Synopsis

1 type index

data Some1 f1 Source #

Constructors

Some1 !(Sing a1) !(f1 a1)

some1 Source #

Arguments

:: forall (f1 :: k1 -> Type). SingI a1
=> f1 a1
-> Some1 f1

fromSome1 Source #

Arguments

:: forall (f1 :: k1 -> Type). (SingI a1, SDecide k1)
=> Some1 f1
-> Maybe (f1 a1)

_Some1 :: forall f1 a1. (SingI a1, SDecide k1) => Prism' (Some1 f1) (f1 a1) Source #

withSome1 Source #

Arguments

:: forall (f1 :: k1 -> Type) (r :: Type). Some1 f1
-> (forall a1. SingI a1 => f1 a1 -> r)
-> r

withSome1Sing Source #

Arguments

:: forall (f1 :: k1 -> Type) (r :: Type). Some1 f1
-> (forall a1. SingI a1 => Sing a1 -> f1 a1 -> r)
-> r

Like withSome1, but takes an explicit Sing besides the SingI instance.

some1SingRep Source #

Arguments

:: SingKind k1
=> Some1 (f1 :: k1 -> Type)
-> DemoteRep k1

class Dict1 c f1 where Source #

Minimal complete definition

dict1

Methods

dict1 :: Sing a1 -> Dict (c (f1 a1)) Source #

Runtime lookup of the c (f1 a1) instance.

2 type indexes

data Some2 f2 Source #

Constructors

Some2 !(Sing a2) !(Sing a1) !(f2 a2 a1)

some2 Source #

Arguments

:: forall (f2 :: k2 -> k1 -> Type). (SingI a2, SingI a1)
=> f2 a2 a1
-> Some2 f2

fromSome2 Source #

Arguments

:: forall (f2 :: k2 -> k1 -> Type). (SingI a2, SDecide k2, SingI a1, SDecide k1)
=> Some2 f2
-> Maybe (f2 a2 a1)

_Some2 :: forall f2 a2 a1. (SingI a2, SDecide k2, SingI a1, SDecide k1) => Prism' (Some2 f2) (f2 a2 a1) Source #

withSome2 Source #

Arguments

:: forall (f2 :: k2 -> k1 -> Type) (r :: Type). Some2 f2
-> (forall a2 a1. (SingI a2, SingI a1) => f2 a2 a1 -> r)
-> r

withSome2Sing Source #

Arguments

:: forall (f2 :: k2 -> k1 -> Type) (r :: Type). Some2 f2
-> (forall a2 a1. (SingI a2, SingI a1) => Sing a2 -> Sing a1 -> f2 a2 a1 -> r)
-> r

Like withSome2, but takes explicit Sings besides the SingI instances.

some2SingRep Source #

Arguments

:: (SingKind k2, SingKind k1)
=> Some2 (f2 :: k2 -> k1 -> Type)
-> (DemoteRep k2, DemoteRep k1)

class Dict2 c f2 where Source #

Minimal complete definition

dict2

Methods

dict2 :: Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1)) Source #

3 type indexes

data Some3 f3 Source #

Constructors

Some3 !(Sing a3) !(Sing a2) !(Sing a1) !(f3 a3 a2 a1)

some3 Source #

Arguments

:: forall (f3 :: k3 -> k2 -> k1 -> Type). (SingI a3, SingI a2, SingI a1)
=> f3 a3 a2 a1
-> Some3 f3

fromSome3 Source #

Arguments

:: forall (f3 :: k3 -> k2 -> k1 -> Type). (SingI a3, SDecide k3, SingI a2, SDecide k2, SingI a1, SDecide k1)
=> Some3 f3
-> Maybe (f3 a3 a2 a1)

_Some3 :: forall f3 a3 a2 a1. (SingI a3, SDecide k3, SingI a2, SDecide k2, SingI a1, SDecide k1) => Prism' (Some3 f3) (f3 a3 a2 a1) Source #

withSome3 Source #

Arguments

:: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type). Some3 f3
-> (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f3 a3 a2 a1 -> r)
-> r

withSome3Sing Source #

Arguments

:: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type). Some3 f3
-> (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r)
-> r

Like withSome3, but takes explicit Sings besides the SingI instances.

some3SingRep Source #

Arguments

:: (SingKind k3, SingKind k2, SingKind k1)
=> Some3 (f3 :: k3 -> k2 -> k1 -> Type)
-> (DemoteRep k3, DemoteRep k2, DemoteRep k1)

class Dict3 c f3 where Source #

Minimal complete definition

dict3

Methods

dict3 :: Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1)) Source #

4 type indexes

data Some4 f4 Source #

Constructors

Some4 !(Sing a4) !(Sing a3) !(Sing a2) !(Sing a1) !(f4 a4 a3 a2 a1)

some4 Source #

Arguments

:: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type). (SingI a4, SingI a3, SingI a2, SingI a1)
=> f4 a4 a3 a2 a1
-> Some4 f4

fromSome4 Source #

Arguments

:: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type). (SingI a4, SDecide k4, SingI a3, SDecide k3, SingI a2, SDecide k2, SingI a1, SDecide k1)
=> Some4 f4
-> Maybe (f4 a4 a3 a2 a1)

_Some4 :: forall f4 a4 a3 a2 a1. (SingI a4, SDecide k4, SingI a3, SDecide k3, SingI a2, SDecide k2, SingI a1, SDecide k1) => Prism' (Some4 f4) (f4 a4 a3 a2 a1) Source #

withSome4 Source #

Arguments

:: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type). Some4 f4
-> (forall a4 a3 a2 a1. (SingI a4, SingI a3, SingI a2, SingI a1) => f4 a4 a3 a2 a1 -> r)
-> r

withSome4Sing Source #

Arguments

:: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type). Some4 f4
-> (forall a4 a3 a2 a1. (SingI a4, SingI a3, SingI a2, SingI a1) => Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r)
-> r

Like withSome4, but takes explicit Sings besides the SingI instances.

some4SingRep Source #

Arguments

:: (SingKind k4, SingKind k3, SingKind k2, SingKind k1)
=> Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type)
-> (DemoteRep k4, DemoteRep k3, DemoteRep k2, DemoteRep k1)

class Dict4 c f4 where Source #

Minimal complete definition

dict4

Methods

dict4 :: Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1)) Source #

Re-exports

data Dict a :: Constraint -> * where #

Values of type Dict p capture a dictionary for a constraint of type p.

e.g.

Dict :: Dict (Eq Int)

captures a dictionary that proves we have an:

instance Eq 'Int

Pattern matching on the Dict constructor will bring this instance into scope.

Constructors

Dict :: Dict a

Instances

a :=> (Read (Dict a))
Methods ins :: a :- Read (Dict a) #
a :=> (Monoid (Dict a))
Methods ins :: a :- Monoid (Dict a) #
a :=> (Enum (Dict a))
Methods ins :: a :- Enum (Dict a) #
a :=> (Bounded (Dict a))
Methods ins :: a :- Bounded (Dict a) #
() :=> (Eq (Dict a))
Methods ins :: () :- Eq (Dict a) #
() :=> (Ord (Dict a))
Methods ins :: () :- Ord (Dict a) #
() :=> (Show (Dict a))
Methods ins :: () :- Show (Dict a) #
a => Bounded (Dict a)
Methods minBound :: Dict a # maxBound :: Dict a #
a => Enum (Dict a)
Methods succ :: Dict a -> Dict a # pred :: Dict a -> Dict a # toEnum :: Int -> Dict a # fromEnum :: Dict a -> Int # enumFrom :: Dict a -> [Dict a] # enumFromThen :: Dict a -> Dict a -> [Dict a] # enumFromTo :: Dict a -> Dict a -> [Dict a] # enumFromThenTo :: Dict a -> Dict a -> Dict a -> [Dict a] #
Eq (Dict a)
Methods (==) :: Dict a -> Dict a -> Bool # (/=) :: Dict a -> Dict a -> Bool #
(Typeable Constraint p, p) => Data (Dict p)
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Dict p -> c (Dict p) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Dict p) # toConstr :: Dict p -> Constr # dataTypeOf :: Dict p -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (Dict p)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Dict p)) # gmapT :: (forall b. Data b => b -> b) -> Dict p -> Dict p # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Dict p -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Dict p -> r # gmapQ :: (forall d. Data d => d -> u) -> Dict p -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Dict p -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Dict p -> m (Dict p) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Dict p -> m (Dict p) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Dict p -> m (Dict p) #
Ord (Dict a)
Methods compare :: Dict a -> Dict a -> Ordering # (<) :: Dict a -> Dict a -> Bool # (<=) :: Dict a -> Dict a -> Bool # (>) :: Dict a -> Dict a -> Bool # (>=) :: Dict a -> Dict a -> Bool # max :: Dict a -> Dict a -> Dict a # min :: Dict a -> Dict a -> Dict a #
a => Read (Dict a)
Methods readsPrec :: Int -> ReadS (Dict a) # readList :: ReadS [Dict a] # readPrec :: ReadPrec (Dict a) # readListPrec :: ReadPrec [Dict a] #
Show (Dict a)
Methods showsPrec :: Int -> Dict a -> ShowS # show :: Dict a -> String # showList :: [Dict a] -> ShowS #
a => Monoid (Dict a)
Methods mempty :: Dict a # mappend :: Dict a -> Dict a -> Dict a # mconcat :: [Dict a] -> Dict a #