| 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
- getRepWitness :: forall (a :: k). rep a -> Dict (Is rep 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
- representative :: rep a
- 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
isWitnessRepresentative :: Dict (Is rep a) -> rep a #
class Eq1 rep => Representative (rep :: k -> *) where #
Methods
getRepWitness :: forall (a :: k). rep a -> Dict (Is rep a) #
Every value is an instance of Is.
Instances
| Representative NatType # | |
Defined in Data.Witness.Nat | |
| Representative (Proxy :: k -> Type) # | |
Defined in Data.Witness.Representative | |
| Representative w => Representative (ListType w :: Type -> Type) # | |
Defined in Data.Witness.List | |
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.
Instances
| Is NatType Zero # | |
Defined in Data.Witness.Nat Methods | |
| Is NatType n => Is NatType (Succ n :: Nat) # | |
Defined in Data.Witness.Nat Methods representative :: NatType (Succ n) # | |
| Is (Proxy :: k -> Type) (a :: k) # | |
Defined in Data.Witness.Representative Methods representative :: Proxy a # | |
| Representative w => Is (ListType w :: Type -> Type) () # | |
Defined in Data.Witness.List Methods representative :: ListType w () # | |
| (Is w a, Is (ListType w) lt) => Is (ListType w :: Type -> Type) ((a, lt) :: Type) # | |
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 #