Generics.Simplistic.Util

Utility Functions and Types

(&&&) :: Arrow a => a b c -> a b c' -> a b (c, c') infixr 3

Fanout: send the input to both argument arrows and combine their output.

The default definition may be overridden with a more efficient version if desired.

(***) :: Arrow a => a b c -> a b' c' -> a (b, b') (c, c') infixr 3

Split the input between the two argument arrows and combine their output. Note that this is in general not a functor.

The default definition may be overridden with a more efficient version if desired.

type (:->) f g = forall n. f n -> g n

Natural transformations

(<.>) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c infixr 8

Kleisli Composition

Poly-kind indexed product functionality

data ((f :: k -> Type) :*: (g :: k -> Type)) (p :: k) :: forall k. (k -> Type) -> (k -> Type) -> k -> Type infixr 6

Products: encode multiple arguments to constructors

Constructors

(f p) :*: (g p) infixr 6

Instances

(GDeep kappa fam f, GDeep kappa fam g) => GDeep kappa fam (f :*: g :: k -> Type)

Defined in Generics.Simplistic.Deep

Methods

gdfrom :: (f :*: g) x -> SRep (SFix kappa fam) (f :*: g)

gdto :: SRep (SFix kappa fam) (f :*: g) -> (f :*: g) x

Generic1 (f :*: g :: k -> Type)

Defined in GHC.Generics

Associated Types

type Rep1 (f :*: g) :: k -> Type

Methods

from1 :: (f :*: g) a -> Rep1 (f :*: g) a

to1 :: Rep1 (f :*: g) a -> (f :*: g) a

(GNFData arity a, GNFData arity b) => GNFData arity (a :*: b)

Defined in Control.DeepSeq

Methods

grnf :: RnfArgs arity a0 -> (a :*: b) a0 -> ()

(ShowHO f, ShowHO g) => ShowHO (f :*: g :: ki -> Type)

Defined in Generics.Simplistic.Util

Methods

showHO :: (f :*: g) k -> String

showsPrecHO :: Int -> (f :*: g) k -> ShowS

(EqHO f, EqHO g) => EqHO (f :*: g :: ki -> Type)

Defined in Generics.Simplistic.Util

Methods

eqHO :: (f :*: g) k -> (f :*: g) k -> Bool

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

Defined in Generics.Simplistic

Methods

sfrom :: (f :*: g) x -> SRep I (f :*: g)

sto :: SRep I (f :*: g) -> (f :*: g) x

(Monad f, Monad g) => Monad (f :*: g)

Since: base-4.9.0.0

Defined in GHC.Generics

Methods

(>>=) :: (f :*: g) a -> (a -> (f :*: g) b) -> (f :*: g) b

(>>) :: (f :*: g) a -> (f :*: g) b -> (f :*: g) b

return :: a -> (f :*: g) a

fail :: String -> (f :*: g) a

(Functor f, Functor g) => Functor (f :*: g)

Since: base-4.9.0.0

Defined in GHC.Generics

Methods

fmap :: (a -> b) -> (f :*: g) a -> (f :*: g) b

(<$) :: a -> (f :*: g) b -> (f :*: g) a

(MonadFix f, MonadFix g) => MonadFix (f :*: g)

Since: base-4.9.0.0

Defined in Control.Monad.Fix

Methods

mfix :: (a -> (f :*: g) a) -> (f :*: g) a

(Applicative f, Applicative g) => Applicative (f :*: g)

Since: base-4.9.0.0

Defined in GHC.Generics

Methods

pure :: a -> (f :*: g) a

(<*>) :: (f :*: g) (a -> b) -> (f :*: g) a -> (f :*: g) b

liftA2 :: (a -> b -> c) -> (f :*: g) a -> (f :*: g) b -> (f :*: g) c

(*>) :: (f :*: g) a -> (f :*: g) b -> (f :*: g) b

(<*) :: (f :*: g) a -> (f :*: g) b -> (f :*: g) a

(Foldable f, Foldable g) => Foldable (f :*: g)

