Copyright | (c) Justin Le 2018 |
---|---|

License | BSD3 |

Maintainer | justin@jle.im |

Stability | experimental |

Portability | non-portable |

Safe Haskell | None |

Language | Haskell2010 |

Combinators for working with type-level predicates, along with typeclasses for canonical proofs and deciding functions.

## Synopsis

- type family Elem (f :: Type -> Type) :: f k -> k -> Type
- type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as
- class Universe (f :: Type -> Type) where
- data Index :: [k] -> k -> Type where
- data IsJust :: Maybe k -> k -> Type where
- data IsRight :: Either j k -> k -> Type where
- data NEIndex :: NonEmpty k -> k -> Type where
- data Snd :: (j, k) -> k -> Type where
- data All f :: (k ~> Type) -> f k ~> Type
- newtype WitAll f p (as :: f k) = WitAll {}
- data Any f :: (k ~> Type) -> f k ~> Type
- data WitAny f :: (k ~> Type) -> f k -> Type where
- type None f p = (Not (Any f p) :: Predicate (f k))
- type Null f = (None f Evident :: Predicate (f k))
- type NotNull f = (Any f Evident :: Predicate (f k))
- decideAny :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (Any f p)
- decideAll :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (All f p)
- genAllA :: forall f k (p :: k ~> Type) (as :: f k) h. (Universe f, Applicative h) => (forall a. Sing a -> h (p @@ a)) -> Sing as -> h (All f p @@ as)
- genAll :: forall f k (p :: k ~> Type). Universe f => Prove p -> Prove (All f p)
- igenAll :: forall f k (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> p @@ a) -> Sing as -> All f p @@ as
- foldMapUni :: forall f k (as :: f k) m. (Universe f, Monoid m) => (forall (a :: k). Sing a -> m) -> Sing as -> m
- ifoldMapUni :: forall f k (as :: f k) m. (Universe f, Monoid m) => (forall a. Elem f as a -> Sing a -> m) -> Sing as -> m
- index :: forall f as a. Universe f => Elem f as a -> Sing as -> Sing a
- pickElem :: forall f k (as :: f k) a. (Universe f, SingI as, SingI a, SDecide k) => Decision (Elem f as a)
- data ElemSym0 (f :: Type -> Type) :: f k ~> (k ~> Type)
- data ElemSym1 (f :: Type -> Type) :: f k -> k ~> Type
- type ElemSym2 (f :: Type -> Type) (as :: f k) (a :: k) = Elem f as a

# Universe

type family Elem (f :: Type -> Type) :: f k -> k -> Type Source #

A witness for membership of a given item in a type-level collection

type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as Source #

is a predicate that a given input `In`

f as`a`

is a member of
collection `as`

.

class Universe (f :: Type -> Type) where Source #

Typeclass for a type-level container that you can quantify or lift type-level predicates over.

:: forall (p :: k ~> Type) (as :: f k). (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) | predicate on value |

-> Sing as -> Decision (Any f p @@ as) | predicate on collection |

:: forall (p :: k ~> Type) (as :: f k). (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) | predicate on value |

-> Sing as -> Decision (All f p @@ as) | predicate on collection |

## Instances

Universe [] Source # | |

Defined in Data.Type.Universe idecideAny :: (forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any [] p @@ as) Source # idecideAll :: (forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All [] p @@ as) Source # igenAllA :: Applicative h => (forall (a :: k). Elem [] as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All [] p @@ as) Source # | |

Universe Maybe Source # | |

Defined in Data.Type.Universe idecideAny :: (forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any Maybe p @@ as) Source # idecideAll :: (forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All Maybe p @@ as) Source # igenAllA :: Applicative h => (forall (a :: k). Elem Maybe as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All Maybe p @@ as) Source # | |

Universe NonEmpty Source # | |

Defined in Data.Type.Universe idecideAny :: (forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any NonEmpty p @@ as) Source # idecideAll :: (forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All NonEmpty p @@ as) Source # igenAllA :: Applicative h => (forall (a :: k). Elem NonEmpty as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All NonEmpty p @@ as) Source # | |

Universe (Either j) Source # | |

Defined in Data.Type.Universe idecideAny :: (forall (a :: k). Elem (Either j) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any (Either j) p @@ as) Source # idecideAll :: (forall (a :: k). Elem (Either j) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All (Either j) p @@ as) Source # igenAllA :: Applicative h => (forall (a :: k). Elem (Either j) as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All (Either j) p @@ as) Source # | |

Universe ((,) j) Source # | |

Defined in Data.Type.Universe idecideAny :: (forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any ((,) j) p @@ as) Source # idecideAll :: (forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All ((,) j) p @@ as) Source # igenAllA :: Applicative h => (forall (a :: k). Elem ((,) j) as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All ((,) j) p @@ as) Source # |

## Instances

data Index :: [k] -> k -> Type where Source #

Witness an item in a type-level list by providing its index.

data NEIndex :: NonEmpty k -> k -> Type where Source #

Witness an item in a type-level `NonEmpty`

by either indicating that
it is the "head", or by providing an index in the "tail".

data Snd :: (j, k) -> k -> Type where Source #

Trivially witness an item in the second field of a type-level tuple.

## Predicates

data All f :: (k ~> Type) -> f k ~> Type Source #

An

is a predicate testing a collection `All`

f p`as :: f a`

for the
fact that *all* items in `as`

