Safe Haskell	Safe
Language	Haskell98

Data.Witness.Representative

Synopsis

class Eq1 (p :: k -> *) where
isWitnessRepresentative :: Dict (Is rep a) -> rep a
class Eq1 rep => Representative (rep :: k -> *) where
withRepresentative :: forall (rep :: k -> *) r. Representative rep => (forall (a :: k). Is rep a => rep a -> r) -> forall (b :: k). rep b -> r
class Representative rep => Is (rep :: k -> *) (a :: k) where
getRepresentative :: Is rep a => a -> rep a
rerepresentative :: Is rep a => p a -> rep a
mkAny :: Is rep a => a -> Any rep
mkAnyF :: Is rep a => f a -> AnyF rep f

Documentation

class Eq1 (p :: k -> *) where #

Minimal complete definition

Methods

equals1 :: forall a. p a -> p a -> Bool #

Instances

Eq1 NatType #
Instance details Defined in Data.Witness.Nat Methods equals1 :: NatType a -> NatType a -> Bool #
Eq1 w => Eq1 (ListType w :: * -> *) #
Instance details Defined in Data.Witness.List Methods equals1 :: ListType w a -> ListType w a -> Bool #
Eq1 (Proxy :: k -> *) #
Instance details Defined in Data.Witness.Representative Methods equals1 :: Proxy a -> Proxy a -> Bool #

class Eq1 rep => Representative (rep :: k -> *) where #

Minimal complete definition

Methods

getRepWitness :: forall (a :: k). rep a -> Dict (Is rep a) #

Every value is an instance of Is.

Instances

Representative NatType #
Instance details Defined in Data.Witness.Nat Methods getRepWitness :: NatType a -> Dict (Is NatType a) #
Representative w => Representative (ListType w :: * -> *) #
Instance details Defined in Data.Witness.List Methods getRepWitness :: ListType w a -> Dict (Is (ListType w) a) #
Representative (Proxy :: k -> *) #
Instance details Defined in Data.Witness.Representative Methods getRepWitness :: Proxy a -> Dict (Is Proxy a) #

withRepresentative :: forall (rep :: k -> *) r. Representative rep => (forall (a :: k). Is rep a => rep a -> r) -> forall (b :: k). rep b -> r #

class Representative rep => Is (rep :: k -> *) (a :: k) where #

If two representatives have the same type, then they have the same value.

Minimal complete definition

Methods

The representative value for type a.

Instances

Is NatType Zero #
Instance details Defined in Data.Witness.Nat Methods representative :: NatType Zero #
Is NatType n => Is NatType (Succ n :: Nat) #
Instance details Defined in Data.Witness.Nat Methods representative :: NatType (Succ n) #
Representative w => Is (ListType w :: * -> *) () #
Instance details Defined in Data.Witness.List Methods representative :: ListType w () #
Is (Proxy :: k -> *) (a :: k) #
Instance details Defined in Data.Witness.Representative Methods representative :: Proxy a #
(Is w a, Is (ListType w) lt) => Is (ListType w :: * -> ) ((a, lt) :: ) #
Instance details Defined in Data.Witness.List Methods representative :: ListType w (a, lt) #

getRepresentative :: Is rep a => a -> rep a #

rerepresentative :: Is rep a => p a -> rep a #

mkAny :: Is rep a => a -> Any rep #

mkAnyF :: Is rep a => f a -> AnyF rep f #