Since: base-4.9.0.0

Defined in Data.Foldable

Methods

fold :: Monoid m => (f :*: g) m -> m

foldMap :: Monoid m => (a -> m) -> (f :*: g) a -> m

foldr :: (a -> b -> b) -> b -> (f :*: g) a -> b

foldr' :: (a -> b -> b) -> b -> (f :*: g) a -> b

foldl :: (b -> a -> b) -> b -> (f :*: g) a -> b

foldl' :: (b -> a -> b) -> b -> (f :*: g) a -> b

foldr1 :: (a -> a -> a) -> (f :*: g) a -> a

foldl1 :: (a -> a -> a) -> (f :*: g) a -> a

toList :: (f :*: g) a -> [a]

null :: (f :*: g) a -> Bool

length :: (f :*: g) a -> Int

elem :: Eq a => a -> (f :*: g) a -> Bool

maximum :: Ord a => (f :*: g) a -> a

minimum :: Ord a => (f :*: g) a -> a

sum :: Num a => (f :*: g) a -> a

product :: Num a => (f :*: g) a -> a

(Traversable f, Traversable g) => Traversable (f :*: g)

Since: base-4.9.0.0

Defined in Data.Traversable

Methods

traverse :: Applicative f0 => (a -> f0 b) -> (f :*: g) a -> f0 ((f :*: g) b)

sequenceA :: Applicative f0 => (f :*: g) (f0 a) -> f0 ((f :*: g) a)

mapM :: Monad m => (a -> m b) -> (f :*: g) a -> m ((f :*: g) b)

sequence :: Monad m => (f :*: g) (m a) -> m ((f :*: g) a)

(Alternative f, Alternative g) => Alternative (f :*: g)

Since: base-4.9.0.0

Defined in GHC.Generics

Methods

empty :: (f :*: g) a

(<|>) :: (f :*: g) a -> (f :*: g) a -> (f :*: g) a

some :: (f :*: g) a -> (f :*: g) [a]

many :: (f :*: g) a -> (f :*: g) [a]

(MonadPlus f, MonadPlus g) => MonadPlus (f :*: g)

Since: base-4.9.0.0

Defined in GHC.Generics

Methods

mzero :: (f :*: g) a

mplus :: (f :*: g) a -> (f :*: g) a -> (f :*: g) a

(GShallow1 f, GShallow1 g) => GShallow1 (f :*: g)

Defined in Generics.Simplistic

Methods

sfrom1 :: (f :*: g) a -> SRep1 (f :*: g) a

sto1 :: SRep1 (f :*: g) a -> (f :*: g) a

(Eq (f p), Eq (g p)) => Eq ((f :*: g) p)

Since: base-4.7.0.0

Defined in GHC.Generics

Methods

(==) :: (f :*: g) p -> (f :*: g) p -> Bool

(/=) :: (f :*: g) p -> (f :*: g) p -> Bool

(Ord (f p), Ord (g p)) => Ord ((f :*: g) p)

Since: base-4.7.0.0

Defined in GHC.Generics

Methods

compare :: (f :*: g) p -> (f :*: g) p -> Ordering

(<) :: (f :*: g) p -> (f :*: g) p -> Bool

(<=) :: (f :*: g) p -> (f :*: g) p -> Bool

(>) :: (f :*: g) p -> (f :*: g) p -> Bool

(>=) :: (f :*: g) p -> (f :*: g) p -> Bool

max :: (f :*: g) p -> (f :*: g) p -> (f :*: g) p

min :: (f :*: g) p -> (f :*: g) p -> (f :*: g) p

(Read (f p), Read (g p)) => Read ((f :*: g) p)

Since: base-4.7.0.0

Defined in GHC.Generics

Methods

readsPrec :: Int -> ReadS ((f :*: g) p)

readList :: ReadS [(f :*: g) p]

readPrec :: ReadPrec ((f :*: g) p)

readListPrec :: ReadPrec [(f :*: g) p]

(Show (f p), Show (g p)) => Show ((f :*: g) p)

