Data.HTree.Constraint

A couple of types to work with Constraints

proving a constraint

data Has c f k where

a functor useful for proving a constraint for some type

>>> import Data.Functor.Identity
>>> Proves @Eq (Identity (5 :: Int))
Proves (Identity 5)

Constructors

Proves :: c k => f k -> Has c f k

Instances

Typeable f => Show (Some (Has (Typeable :: l -> Constraint) f))

Defined in Data.HTree.Existential

Methods

showsPrec :: Int -> Some (Has Typeable f) -> ShowS

show :: Some (Has Typeable f) -> String

showList :: [Some (Has Typeable f)] -> ShowS

(forall x. Eq x => Eq (f x), Typeable f) => Eq (EList (Has (Both (Typeable :: Type -> Constraint) Eq) f))

Defined in Data.HTree.Existential

Methods

(==) :: EList (Has (Both Typeable Eq) f) -> EList (Has (Both Typeable Eq) f) -> Bool

(/=) :: EList (Has (Both Typeable Eq) f) -> EList (Has (Both Typeable Eq) f) -> Bool

Eq (f k2) => Eq (EList (HasIs k2 f))

Defined in Data.HTree.Existential

Methods

(==) :: EList (HasIs k2 f) -> EList (HasIs k2 f) -> Bool

(/=) :: EList (HasIs k2 f) -> EList (HasIs k2 f) -> Bool

(forall x. Eq x => Eq (f x), Typeable f) => Eq (ETree (Has (Both (Typeable :: Type -> Constraint) Eq) f))

Defined in Data.HTree.Existential

Methods

(==) :: ETree (Has (Both Typeable Eq) f) -> ETree (Has (Both Typeable Eq) f) -> Bool

(/=) :: ETree (Has (Both Typeable Eq) f) -> ETree (Has (Both Typeable Eq) f) -> Bool

(forall x. Eq x => Eq (f x), Typeable f) => Eq (Some (Has (Typeable :: Type -> Constraint) (Has Eq f)))

Defined in Data.HTree.Existential

Methods

(==) :: Some (Has Typeable (Has Eq f)) -> Some (Has Typeable (Has Eq f)) -> Bool

(/=) :: Some (Has Typeable (Has Eq f)) -> Some (Has Typeable (Has Eq f)) -> Bool

(forall x. Ord x => Ord (f x), Typeable f, Eq (Some (Has (Typeable :: Type -> Constraint) (Has Ord f)))) => Ord (Some (Has (Typeable :: Type -> Constraint) (Has Ord f)))

Defined in Data.HTree.Existential

Methods

compare :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Ordering

(<) :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Bool

(<=) :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Bool

(>) :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Bool

(>=) :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Bool

max :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f))

min :: Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f)) -> Some (Has Typeable (Has Ord f))

Show (f k2) => Show (Has c f k2)

Defined in Data.HTree.Constraint

Methods

showsPrec :: Int -> Has c f k2 -> ShowS

show :: Has c f k2 -> String

showList :: [Has c f k2] -> ShowS

synonyms for proving a constraint

type HasTypeable = Has Typeable

Has but specialised to Typeable

type HasIs k = Has ((~) k)

Has but specialised to a constant type, Some (HasIs k f) is isomorphic to f k

helpers to work with constraints

proves :: Has c f a -> (c a => f a -> r) -> r

destruct a Has

class c => Charge c a

transform a Constraint in something of kind k -> Constraint to be able to use it in Has

Instances

c => Charge c (a :: k)

Defined in Data.HTree.Constraint

Dict

type Dict c = Has (Charge c) Proxy ()

a Dict witnesses some constraint

pattern Dict :: forall (c :: Constraint). forall. c => Dict c

match on a Dict

functions for working with Dicts

withDict :: Dict c -> (c => r) -> r

destructing a Dict