module Data.Type.Quantifier where
import Type.Family.Constraint
data Some (f :: k -> *) :: * where
Some :: f a -> Some f
some :: Some f -> (forall a. f a -> r) -> r
some (Some a) f = f a
(>>-) :: Some f -> (forall a. f a -> r) -> r
(>>-) = some
infixl 1 >>-
withSome :: (forall a. f a -> r) -> Some f -> r
withSome f (Some a) = f a
onSome :: (forall a. f a -> g x) -> Some f -> Some g
onSome f (Some a) = Some (f a)
data Some2 (f :: k -> l -> *) :: * where
Some2 :: f a b -> Some2 f
some2 :: Some2 f -> (forall a b. f a b -> r) -> r
some2 (Some2 a) f = f a
(>>--) :: Some2 f -> (forall a b. f a b -> r) -> r
(>>--) = some2
infixl 1 >>--
withSome2 :: (forall a b. f a b -> r) -> Some2 f -> r
withSome2 f (Some2 a) = f a
onSome2 :: (forall a b. f a b -> g x y) -> Some2 f -> Some2 g
onSome2 f (Some2 a) = Some2 (f a)
data Some3 (f :: k -> l -> m -> *) :: * where
Some3 :: f a b c -> Some3 f
some3 :: Some3 f -> (forall a b c. f a b c -> r) -> r
some3 (Some3 a) f = f a
(>>---) :: Some3 f -> (forall a b c. f a b c -> r) -> r
(>>---) = some3
infixl 1 >>---
withSome3 :: (forall a b c. f a b c -> r) -> Some3 f -> r
withSome3 f (Some3 a) = f a
onSome3 :: (forall a b c. f a b c -> g x y z) -> Some3 f -> Some3 g
onSome3 f (Some3 a) = Some3 (f a)
data SomeC (c :: k -> Constraint) (f :: k -> *) where
SomeC :: c a => f a -> SomeC c f
someC :: SomeC c f -> (forall a. c a => f a -> r) -> r
someC (SomeC a) f = f a
(>>~) :: SomeC c f -> (forall a. c a => f a -> r) -> r
(>>~) = someC
infixl 1 >>~
data Every (f :: k -> *) :: * where
Every :: { instEvery :: forall a. f a } -> Every f
data Every2 (f :: k -> l -> *) :: * where
Every2 :: { instEvery2 :: forall a b. f a b } -> Every2 f
data Every3 (f :: k -> l -> m -> *) :: * where
Every3 :: { instEvery3 :: forall a b c. f a b c } -> Every3 f