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
.
Synopsis
- elimAll :: forall (p :: (~>) All Type) (s :: All). Sing s -> (forall (f0 :: Bool). Sing f0 -> Apply p ('All f0)) -> Apply p s
- type family ElimAll p s p where ...
- elimAny :: forall (p :: (~>) Any Type) (s :: Any). Sing s -> (forall (f0 :: Bool). Sing f0 -> Apply p ('Any f0)) -> Apply p s
- type family ElimAny p s p where ...
- elimArg :: forall (a :: Type) (b :: Type) (p :: (~>) (Arg a b) Type) (s :: Arg a b). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> Apply p ('Arg f0 f1)) -> Apply p s
- type family ElimArg p s p where ...
- elimBool :: forall (p :: (~>) Bool Type) (s :: Bool). Sing s -> Apply p 'False -> Apply p 'True -> Apply p s
- type family ElimBool p s p p where ...
- elimConst :: forall (a :: Type) (k :: Type) (b :: k) (p :: (~>) (Const a b) Type) (s :: Const a b). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Const f0)) -> Apply p s
- type family ElimConst p s p where ...
- elimDown :: forall (a :: Type) (p :: (~>) (Down a) Type) (s :: Down a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Down f0)) -> Apply p s
- type family ElimDown p s p where ...
- elimDual :: forall (a :: Type) (p :: (~>) (Dual a) Type) (s :: Dual a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Dual f0)) -> Apply p s
- type family ElimDual p s p where ...
- elimEither :: forall (a :: Type) (b :: Type) (p :: (~>) (Either a b) Type) (s :: Either a b). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Left f0)) -> (forall (f0 :: b). Sing f0 -> Apply p ('Right f0)) -> Apply p s
- type family ElimEither p s p p where ...
- elimFirst :: forall (a :: Type) (p :: (~>) (First a) Type) (s :: First a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('First f0)) -> Apply p s
- type family ElimFirst p s p where ...
- elimIdentity :: forall (a :: Type) (p :: (~>) (Identity a) Type) (s :: Identity a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Identity f0)) -> Apply p s
- type family ElimIdentity p s p where ...
- elimLast :: forall (a :: Type) (p :: (~>) (Last a) Type) (s :: Last a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Last f0)) -> Apply p s
- type family ElimLast p s p where ...
- elimList :: forall (a :: Type) (p :: (~>) ([] a) Type) (s :: [] a). Sing s -> Apply p '[] -> (forall (f0 :: a). Sing f0 -> forall (f1 :: [a]). Sing f1 -> Apply p f1 -> Apply p ('(:) f0 f1)) -> Apply p s
- type family ElimList p s p p where ...
- elimMax :: forall (a :: Type) (p :: (~>) (Max a) Type) (s :: Max a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Max f0)) -> Apply p s
- type family ElimMax p s p where ...
- elimMaybe :: forall (a :: Type) (p :: (~>) (Maybe a) Type) (s :: Maybe a). Sing s -> Apply p 'Nothing -> (forall (f0 :: a). Sing f0 -> Apply p ('Just f0)) -> Apply p s
- type family ElimMaybe p s p p where ...
- elimMin :: forall (a :: Type) (p :: (~>) (Min a) Type) (s :: Min a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Min f0)) -> Apply p s
- type family ElimMin p s p where ...
- elimNat :: forall (p :: (~>) Nat Type) (s :: Nat). Sing s -> Apply p 'Z -> (forall (f0 :: Nat). Sing f0 -> Apply p f0 -> Apply p ('S f0)) -> Apply p s
- type family ElimNat p s p p where ...
- elimNonEmpty :: forall (a :: Type) (p :: (~>) (NonEmpty a) Type) (s :: NonEmpty a). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: [a]). Sing f1 -> Apply p ('(:|) f0 f1)) -> Apply p s
- type family ElimNonEmpty p s p where ...
- elimOrdering :: forall (p :: (~>) Ordering Type) (s :: Ordering). Sing s -> Apply p 'LT -> Apply p 'EQ -> Apply p 'GT -> Apply p s
- type family ElimOrdering p s p p p where ...
- elimProduct :: forall (a :: Type) (p :: (~>) (Product a) Type) (s :: Product a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Product f0)) -> Apply p s
- type family ElimProduct p s p where ...
- elimSum :: forall (a :: Type) (p :: (~>) (Sum a) Type) (s :: Sum a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Sum f0)) -> Apply p s
- type family ElimSum p s p where ...
- elimTuple0 :: forall (p :: (~>) () Type) (s :: ()). Sing s -> Apply p '() -> Apply p s
- type family ElimTuple0 p s p where ...
- elimTuple2 :: forall (a :: Type) (b :: Type) (p :: (~>) ((,) a b) Type) (s :: (,) a b). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> Apply p ('(,) f0 f1)) -> Apply p s
- type family ElimTuple2 p s p where ...
- elimTuple3 :: forall (a :: Type) (b :: Type) (c :: Type) (p :: (~>) ((,,) a b c) Type) (s :: (,,) a b c). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> Apply p ('(,,) f0 f1 f2)) -> Apply p s
- type family ElimTuple3 p s p where ...
- elimTuple4 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (p :: (~>) ((,,,) a b c d) Type) (s :: (,,,) a b c d). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> forall (f3 :: d). Sing f3 -> Apply p ('(,,,) f0 f1 f2 f3)) -> Apply p s
- type family ElimTuple4 p s p where ...
- elimTuple5 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (p :: (~>) ((,,,,) a b c d e) Type) (s :: (,,,,) a b c d e). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> forall (f3 :: d). Sing f3 -> forall (f4 :: e). Sing f4 -> Apply p ('(,,,,) f0 f1 f2 f3 f4)) -> Apply p s
- type family ElimTuple5 p s p where ...
- elimTuple6 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (p :: (~>) ((,,,,,) a b c d e f) Type) (s :: (,,,,,) a b c d e f). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> forall (f3 :: d). Sing f3 -> forall (f4 :: e). Sing f4 -> forall (f5 :: f). Sing f5 -> Apply p ('(,,,,,) f0 f1 f2 f3 f4 f5)) -> Apply p s
- type family ElimTuple6 p s p where ...
- 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) (s :: (,,,,,,) a b c d e f g). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> forall (f3 :: d). Sing f3 -> forall (f4 :: e). Sing f4 -> forall (f5 :: f). Sing f5 -> forall (f6 :: g). Sing f6 -> Apply p ('(,,,,,,) f0 f1 f2 f3 f4 f5 f6)) -> Apply p s
- type family ElimTuple7 p s p where ...
- elimVoid :: forall (p :: (~>) Void Type) (s :: Void). Sing s -> Apply p s
- type family ElimVoid p s where ...
- elimWrappedMonoid :: forall (m :: Type) (p :: (~>) (WrappedMonoid m) Type) (s :: WrappedMonoid m). Sing s -> (forall (f0 :: m). Sing f0 -> Apply p ('WrapMonoid f0)) -> Apply p s
- type family ElimWrappedMonoid p s p where ...
Eliminator functions
These eliminators are defined with propositions of kind <Datatype> ~>
(that is, using the Type
(
kind). These eliminators are designed for
defunctionalized (i.e., "partially applied") types as predicates,
and as a result, the predicates must be applied manually with ~>
)Apply
.
The naming conventions are:
- If the datatype has an alphanumeric name, its eliminator will have that name
with
elim
prepended. - If the datatype has a symbolic name, its eliminator will have that name
with
~>
prepended.
elimAll :: forall (p :: (~>) All Type) (s :: All). Sing s -> (forall (f0 :: Bool). Sing f0 -> Apply p ('All f0)) -> Apply p s Source #
elimAny :: forall (p :: (~>) Any Type) (s :: Any). Sing s -> (forall (f0 :: Bool). Sing f0 -> Apply p ('Any f0)) -> Apply p s Source #
elimArg :: forall (a :: Type) (b :: Type) (p :: (~>) (Arg a b) Type) (s :: Arg a b). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> Apply p ('Arg f0 f1)) -> Apply p s Source #
elimBool :: forall (p :: (~>) Bool Type) (s :: Bool). Sing s -> Apply p 'False -> Apply p 'True -> Apply p s Source #
elimConst :: forall (a :: Type) (k :: Type) (b :: k) (p :: (~>) (Const a b) Type) (s :: Const a b). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Const f0)) -> Apply p s Source #
elimDown :: forall (a :: Type) (p :: (~>) (Down a) Type) (s :: Down a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Down f0)) -> Apply p s Source #
elimDual :: forall (a :: Type) (p :: (~>) (Dual a) Type) (s :: Dual a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Dual f0)) -> Apply p s Source #
elimEither :: forall (a :: Type) (b :: Type) (p :: (~>) (Either a b) Type) (s :: Either a b). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Left f0)) -> (forall (f0 :: b). Sing f0 -> Apply p ('Right f0)) -> Apply p s Source #
type family ElimEither p s p p where ... Source #
ElimEither @a @b p ('Left s0) useThis _p1 = useThis s0 | |
ElimEither @a @b p ('Right s0) _p0 useThis = useThis s0 |
elimFirst :: forall (a :: Type) (p :: (~>) (First a) Type) (s :: First a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('First f0)) -> Apply p s Source #
elimIdentity :: forall (a :: Type) (p :: (~>) (Identity a) Type) (s :: Identity a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Identity f0)) -> Apply p s Source #
type family ElimIdentity p s p where ... Source #
ElimIdentity @a p ('Identity s0) useThis = useThis s0 |
elimLast :: forall (a :: Type) (p :: (~>) (Last a) Type) (s :: Last a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Last f0)) -> Apply p s Source #
elimList :: forall (a :: Type) (p :: (~>) ([] a) Type) (s :: [] a). Sing s -> Apply p '[] -> (forall (f0 :: a). Sing f0 -> forall (f1 :: [a]). Sing f1 -> Apply p f1 -> Apply p ('(:) f0 f1)) -> Apply p s Source #
elimMax :: forall (a :: Type) (p :: (~>) (Max a) Type) (s :: Max a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Max f0)) -> Apply p s Source #
elimMaybe :: forall (a :: Type) (p :: (~>) (Maybe a) Type) (s :: Maybe a). Sing s -> Apply p 'Nothing -> (forall (f0 :: a). Sing f0 -> Apply p ('Just f0)) -> Apply p s Source #
elimMin :: forall (a :: Type) (p :: (~>) (Min a) Type) (s :: Min a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Min f0)) -> Apply p s Source #
elimNat :: forall (p :: (~>) Nat Type) (s :: Nat). Sing s -> Apply p 'Z -> (forall (f0 :: Nat). Sing f0 -> Apply p f0 -> Apply p ('S f0)) -> Apply p s Source #
elimNonEmpty :: forall (a :: Type) (p :: (~>) (NonEmpty a) Type) (s :: NonEmpty a). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: [a]). Sing f1 -> Apply p ('(:|) f0 f1)) -> Apply p s Source #
type family ElimNonEmpty p s p where ... Source #
ElimNonEmpty @a p ('(:|) s0 s1) useThis = useThis s0 s1 |
elimOrdering :: forall (p :: (~>) Ordering Type) (s :: Ordering). Sing s -> Apply p 'LT -> Apply p 'EQ -> Apply p 'GT -> Apply p s Source #
type family ElimOrdering p s p p p where ... Source #
ElimOrdering p 'LT useThis _p1 _p2 = useThis | |
ElimOrdering p 'EQ _p0 useThis _p2 = useThis | |
ElimOrdering p 'GT _p0 _p1 useThis = useThis |
elimProduct :: forall (a :: Type) (p :: (~>) (Product a) Type) (s :: Product a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Product f0)) -> Apply p s Source #
type family ElimProduct p s p where ... Source #
ElimProduct @a p ('Product s0) useThis = useThis s0 |
elimSum :: forall (a :: Type) (p :: (~>) (Sum a) Type) (s :: Sum a). Sing s -> (forall (f0 :: a). Sing f0 -> Apply p ('Sum f0)) -> Apply p s Source #
type family ElimTuple0 p s p where ... Source #
ElimTuple0 p '() useThis = useThis |
elimTuple2 :: forall (a :: Type) (b :: Type) (p :: (~>) ((,) a b) Type) (s :: (,) a b). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> Apply p ('(,) f0 f1)) -> Apply p s Source #
type family ElimTuple2 p s p where ... Source #
ElimTuple2 @a @b p ('(,) s0 s1) useThis = useThis s0 s1 |
elimTuple3 :: forall (a :: Type) (b :: Type) (c :: Type) (p :: (~>) ((,,) a b c) Type) (s :: (,,) a b c). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> Apply p ('(,,) f0 f1 f2)) -> Apply p s Source #
type family ElimTuple3 p s p where ... Source #
ElimTuple3 @a @b @c p ('(,,) s0 s1 s2) useThis = useThis s0 s1 s2 |
elimTuple4 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (p :: (~>) ((,,,) a b c d) Type) (s :: (,,,) a b c d). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> forall (f3 :: d). Sing f3 -> Apply p ('(,,,) f0 f1 f2 f3)) -> Apply p s Source #
type family ElimTuple4 p s p where ... Source #
ElimTuple4 @a @b @c @d p ('(,,,) s0 s1 s2 s3) useThis = useThis s0 s1 s2 s3 |
elimTuple5 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (p :: (~>) ((,,,,) a b c d e) Type) (s :: (,,,,) a b c d e). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> forall (f3 :: d). Sing f3 -> forall (f4 :: e). Sing f4 -> Apply p ('(,,,,) f0 f1 f2 f3 f4)) -> Apply p s Source #
type family ElimTuple5 p s p where ... Source #
ElimTuple5 @a @b @c @d @e p ('(,,,,) s0 s1 s2 s3 s4) useThis = useThis s0 s1 s2 s3 s4 |
elimTuple6 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (p :: (~>) ((,,,,,) a b c d e f) Type) (s :: (,,,,,) a b c d e f). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> forall (f3 :: d). Sing f3 -> forall (f4 :: e). Sing f4 -> forall (f5 :: f). Sing f5 -> Apply p ('(,,,,,) f0 f1 f2 f3 f4 f5)) -> Apply p s Source #
type family ElimTuple6 p s p where ... Source #
ElimTuple6 @a @b @c @d @e @f p ('(,,,,,) s0 s1 s2 s3 s4 s5) useThis = useThis s0 s1 s2 s3 s4 s5 |
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) (s :: (,,,,,,) a b c d e f g). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: b). Sing f1 -> forall (f2 :: c). Sing f2 -> forall (f3 :: d). Sing f3 -> forall (f4 :: e). Sing f4 -> forall (f5 :: f). Sing f5 -> forall (f6 :: g). Sing f6 -> Apply p ('(,,,,,,) f0 f1 f2 f3 f4 f5 f6)) -> Apply p s Source #
type family ElimTuple7 p s p where ... Source #
ElimTuple7 @a @b @c @d @e @f @g p ('(,,,,,,) s0 s1 s2 s3 s4 s5 s6) useThis = useThis s0 s1 s2 s3 s4 s5 s6 |
elimWrappedMonoid :: forall (m :: Type) (p :: (~>) (WrappedMonoid m) Type) (s :: WrappedMonoid m). Sing s -> (forall (f0 :: m). Sing f0 -> Apply p ('WrapMonoid f0)) -> Apply p s Source #
type family ElimWrappedMonoid p s p where ... Source #
ElimWrappedMonoid @m p ('WrapMonoid s0) useThis = useThis s0 |