Since: base-4.7.0.0

Defined in GHC.Generics

Methods

showsPrec :: Int -> (f :*: g) p -> ShowS

show :: (f :*: g) p -> String

showList :: [(f :*: g) p] -> ShowS

Generic ((f :*: g) p)

Defined in GHC.Generics

Associated Types

type Rep ((f :*: g) p) :: Type -> Type

Methods

from :: (f :*: g) p -> Rep ((f :*: g) p) x

to :: Rep ((f :*: g) p) x -> (f :*: g) p

(Semigroup (f p), Semigroup (g p)) => Semigroup ((f :*: g) p)

Since: base-4.12.0.0

Defined in GHC.Generics

Methods

(<>) :: (f :*: g) p -> (f :*: g) p -> (f :*: g) p

sconcat :: NonEmpty ((f :*: g) p) -> (f :*: g) p

stimes :: Integral b => b -> (f :*: g) p -> (f :*: g) p

(Monoid (f p), Monoid (g p)) => Monoid ((f :*: g) p)

Since: base-4.12.0.0

Defined in GHC.Generics

Methods

mempty :: (f :*: g) p

mappend :: (f :*: g) p -> (f :*: g) p -> (f :*: g) p

mconcat :: [(f :*: g) p] -> (f :*: g) p

type Rep1 (f :*: g :: k -> Type)

Since: base-4.9.0.0

Defined in GHC.Generics

type Rep1 (f :*: g :: k -> Type) = D1 (MetaData ":*:" "GHC.Generics" "base" False) (C1 (MetaCons ":*:" (InfixI RightAssociative 6) False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec1 f) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec1 g)))

type Rep ((f :*: g) p)

Since: base-4.7.0.0

Defined in GHC.Generics

type Rep ((f :*: g) p) = D1 (MetaData ":*:" "GHC.Generics" "base" False) (C1 (MetaCons ":*:" (InfixI RightAssociative 6) False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (f p)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (g p))))

type Delta f = f :*: f

Diagonal indexed functor

curry' :: ((f :*: g) x -> a) -> f x -> g x -> a

Lifted curry

uncurry' :: (f x -> g x -> a) -> (f :*: g) x -> a

Lifted uncurry

delta :: f :-> Delta f

Duplicates its argument

deltaMap :: (f :-> g) -> Delta f :-> Delta g

Applies the same function to both components of the pair

Poly-kind indexed sums

data Sum (f :: k -> Type) (g :: k -> Type) (a :: k) :: forall k. (k -> Type) -> (k -> Type) -> k -> Type

Lifted sum of functors.

Constructors

InL (f a)

InR (g a)

Instances

Generic1 (Sum f g :: k -> Type)

Defined in Data.Functor.Sum

Associated Types

type Rep1 (Sum f g) :: k -> Type

Methods

from1 :: Sum f g a -> Rep1 (Sum f g) a

to1 :: Rep1 (Sum f g) a -> Sum f g a

(ShowHO f, ShowHO g) => ShowHO (Sum f g :: ki -> Type)

Defined in Generics.Simplistic.Util

Methods

showHO :: Sum f g k -> String

showsPrecHO :: Int -> Sum f g k -> ShowS

(EqHO f, EqHO g) => EqHO (Sum f g :: ki -> Type)

Defined in Generics.Simplistic.Util

Methods

eqHO :: Sum f g k -> Sum f g k -> Bool

(Functor f, Functor g) => Functor (Sum f g)

Since: base-4.9.0.0

Defined in Data.Functor.Sum

Methods

fmap :: (a -> b) -> Sum f g a -> Sum f g b

(<$) :: a -> Sum f g b -> Sum f g a

(Foldable f, Foldable g) => Foldable (Sum f g)

Since: base-4.9.0.0

Defined in Data.Functor.Sum

Methods

fold :: Monoid m => Sum f g m -> m

foldMap :: Monoid m => (a -> m) -> Sum f g a -> m

foldr :: (a -> b -> b) -> b -> Sum f g a -> b

