Safe Haskell	None
Language	Haskell2010

Exinst.Singletons

Contents

1 type index
2 type indexes
3 type indexes
4 type indexes

Description

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

Synopsis

1 type index

data Some1 f1 Source

some1 Source

Arguments

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

withSome1Sing Source

Arguments

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

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

withSome1 Source

Arguments

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

fromSome1 Source

Arguments

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

class Dict1 c f1 where Source

Methods

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

2 type indexes

data Some2 f2 Source

some2 Source

Arguments

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

withSome2Sing Source

Arguments

:: forall (f2 :: k2 -> k1 -> ) (r :: ). 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.

withSome2 Source

Arguments

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

fromSome2 Source

Arguments

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

class Dict2 c f2 where Source

Methods

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

3 type indexes

data Some3 f3 Source

some3 Source

Arguments

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

withSome3Sing Source

Arguments

:: forall (f3 :: k3 -> k2 -> k1 -> ) (r :: ). 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.

withSome3 Source

Arguments

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

fromSome3 Source

Arguments

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

class Dict3 c f3 where Source

Methods

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

4 type indexes

data Some4 f4 Source

some4 Source

Arguments

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

withSome4Sing Source

Arguments

:: forall (f4 :: k4 -> k3 -> k2 -> k1 -> ) (r :: ). 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.

withSome4 Source

Arguments

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

fromSome4 Source

Arguments

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

class Dict4 c f4 where Source

Methods

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