witness-0.2: values that witness types

Data.Witness.Representative

Synopsis

Documentation

class Eq1 p whereSource

Methods

equals1 :: forall a. p a -> p a -> BoolSource

Instances

Eq1 Type 
Eq1 Nat 
Eq1 (RepWitness rep) 
Eq1 w => Eq1 (ListType w) 

data RepWitness rep a whereSource

Constructors

MkRepWitness :: Is rep a => RepWitness rep a 

Instances

class Eq1 rep => Representative rep whereSource

Methods

getRepWitness :: rep a -> RepWitness rep aSource

Every value is an instance of Is.

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

class Representative rep => Is rep a whereSource

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

Methods

representative :: rep aSource

The representative value for type a.

Instances

Is Type a 
Is Nat Zero 
Is Nat n => Is Nat (Succ n) 
Is rep a => Is (RepWitness rep) a 
Representative w => Is (ListType w) () 
(Is w a, Is (ListType w) b) => Is (ListType w) (a, b) 

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

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

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

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