foldr' :: (a -> b -> b) -> b -> Sum f g a -> b

foldl :: (b -> a -> b) -> b -> Sum f g a -> b

foldl' :: (b -> a -> b) -> b -> Sum f g a -> b

foldr1 :: (a -> a -> a) -> Sum f g a -> a

foldl1 :: (a -> a -> a) -> Sum f g a -> a

toList :: Sum f g a -> [a]

null :: Sum f g a -> Bool

length :: Sum f g a -> Int

elem :: Eq a => a -> Sum f g a -> Bool

maximum :: Ord a => Sum f g a -> a

minimum :: Ord a => Sum f g a -> a

sum :: Num a => Sum f g a -> a

product :: Num a => Sum f g a -> a

(Traversable f, Traversable g) => Traversable (Sum f g)

Since: base-4.9.0.0

Defined in Data.Functor.Sum

Methods

traverse :: Applicative f0 => (a -> f0 b) -> Sum f g a -> f0 (Sum f g b)

sequenceA :: Applicative f0 => Sum f g (f0 a) -> f0 (Sum f g a)

mapM :: Monad m => (a -> m b) -> Sum f g a -> m (Sum f g b)

sequence :: Monad m => Sum f g (m a) -> m (Sum f g a)

(Eq1 f, Eq1 g) => Eq1 (Sum f g)

Since: base-4.9.0.0

Defined in Data.Functor.Sum

Methods

liftEq :: (a -> b -> Bool) -> Sum f g a -> Sum f g b -> Bool

(Ord1 f, Ord1 g) => Ord1 (Sum f g)

Since: base-4.9.0.0

Defined in Data.Functor.Sum

Methods

liftCompare :: (a -> b -> Ordering) -> Sum f g a -> Sum f g b -> Ordering

(Read1 f, Read1 g) => Read1 (Sum f g)

Since: base-4.9.0.0

Defined in Data.Functor.Sum

Methods

liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Sum f g a)

liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [Sum f g a]

liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (Sum f g a)

liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [Sum f g a]

(Show1 f, Show1 g) => Show1 (Sum f g)

Since: base-4.9.0.0

Defined in Data.Functor.Sum

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Sum f g a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Sum f g a] -> ShowS

(NFData1 f, NFData1 g) => NFData1 (Sum f g)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

liftRnf :: (a -> ()) -> Sum f g a -> ()

(Eq1 f, Eq1 g, Eq a) => Eq (Sum f g a)

Since: base-4.9.0.0

Defined in Data.Functor.Sum

Methods

(==) :: Sum f g a -> Sum f g a -> Bool

(/=) :: Sum f g a -> Sum f g a -> Bool

(Typeable a, Typeable f, Typeable g, Typeable k, Data (f a), Data (g a)) => Data (Sum f g a)

Since: base-4.9.0.0

Defined in Data.Functor.Sum

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g0. g0 -> c g0) -> Sum f g a -> c (Sum f g a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Sum f g a)

toConstr :: Sum f g a -> Constr

dataTypeOf :: Sum f g a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Sum f g a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Sum f g a))

gmapT :: (forall b. Data b => b -> b) -> Sum f g a -> Sum f g a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sum f g a -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sum f g a -> r