satisfy `p`

. Represents the "forall"
quantifier over a given universe.

This is mostly useful for its `Decidable`

, `Provable`

, and `TFunctor`

instances, which lets you lift predicates on `p`

to predicates on

.`All`

f p

## Instances

Universe f => TFunctor (All f :: (k1 ~> Type) -> TyFun (f k1) Type -> *) Source # | |

Universe f => DFunctor (All f :: (k1 ~> Type) -> TyFun (f k1) Type -> *) Source # | |

(Universe f, Provable p) => Provable (All f p :: TyFun (f k) Type -> *) Source # | |

(Universe f, Decidable p) => Decidable (All f p :: TyFun (f k) Type -> *) Source # | |

type Apply (All f p :: TyFun (f k) Type -> *) (as :: f k) Source # | |

newtype WitAll f p (as :: f k) Source #

A

is a witness that the predicate `WitAll`

p as`p a`

is true for all
items `a`

in the type-level collection `as`

.

data Any f :: (k ~> Type) -> f k ~> Type Source #

An

is a predicate testing a collection `Any`

f p`as :: f a`

for the
fact that at least one item in `as`

satisfies `p`

. Represents the
"exists" quantifier over a given universe.

This is mostly useful for its `Decidable`

and `TFunctor`

instances,
which lets you lift predicates on `p`

to predicates on

.`Any`

f p

## Instances

Universe f => TFunctor (Any f :: (k1 ~> Type) -> TyFun (f k1) Type -> *) Source # | |

Provable p => Provable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> *) Source # | |

Provable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *) Source # | |

Provable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *) Source # | |

(Universe f, Provable p) => Decidable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> *) Source # | |

(Universe f, Decidable p) => Decidable (Any f p :: TyFun (f k) Type -> *) Source # | |

Decidable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *) Source # | |

Decidable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *) Source # | |

type Apply (Any f p :: TyFun (f k) Type -> *) (as :: f k) Source # | |

data WitAny f :: (k ~> Type) -> f k -> Type where Source #

A

is a witness that, for at least one item `WitAny`

p as`a`

in the
type-level collection `as`

, the predicate `p a`

is true.

type None f p = (Not (Any f p) :: Predicate (f k)) Source #

A

is a predicate on a collection `None`

f p`as`

that no `a`

in `as`

satisfies predicate `p`

.

type Null f = (None f Evident :: Predicate (f k)) Source #

Predicate that a given `as :: f k`

is empty and has no items in it.

type NotNull f = (Any f Evident :: Predicate (f k)) Source #

Predicate that a given `as :: f k`

is not empty, and has at least one
item in it.

# Decisions and manipulations

:: forall (p :: k ~> Type). Universe f | |

=> Decide p | predicate on value |

-> Decide (Any f p) | predicate on collection |

Lifts a predicate `p`

on an individual `a`

into a predicate that on
a collection `as`

that is true if and only if *any* item in `as`

satisfies the original predicate.

That is, it turns a predicate of kind `k ~> Type`

into a predicate
of kind `f k ~> Type`

.

Essentially tests existential quantification.

:: forall (p :: k ~> Type). Universe f | |

=> Decide p | predicate on value |

-> Decide (All f p) | predicate on collection |

Lifts a predicate `p`

on an individual `a`

into a predicate that on
a collection `as`

that is true if and only if *all* items in `as`

satisfies the original predicate.

That is, it turns a predicate of kind `k ~> Type`

into a predicate
of kind `f k ~> Type`

.

Essentially tests universal quantification.

:: forall (p :: k ~> Type) (as :: f k). (Universe f, Applicative h) | |

=> (forall a. Sing a -> h (p @@ a)) | predicate on value in context |

-> Sing as -> h (All f p @@ as) | predicate on collection in context |

If `p a`

is true for all values `a`

in `as`

under some
(Applicative) context `h`

, then you can create an

under
that Applicative context `All`

p as`h`

.

Can be useful with `Identity`

(which is basically unwrapping and
wrapping `All`

), or with `Maybe`

(which can express predicates that
are either provably true or not provably false).

In practice, this can be used to iterate and traverse and sequence
actions over all "items" in `as`

.

foldMapUni :: forall f k (as :: f k) m. (Universe f, Monoid m) => (forall (a :: k). Sing a -> m) -> Sing as -> m Source #

A `foldMap`

over all items in a collection.

ifoldMapUni :: forall f k (as :: f k) m. (Universe f, Monoid m) => (forall a. Elem f as a -> Sing a -> m) -> Sing as -> m Source #

`foldMapUni`

but with access to the index.

Extract the item from the container witnessed by the `Elem`

pickElem :: forall f k (as :: f k) a. (Universe f, SingI as, SingI a, SDecide k) => Decision (Elem f as a) Source #

Automatically generate a witness for a member, if possible

# Defunctionalization symbols

data ElemSym1 (f :: Type -> Type) :: f k -> k ~> Type Source #

## Instances

AutoElem f as a => Auto (In f as :: TyFun k Type -> *) (a :: k) Source # | |

Provable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *) Source # | |

Provable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *) Source # | |

Decidable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *) Source # | |

Decidable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *) Source # | |

Universe f => Decidable (Found (InP f :: ParamPred (f v) v) :: TyFun (f v) Type -> *) Source # | |

type Apply (ElemSym1 f as :: TyFun k Type -> *) (a :: k) Source # | |