ten-0.1.0.0: Typeclasses like Functor, etc. over arity-1 type constructors.
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Ten.Entails

Description

A typeclass of GADT-like types whose existence implies an instance.

Synopsis

Documentation

class Entails k c where Source #

A typeclass of GADT-like types whose existence implies an instance.

For a trivial example, the existence of Int :~: b implies Show b, since we can discover that b is Int and use the Show Int instance.

Methods

entailment :: k a -> Dict1 c a Source #

Instances

Instances details
(forall (a :: k). c a) => Entails (Proxy :: k -> Type) (c :: k -> Constraint) Source # 
Instance details

Defined in Data.Ten.Entails

Methods

entailment :: forall (a :: k0). Proxy a -> Dict1 c a Source #

(forall (a :: k). c a) => Entails (TypeRep :: k -> Type) (c :: k -> Constraint) Source #

Non-GADTy types don't entail anything except parametric instances.

Instance details

Defined in Data.Ten.Entails

Methods

entailment :: forall (a :: k0). TypeRep a -> Dict1 c a Source #

Entails (Dict1 c :: k -> Type) (c :: k -> Constraint) Source #

Dict1s entail their own type parameter.

Instance details

Defined in Data.Ten.Entails

Methods

entailment :: forall (a :: k0). Dict1 c a -> Dict1 c a Source #

c a => Entails ((:~:) a :: k -> Type) (c :: k -> Constraint) Source #

Equality to a particular type entails any instance that type has.

Instance details

Defined in Data.Ten.Entails

Methods

entailment :: forall (a0 :: k0). (a :~: a0) -> Dict1 c a0 Source #

(Constrained10 c f, Applicative10 f) => Entails (Field10 f :: k -> Type) (c :: k -> Constraint) Source # 
Instance details

Defined in Data.Ten.Field

Methods

entailment :: forall (a :: k0). Field10 f a -> Dict1 c a Source #

data Dict1 (c :: k -> Constraint) a Source #

A dictionary for the given arity-1 constraint constructor ("a class").

Constructors

c a => Dict1 

Instances

Instances details
Entails (Dict1 c :: k -> Type) (c :: k -> Constraint) Source #

Dict1s entail their own type parameter.

Instance details

Defined in Data.Ten.Entails

Methods

entailment :: forall (a :: k0). Dict1 c a -> Dict1 c a Source #

class c (d a) => (c :!: d) a Source #

A utility "typeclass newtype" that's convenient with Entails.

If you want to use entailment to get an instance of the form c (d a), use entailment @(c :!: d). Really I wanted to use the name (:.:), but it's taken, so I just replaced the period with something else that involves a dot near the typographic base line.

Instances

Instances details
c (d a) => ((c :: k1 -> Constraint) :!: (d :: k2 -> k1)) (a :: k2) Source # 
Instance details

Defined in Data.Ten.Entails

withEntailment :: forall c k a r. Entails k c => k a -> (c a => r) -> r Source #

Bring an instance into scope using an Entails instance.

    ( (k :: Int :~: b) (x :: b) -> withEntailment @Show k (show x)) Refl 2

byEntailment :: forall c k a r. Entails k c => (c a => r) -> k a -> r Source #

flip withEntailment.

This is useful for "consuming" an index off the front of a function type and turning it into an instance, e.g. in the context of an imap10 call.