witness-0.4: values that witness types

Safe HaskellSafe
LanguageHaskell98

Data.Witness.Representative

Synopsis

Documentation

class Eq1 p where Source #

Minimal complete definition

equals1

Methods

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

Instances

Eq1 Nat NatType Source # 

Methods

equals1 :: p a -> p a -> Bool Source #

Eq1 * w => Eq1 * (ListType w) Source # 

Methods

equals1 :: p a -> p a -> Bool Source #

Eq1 k (Proxy k) Source # 

Methods

equals1 :: p a -> p a -> Bool Source #

isWitnessRepresentative :: Dict (Is rep a) -> rep a Source #

class Eq1 rep => Representative rep where Source #

Minimal complete definition

getRepWitness

Methods

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

Every value is an instance of Is.

Instances

Representative Nat NatType Source # 

Methods

getRepWitness :: rep a -> Dict (Is NatType rep a) Source #

Representative * w => Representative * (ListType w) Source # 

Methods

getRepWitness :: rep a -> Dict (Is (ListType w) rep a) Source #

Representative k (Proxy k) Source # 

Methods

getRepWitness :: rep a -> Dict (Is (Proxy k) rep a) Source #

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

class Representative rep => Is rep a where Source #

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

Minimal complete definition

representative

Methods

representative :: rep a Source #

The representative value for type a.

Instances

Is Nat NatType Zero Source # 
Is Nat NatType n => Is Nat NatType (Succ n) Source # 

Methods

representative :: Succ n a Source #

Representative * w => Is * (ListType w) () Source # 

Methods

representative :: () a Source #

Is k (Proxy k) a Source # 

Methods

representative :: a a Source #

(Is * w a, Is * (ListType w) lt) => Is * (ListType w) (a, lt) Source # 

Methods

representative :: (a, lt) a Source #

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

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

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

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