gmapQ :: (forall d. Data d => d -> u) -> Sum f g a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Sum f g a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sum f g a -> m (Sum f g a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sum f g a -> m (Sum f g a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sum f g a -> m (Sum f g a)

(Ord1 f, Ord1 g, Ord a) => Ord (Sum f g a)

Since: base-4.9.0.0

Defined in Data.Functor.Sum

Methods

compare :: Sum f g a -> Sum f g a -> Ordering

(<) :: Sum f g a -> Sum f g a -> Bool

(<=) :: Sum f g a -> Sum f g a -> Bool

(>) :: Sum f g a -> Sum f g a -> Bool

(>=) :: Sum f g a -> Sum f g a -> Bool

max :: Sum f g a -> Sum f g a -> Sum f g a

min :: Sum f g a -> Sum f g a -> Sum f g a

(Read1 f, Read1 g, Read a) => Read (Sum f g a)

Since: base-4.9.0.0

Defined in Data.Functor.Sum

Methods

readsPrec :: Int -> ReadS (Sum f g a)

readList :: ReadS [Sum f g a]

readPrec :: ReadPrec (Sum f g a)

readListPrec :: ReadPrec [Sum f g a]

(Show1 f, Show1 g, Show a) => Show (Sum f g a)

Since: base-4.9.0.0

Defined in Data.Functor.Sum

Methods

showsPrec :: Int -> Sum f g a -> ShowS

show :: Sum f g a -> String

showList :: [Sum f g a] -> ShowS

Generic (Sum f g a)

Defined in Data.Functor.Sum

Associated Types

type Rep (Sum f g a) :: Type -> Type

Methods

from :: Sum f g a -> Rep (Sum f g a) x

to :: Rep (Sum f g a) x -> Sum f g a

(NFData1 f, NFData1 g, NFData a) => NFData (Sum f g a)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

rnf :: Sum f g a -> ()

type Rep1 (Sum f g :: k -> Type)

Since: base-4.9.0.0

Defined in Data.Functor.Sum

type Rep1 (Sum f g :: k -> Type) = D1 (MetaData "Sum" "Data.Functor.Sum" "base" False) (C1 (MetaCons "InL" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec1 f)) :+: C1 (MetaCons "InR" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec1 g)))

type Rep (Sum f g a)

Since: base-4.9.0.0

Defined in Data.Functor.Sum

type Rep (Sum f g a) = D1 (MetaData "Sum" "Data.Functor.Sum" "base" False) (C1 (MetaCons "InL" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (f a))) :+: C1 (MetaCons "InR" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (g a))))

either' :: (f :-> r) -> (g :-> r) -> Sum f g :-> r

Higher-order sum eliminator

either'' :: (forall x. f x -> a) -> (forall y. g y -> a) -> Sum f g r -> a

Just like either', but the result type is of kind Star

Constraints

class c => d => Implies c d

Constraint implication

Instances

c -> d => Implies c d

Defined in Generics.Simplistic.Util

class Trivial c

Trivial constraint

Instances

Trivial (c :: k)

Defined in Generics.Simplistic.Util

Higher-order Eq and Show

class EqHO (f :: ki -> *) where

Higher order , poly kinded, version of Eq

Methods

eqHO :: forall k. f k -> f k -> Bool

Instances

EqHO (U1 :: ki -> Type)

Defined in Generics.Simplistic.Util

Methods

eqHO :: U1 k -> U1 k -> Bool

EqHO (V1 :: ki -> Type)

Defined in Generics.Simplistic.Util

Methods

eqHO :: V1 k -> V1 k -> Bool

Eq a => EqHO (Const a :: ki -> Type)

Defined in Generics.Simplistic.Util

Methods

eqHO :: Const a k -> Const a k -> Bool

(EqHO f, EqHO g) => EqHO (Sum f g :: ki -> Type)

Defined in Generics.Simplistic.Util

Methods

eqHO :: Sum f g k -> Sum f g k -> Bool

(EqHO f, EqHO g) => EqHO (f :*: g :: ki -> Type)

Defined in Generics.Simplistic.Util

Methods

eqHO :: (f :*: g) k -> (f :*: g) k -> Bool

(All Eq kappa, EqHO h) => EqHO (Holes kappa fam h :: Type -> Type)

Defined in Generics.Simplistic.Deep

Methods

eqHO :: Holes kappa fam h k -> Holes kappa fam h k -> Bool

class ShowHO (f :: ki -> *) where

Higher order, poly kinded, version of Show; We provide the same showsPrec mechanism. The documentation of Text.Show has a good example of the correct usage of showsPrec:

infixr 5 :^:
data Tree a =  Leaf a  |  Tree a :^: Tree a

