Copyright | (C) 2017 Ryan Scott |
---|---|
License | BSD-style (see the file LICENSE) |
Maintainer | Ryan Scott |
Stability | Experimental |
Portability | GHC |
Safe Haskell | Trustworthy |
Language | Haskell2010 |
Dependently typed elimination functions using singletons
.
- elimBool :: forall (p :: Bool -> Type) (b :: Bool). Sing b -> p False -> p True -> p b
- elimEither :: forall (a :: Type) (b :: Type) (p :: Either a b -> Type) (e :: Either a b). Sing e -> (forall (l :: a). Sing l -> p (Left l)) -> (forall (r :: b). Sing r -> p (Right r)) -> p e
- elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]). Sing l -> p '[] -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x ': xs)) -> p l
- elimMaybe :: forall (a :: Type) (p :: Maybe a -> Type) (m :: Maybe a). Sing m -> p Nothing -> (forall (x :: a). Sing x -> p (Just x)) -> p m
- elimNat :: forall (p :: Nat -> Type) (n :: Nat). Sing n -> p 0 -> (forall (k :: Nat). Sing k -> p k -> p (k :+ 1)) -> p n
- elimNonEmpty :: forall (a :: Type) (p :: NonEmpty a -> Type) (n :: NonEmpty a). Sing n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p (x :| xs)) -> p n
- elimOrdering :: forall (p :: Ordering -> Type) (o :: Ordering). Sing o -> p LT -> p EQ -> p GT -> p o
- elimTuple0 :: forall (p :: () -> Type) (u :: ()). Sing u -> p () -> p u
- elimTuple2 :: forall (a :: Type) (b :: Type) (p :: (a, b) -> Type) (t :: (a, b)). Sing t -> (forall (aa :: a) (bb :: b). Sing aa -> Sing bb -> p '(aa, bb)) -> p t
- elimTuple3 :: forall (a :: Type) (b :: Type) (c :: Type) (p :: (a, b, c) -> Type) (t :: (a, b, c)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c). Sing aa -> Sing bb -> Sing cc -> p '(aa, bb, cc)) -> p t
- elimTuple4 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (p :: (a, b, c, d) -> Type) (t :: (a, b, c, d)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d). Sing aa -> Sing bb -> Sing cc -> Sing dd -> p '(aa, bb, cc, dd)) -> p t
- elimTuple5 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (p :: (a, b, c, d, e) -> Type) (t :: (a, b, c, d, e)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> p '(aa, bb, cc, dd, ee)) -> p t
- elimTuple6 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (p :: (a, b, c, d, e, f) -> Type) (t :: (a, b, c, d, e, f)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> p '(aa, bb, cc, dd, ee, ff)) -> p t
- elimTuple7 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type) (p :: (a, b, c, d, e, f, g) -> Type) (t :: (a, b, c, d, e, f, g)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f) (gg :: g). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> Sing gg -> p '(aa, bb, cc, dd, ee, ff, gg)) -> p t
- elimBoolTyFun :: forall (p :: Bool ~> Type) (b :: Bool). Sing b -> (p @@ False) -> (p @@ True) -> p @@ b
- elimEitherTyFun :: forall (a :: Type) (b :: Type) (p :: Either a b ~> Type) (e :: Either a b). Sing e -> (forall (l :: a). Sing l -> p @@ Left l) -> (forall (r :: b). Sing r -> p @@ Right r) -> p @@ e
- elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]). Sing l -> (p @@ '[]) -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> (p @@ xs) -> p @@ (x ': xs)) -> p @@ l
- elimMaybeTyFun :: forall (a :: Type) (p :: Maybe a ~> Type) (m :: Maybe a). Sing m -> (p @@ Nothing) -> (forall (x :: a). Sing x -> p @@ Just x) -> p @@ m
- elimNatTyFun :: forall (p :: Nat ~> Type) (n :: Nat). Sing n -> (p @@ 0) -> (forall (k :: Nat). Sing k -> (p @@ k) -> p @@ (k :+ 1)) -> p @@ n
- elimNonEmptyTyFun :: forall (a :: Type) (p :: NonEmpty a ~> Type) (n :: NonEmpty a). Sing n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ (x :| xs)) -> p @@ n
- elimOrderingTyFun :: forall (p :: Ordering ~> Type) (o :: Ordering). Sing o -> (p @@ LT) -> (p @@ EQ) -> (p @@ GT) -> p @@ o
- elimTuple0TyFun :: forall (p :: () ~> Type) (u :: ()). Sing u -> (p @@ ()) -> p @@ u
- elimTuple2TyFun :: forall (a :: Type) (b :: Type) (p :: (a, b) ~> Type) (t :: (a, b)). Sing t -> (forall (aa :: a) (bb :: b). Sing aa -> Sing bb -> p @@ '(aa, bb)) -> p @@ t
- elimTuple3TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (p :: (a, b, c) ~> Type) (t :: (a, b, c)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c). Sing aa -> Sing bb -> Sing cc -> p @@ '(aa, bb, cc)) -> p @@ t
- elimTuple4TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (p :: (a, b, c, d) ~> Type) (t :: (a, b, c, d)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d). Sing aa -> Sing bb -> Sing cc -> Sing dd -> p @@ '(aa, bb, cc, dd)) -> p @@ t
- elimTuple5TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (p :: (a, b, c, d, e) ~> Type) (t :: (a, b, c, d, e)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> p @@ '(aa, bb, cc, dd, ee)) -> p @@ t
- elimTuple6TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (p :: (a, b, c, d, e, f) ~> Type) (t :: (a, b, c, d, e, f)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> p @@ '(aa, bb, cc, dd, ee, ff)) -> p @@ t
- elimTuple7TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type) (p :: (a, b, c, d, e, f, g) ~> Type) (t :: (a, b, c, d, e, f, g)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f) (gg :: g). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> Sing gg -> p @@ '(aa, bb, cc, dd, ee, ff, gg)) -> p @@ t
- data FunArrow
- class FunType (arr :: FunArrow) where
- type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
- class FunType arr => AppType (arr :: FunArrow) where
- type FunApp arr = (FunType arr, AppType arr)
- elimBoolPoly :: forall (arr :: FunArrow) (p :: (Bool -?> Type) arr) (b :: Bool). FunApp arr => Sing b -> App Bool arr Type p False -> App Bool arr Type p True -> App Bool arr Type p b
- elimEitherPoly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (p :: (Either a b -?> Type) arr) (e :: Either a b). FunApp arr => Sing e -> (forall (l :: a). Sing l -> App (Either a b) arr Type p (Left l)) -> (forall (r :: b). Sing r -> App (Either a b) arr Type p (Right r)) -> App (Either a b) arr Type p e
- elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]). FunApp arr => Sing l -> App [a] arr Type p '[] -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x ': xs)) -> App [a] arr Type p l
- elimMaybePoly :: forall (arr :: FunArrow) (a :: Type) (p :: (Maybe a -?> Type) arr) (m :: Maybe a). FunApp arr => Sing m -> App (Maybe a) arr Type p Nothing -> (forall (x :: a). Sing x -> App (Maybe a) arr Type p (Just x)) -> App (Maybe a) arr Type p m
- elimNonEmptyPoly :: forall (arr :: FunArrow) (a :: Type) (p :: (NonEmpty a -?> Type) arr) (n :: NonEmpty a). FunApp arr => Sing n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App (NonEmpty a) arr Type p (x :| xs)) -> App (NonEmpty a) arr Type p n
- elimNatPoly :: forall (arr :: FunArrow) (p :: (Nat -?> Type) arr) (n :: Nat). FunApp arr => Sing n -> App Nat arr Type p 0 -> (forall (k :: Nat). Sing k -> App Nat arr Type p k -> App Nat arr Type p (k :+ 1)) -> App Nat arr Type p n
- elimOrderingPoly :: forall (arr :: FunArrow) (p :: (Ordering -?> Type) arr) (o :: Ordering). Sing o -> App Ordering arr Type p LT -> App Ordering arr Type p EQ -> App Ordering arr Type p GT -> App Ordering arr Type p o
- elimTuple0Poly :: forall (arr :: FunArrow) (p :: (() -?> Type) arr) (u :: ()). FunApp arr => Sing u -> App () arr Type p () -> App () arr Type p u
- elimTuple2Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (p :: ((a, b) -?> Type) arr) (t :: (a, b)). FunApp arr => Sing t -> (forall (aa :: a) (bb :: b). Sing aa -> Sing bb -> App (a, b) arr Type p '(aa, bb)) -> App (a, b) arr Type p t
- elimTuple3Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (p :: ((a, b, c) -?> Type) arr) (t :: (a, b, c)). FunApp arr => Sing t -> (forall (aa :: a) (bb :: b) (cc :: c). Sing aa -> Sing bb -> Sing cc -> App (a, b, c) arr Type p '(aa, bb, cc)) -> App (a, b, c) arr Type p t
- elimTuple4Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (d :: Type) (p :: ((a, b, c, d) -?> Type) arr) (t :: (a, b, c, d)). FunApp arr => Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d). Sing aa -> Sing bb -> Sing cc -> Sing dd -> App (a, b, c, d) arr Type p '(aa, bb, cc, dd)) -> App (a, b, c, d) arr Type p t
- elimTuple5Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (p :: ((a, b, c, d, e) -?> Type) arr) (t :: (a, b, c, d, e)). FunApp arr => Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> App (a, b, c, d, e) arr Type p '(aa, bb, cc, dd, ee)) -> App (a, b, c, d, e) arr Type p t
- elimTuple6Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (p :: ((a, b, c, d, e, f) -?> Type) arr) (t :: (a, b, c, d, e, f)). FunApp arr => Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> App (a, b, c, d, e, f) arr Type p '(aa, bb, cc, dd, ee, ff)) -> App (a, b, c, d, e, f) arr Type p t
- elimTuple7Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type) (p :: ((a, b, c, d, e, f, g) -?> Type) arr) (t :: (a, b, c, d, e, f, g)). FunApp arr => Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f) (gg :: g). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> Sing gg -> App (a, b, c, d, e, f, g) arr Type p '(aa, bb, cc, dd, ee, ff, gg)) -> App (a, b, c, d, e, f, g) arr Type p t
Eliminator functions
Eliminators using '(->)'
These eliminators are defined with propositions of kind <Datatype> ->
(that is, using the '(->)' kind). As a result, these eliminators' type signatures
are the most readable in this library, and most closely resemble eliminator functions
in other dependently typed languages.Type
elimEither :: forall (a :: Type) (b :: Type) (p :: Either a b -> Type) (e :: Either a b). Sing e -> (forall (l :: a). Sing l -> p (Left l)) -> (forall (r :: b). Sing r -> p (Right r)) -> p e Source #
elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]). Sing l -> p '[] -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x ': xs)) -> p l Source #
elimMaybe :: forall (a :: Type) (p :: Maybe a -> Type) (m :: Maybe a). Sing m -> p Nothing -> (forall (x :: a). Sing x -> p (Just x)) -> p m Source #
elimNat :: forall (p :: Nat -> Type) (n :: Nat). Sing n -> p 0 -> (forall (k :: Nat). Sing k -> p k -> p (k :+ 1)) -> p n Source #
elimNonEmpty :: forall (a :: Type) (p :: NonEmpty a -> Type) (n :: NonEmpty a). Sing n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p (x :| xs)) -> p n Source #
elimOrdering :: forall (p :: Ordering -> Type) (o :: Ordering). Sing o -> p LT -> p EQ -> p GT -> p o Source #
elimTuple0 :: forall (p :: () -> Type) (u :: ()). Sing u -> p () -> p u Source #
elimTuple2 :: forall (a :: Type) (b :: Type) (p :: (a, b) -> Type) (t :: (a, b)). Sing t -> (forall (aa :: a) (bb :: b). Sing aa -> Sing bb -> p '(aa, bb)) -> p t Source #
elimTuple3 :: forall (a :: Type) (b :: Type) (c :: Type) (p :: (a, b, c) -> Type) (t :: (a, b, c)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c). Sing aa -> Sing bb -> Sing cc -> p '(aa, bb, cc)) -> p t Source #
elimTuple4 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (p :: (a, b, c, d) -> Type) (t :: (a, b, c, d)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d). Sing aa -> Sing bb -> Sing cc -> Sing dd -> p '(aa, bb, cc, dd)) -> p t Source #
elimTuple5 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (p :: (a, b, c, d, e) -> Type) (t :: (a, b, c, d, e)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> p '(aa, bb, cc, dd, ee)) -> p t Source #
elimTuple6 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (p :: (a, b, c, d, e, f) -> Type) (t :: (a, b, c, d, e, f)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> p '(aa, bb, cc, dd, ee, ff)) -> p t Source #
elimTuple7 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type) (p :: (a, b, c, d, e, f, g) -> Type) (t :: (a, b, c, d, e, f, g)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f) (gg :: g). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> Sing gg -> p '(aa, bb, cc, dd, ee, ff, gg)) -> p t Source #
Eliminators using '(~>)'
These eliminators are defined with propositions of kind <Datatype> ~>
(that is, using the '(~>)' kind). These eliminators are designed for
defunctionalized (i.e., "partially applied") type families as predicates,
and as a result, the predicates must be applied manually with '(@@)'.Type
elimBoolTyFun :: forall (p :: Bool ~> Type) (b :: Bool). Sing b -> (p @@ False) -> (p @@ True) -> p @@ b Source #
elimEitherTyFun :: forall (a :: Type) (b :: Type) (p :: Either a b ~> Type) (e :: Either a b). Sing e -> (forall (l :: a). Sing l -> p @@ Left l) -> (forall (r :: b). Sing r -> p @@ Right r) -> p @@ e Source #
elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]). Sing l -> (p @@ '[]) -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> (p @@ xs) -> p @@ (x ': xs)) -> p @@ l Source #
elimMaybeTyFun :: forall (a :: Type) (p :: Maybe a ~> Type) (m :: Maybe a). Sing m -> (p @@ Nothing) -> (forall (x :: a). Sing x -> p @@ Just x) -> p @@ m Source #
elimNatTyFun :: forall (p :: Nat ~> Type) (n :: Nat). Sing n -> (p @@ 0) -> (forall (k :: Nat). Sing k -> (p @@ k) -> p @@ (k :+ 1)) -> p @@ n Source #
elimNonEmptyTyFun :: forall (a :: Type) (p :: NonEmpty a ~> Type) (n :: NonEmpty a). Sing n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ (x :| xs)) -> p @@ n Source #
elimOrderingTyFun :: forall (p :: Ordering ~> Type) (o :: Ordering). Sing o -> (p @@ LT) -> (p @@ EQ) -> (p @@ GT) -> p @@ o Source #
elimTuple0TyFun :: forall (p :: () ~> Type) (u :: ()). Sing u -> (p @@ ()) -> p @@ u Source #
elimTuple2TyFun :: forall (a :: Type) (b :: Type) (p :: (a, b) ~> Type) (t :: (a, b)). Sing t -> (forall (aa :: a) (bb :: b). Sing aa -> Sing bb -> p @@ '(aa, bb)) -> p @@ t Source #
elimTuple3TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (p :: (a, b, c) ~> Type) (t :: (a, b, c)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c). Sing aa -> Sing bb -> Sing cc -> p @@ '(aa, bb, cc)) -> p @@ t Source #
elimTuple4TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (p :: (a, b, c, d) ~> Type) (t :: (a, b, c, d)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d). Sing aa -> Sing bb -> Sing cc -> Sing dd -> p @@ '(aa, bb, cc, dd)) -> p @@ t Source #
elimTuple5TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (p :: (a, b, c, d, e) ~> Type) (t :: (a, b, c, d, e)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> p @@ '(aa, bb, cc, dd, ee)) -> p @@ t Source #
elimTuple6TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (p :: (a, b, c, d, e, f) ~> Type) (t :: (a, b, c, d, e, f)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> p @@ '(aa, bb, cc, dd, ee, ff)) -> p @@ t Source #
elimTuple7TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type) (p :: (a, b, c, d, e, f, g) ~> Type) (t :: (a, b, c, d, e, f, g)). Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f) (gg :: g). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> Sing gg -> p @@ '(aa, bb, cc, dd, ee, ff, gg)) -> p @@ t Source #
Arrow-polymorphic eliminators (very experimental)
Eliminators using '(->)' and eliminators using '(~>)' end up having very similar
implementations - so similar, in fact, that they can be generalized to be polymorphic
over the arrow kind used (as well as the application operator). The FunType
and
AppType
classes capture these notions of abstraction and application, respectively.
Not all eliminators are known to work under this generalized scheme yet (for instance, eliminators for GADTs).
Chances are, you won't want to use these eliminators directly, since their type signatures are pretty horrific and don't always play well with type inference. However, they are provided for the sake of completeness.
An enumeration which represents the possible choices of arrow kind for eliminator functions.
type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2 infixr 0 Source #
An infix synonym for Fun
.
class FunType arr => AppType (arr :: FunArrow) Source #
Things which can be applied.
elimBoolPoly :: forall (arr :: FunArrow) (p :: (Bool -?> Type) arr) (b :: Bool). FunApp arr => Sing b -> App Bool arr Type p False -> App Bool arr Type p True -> App Bool arr Type p b Source #
elimEitherPoly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (p :: (Either a b -?> Type) arr) (e :: Either a b). FunApp arr => Sing e -> (forall (l :: a). Sing l -> App (Either a b) arr Type p (Left l)) -> (forall (r :: b). Sing r -> App (Either a b) arr Type p (Right r)) -> App (Either a b) arr Type p e Source #
elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]). FunApp arr => Sing l -> App [a] arr Type p '[] -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x ': xs)) -> App [a] arr Type p l Source #
elimMaybePoly :: forall (arr :: FunArrow) (a :: Type) (p :: (Maybe a -?> Type) arr) (m :: Maybe a). FunApp arr => Sing m -> App (Maybe a) arr Type p Nothing -> (forall (x :: a). Sing x -> App (Maybe a) arr Type p (Just x)) -> App (Maybe a) arr Type p m Source #
elimNonEmptyPoly :: forall (arr :: FunArrow) (a :: Type) (p :: (NonEmpty a -?> Type) arr) (n :: NonEmpty a). FunApp arr => Sing n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App (NonEmpty a) arr Type p (x :| xs)) -> App (NonEmpty a) arr Type p n Source #
elimNatPoly :: forall (arr :: FunArrow) (p :: (Nat -?> Type) arr) (n :: Nat). FunApp arr => Sing n -> App Nat arr Type p 0 -> (forall (k :: Nat). Sing k -> App Nat arr Type p k -> App Nat arr Type p (k :+ 1)) -> App Nat arr Type p n Source #
elimOrderingPoly :: forall (arr :: FunArrow) (p :: (Ordering -?> Type) arr) (o :: Ordering). Sing o -> App Ordering arr Type p LT -> App Ordering arr Type p EQ -> App Ordering arr Type p GT -> App Ordering arr Type p o Source #
elimTuple0Poly :: forall (arr :: FunArrow) (p :: (() -?> Type) arr) (u :: ()). FunApp arr => Sing u -> App () arr Type p () -> App () arr Type p u Source #
elimTuple2Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (p :: ((a, b) -?> Type) arr) (t :: (a, b)). FunApp arr => Sing t -> (forall (aa :: a) (bb :: b). Sing aa -> Sing bb -> App (a, b) arr Type p '(aa, bb)) -> App (a, b) arr Type p t Source #
elimTuple3Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (p :: ((a, b, c) -?> Type) arr) (t :: (a, b, c)). FunApp arr => Sing t -> (forall (aa :: a) (bb :: b) (cc :: c). Sing aa -> Sing bb -> Sing cc -> App (a, b, c) arr Type p '(aa, bb, cc)) -> App (a, b, c) arr Type p t Source #
elimTuple4Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (d :: Type) (p :: ((a, b, c, d) -?> Type) arr) (t :: (a, b, c, d)). FunApp arr => Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d). Sing aa -> Sing bb -> Sing cc -> Sing dd -> App (a, b, c, d) arr Type p '(aa, bb, cc, dd)) -> App (a, b, c, d) arr Type p t Source #
elimTuple5Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (p :: ((a, b, c, d, e) -?> Type) arr) (t :: (a, b, c, d, e)). FunApp arr => Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> App (a, b, c, d, e) arr Type p '(aa, bb, cc, dd, ee)) -> App (a, b, c, d, e) arr Type p t Source #
elimTuple6Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (p :: ((a, b, c, d, e, f) -?> Type) arr) (t :: (a, b, c, d, e, f)). FunApp arr => Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> App (a, b, c, d, e, f) arr Type p '(aa, bb, cc, dd, ee, ff)) -> App (a, b, c, d, e, f) arr Type p t Source #
elimTuple7Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type) (p :: ((a, b, c, d, e, f, g) -?> Type) arr) (t :: (a, b, c, d, e, f, g)). FunApp arr => Sing t -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f) (gg :: g). Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> Sing gg -> App (a, b, c, d, e, f, g) arr Type p '(aa, bb, cc, dd, ee, ff, gg)) -> App (a, b, c, d, e, f, g) arr Type p t Source #