Copyright | (C) 2011-2015 Edward Kmett (C) 2015 Ørjan Johansen (C) 2016 David Feuer |
---|---|
License | BSD-style (see the file LICENSE) |
Maintainer | Edward Kmett <ekmett@gmail.com> |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Trustworthy |
Language | Haskell2010 |
This module uses a trick to provide quantification over constraints.
- type family Forall (p :: k -> Constraint) :: Constraint
- inst :: forall p a. Forall p :- p a
- class Forall (ComposeC p f) => ForallF (p :: k2 -> Constraint) (f :: k1 -> k2)
- instF :: forall p f a. ForallF p f :- p (f a)
- type Forall1 p = Forall p
- inst1 :: forall (p :: (* -> *) -> Constraint) (f :: * -> *). Forall p :- p f
- class Forall (Q p t) => ForallT (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4)
- instT :: forall (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4) (f :: k1 -> k2) (a :: k3). ForallT p t :- p (t f a)
- type family ForallV :: k -> Constraint
- class InstV (p :: k) c | k c -> p where
- forall :: forall p. (forall a. Dict (p a)) -> Dict (Forall p)
Documentation
type family Forall (p :: k -> Constraint) :: Constraint Source #
A representation of the quantified constraint forall a. p a
.
class Forall (ComposeC p f) => ForallF (p :: k2 -> Constraint) (f :: k1 -> k2) Source #
A representation of the quantified constraint forall a. p (f a)
.
instF :: forall p f a. ForallF p f :- p (f a) Source #
Instantiate a quantified
constraint at type ForallF
p fa
.
inst1 :: forall (p :: (* -> *) -> Constraint) (f :: * -> *). Forall p :- p f Source #
Instantiate a quantified constraint on kind * -> *
.
This is now redundant since
became polykinded.inst
class Forall (Q p t) => ForallT (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4) Source #
A representation of the quantified constraint forall f a. p (t f a)
.
instT :: forall (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4) (f :: k1 -> k2) (a :: k3). ForallT p t :- p (t f a) Source #
Instantiate a quantified
constraint at types ForallT
p tf
and a
.
type family ForallV :: k -> Constraint Source #
A representation of the quantified constraint
forall a1 a2 ... an . p a1 a2 ... an
, supporting a variable number of
parameters.
class InstV (p :: k) c | k c -> p where Source #
Instantiate a quantified
constraint as ForallV
pc
, where
c ~ p a1 a2 ... an
.
(~) Constraint p c => InstV Constraint p c Source # | |
InstV (k2 -> k3) (p a) c => InstV (k1 -> k2 -> k3) p c Source # | |
(~) Constraint (p a) c => InstV (k -> Constraint) p c Source # | |