instance (Show a) => Show (Tree a) where
  showsPrec d (Leaf m) = showParen (d > app_prec) $
       showString "Leaf " . showsPrec (app_prec+1) m
    where app_prec = 10

  showsPrec d (u :^: v) = showParen (d > up_prec) $
       showsPrec (up_prec+1) u .
       showString " :^: "      .
       showsPrec (up_prec+1) v
    where up_prec = 5

Minimal complete definition

showHO | showsPrecHO

Methods

showHO :: forall k. f k -> String

showsPrecHO :: forall k. Int -> f k -> ShowS

Instances

Show a => ShowHO (Const a :: ki -> Type)

Defined in Generics.Simplistic.Util

Methods

showHO :: Const a k -> String

showsPrecHO :: Int -> Const a k -> ShowS

(ShowHO f, ShowHO g) => ShowHO (Sum f g :: ki -> Type)

Defined in Generics.Simplistic.Util

Methods

showHO :: Sum f g k -> String

showsPrecHO :: Int -> Sum f g k -> ShowS

(ShowHO f, ShowHO g) => ShowHO (f :*: g :: ki -> Type)

Defined in Generics.Simplistic.Util

Methods

showHO :: (f :*: g) k -> String

showsPrecHO :: Int -> (f :*: g) k -> ShowS

Existential Wrapper

data Exists (f :: k -> *) :: * where

Existential type wrapper. This comesin particularly handy when we want to add mrsop terms to some container. See Generics.MRSOP.Holes.Unify for example.

Constructors

Exists :: f x -> Exists f

Instances

ShowHO f => Show (Exists f)

Defined in Generics.Simplistic.Util

Methods

showsPrec :: Int -> Exists f -> ShowS

show :: Exists f -> String

showList :: [Exists f] -> ShowS

exMap :: (forall x. f x -> g x) -> Exists f -> Exists g

Maps over Exists

exMapM :: Monad m => (forall x. f x -> m (g x)) -> Exists f -> m (Exists g)

Maps a monadic actino over Exists

exElim :: (forall x. f x -> a) -> Exists f -> a

eliminates an Exists

Elem functionality

type Elem a as = (IsElem a as ~ True, HasElem a as)

We will carry constructive information on the constraint. Forcing IsElem to true

type NotElem a as = IsElem a as ~ False

Negation of Elem

class HasElem a as where

Methods

hasElem :: ElemPrf a as

Instances

HasElem a2 as => HasElem (a2 :: a1) (b ': as :: [a1])

Defined in Generics.Simplistic.Util

Methods

hasElem :: ElemPrf a2 (b ': as)

HasElem (a2 :: a1) (a2 ': as :: [a1])

Defined in Generics.Simplistic.Util

Methods

hasElem :: ElemPrf a2 (a2 ': as)

data ElemPrf a as where

Constructors

Here :: ElemPrf a (a ': as)

There :: ElemPrf a as -> ElemPrf a (b ': as)

type family IsElem (a :: k) (as :: [k]) :: Bool where ...

Equations

IsElem a (a ': as) = True

IsElem a (b ': as) = IsElem a as

IsElem a '[] = False

sameTy :: forall fam x y. (Elem x fam, Elem y fam) => Proxy fam -> Proxy x -> Proxy y -> Maybe (x :~: y)

Returns whether two types are the same, given that both belong to the same list.

Witnessing and All constraints

type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where ...

Equations

All c '[] = ()

All c (x ': xs) = (c x, All c xs)

data Witness c x where

Carries information about x being an instance of c

Constructors

Witness :: c x => Witness c x

witness :: forall x xs c. (HasElem x xs, All c xs) => Proxy xs -> Witness c x

Provides the witness that x is an instance of c

witnessPrf :: All c xs => ElemPrf x xs -> Witness c x

Provides the witness that x is an instance of c

weq :: forall x xs. (All Eq xs, Elem x xs) => Proxy xs -> x -> x -> Bool

Fetches the Eq instance for an element of a list

wshow :: forall x xs. (All Show xs, Elem x xs) => Proxy xs -> x -> String

Fetches the Eq instance for an element of a list