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) (s :: Bool). Sing s -> (@@) p False -> (@@) p True -> (@@) p s
- elimEither :: forall (a :: Type) (b :: Type) (p :: (~>) (Either a b) Type) (s :: Either a b). Sing s -> (forall (f0 :: a). Sing f0 -> (@@) p (Left f0)) -> (forall (f0 :: b). Sing f0 -> (@@) p (Right f0)) -> (@@) p s
- elimList :: forall (a :: Type) (p :: (~>) ([] a) Type) (s :: [] a). Sing s -> (@@) p [] -> (forall (f0 :: a). Sing f0 -> forall (f1 :: [a]). Sing f1 -> (@@) p f1 -> (@@) p ((:) f0 f1)) -> (@@) p s
- elimMaybe :: forall (a :: Type) (p :: (~>) (Maybe a) Type) (s :: Maybe a). Sing s -> (@@) p Nothing -> (forall (f0 :: a). Sing f0 -> (@@) p (Just f0)) -> (@@) p s
- elimNat :: forall (p :: (~>) Nat Type) (s :: Nat). Sing s -> (@@) p Z -> (forall (f0 :: Nat). Sing f0 -> (@@) p f0 -> (@@) p (S f0)) -> (@@) p s
- elimNonEmpty :: forall (a :: Type) (p :: (~>) (NonEmpty a) Type) (s :: NonEmpty a). Sing s -> (forall (f0 :: a). Sing f0 -> forall (f1 :: [a]). Sing f1 -> (@@) p ((:|) f0 f1)) -> (@@) p s
- elimOrdering :: forall (p :: (~>) Ordering Type) (s :: Ordering). Sing s -> (@@) p LT -> (@@) p EQ -> (@@) p GT -> (@@) p s
- elimTuple0 :: forall (p :: (~>) () Type) (s :: ()). Sing s -> (@@) p () -> (@@) p s
- 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 -> (@@) p ((,) f0 f1)) -> (@@) p s
- 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 -> (@@) p ((,,) f0 f1 f2)) -> (@@) p s
- 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 -> (@@) p ((,,,) f0 f1 f2 f3)) -> (@@) p s
- 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 -> (@@) p ((,,,,) f0 f1 f2 f3 f4)) -> (@@) p s
- 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 -> (@@) p ((,,,,,) f0 f1 f2 f3 f4 f5)) -> (@@) p s
- 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 -> (@@) p ((,,,,,,) f0 f1 f2 f3 f4 f5 f6)) -> (@@) p s
Eliminator functions
These eliminators are defined with propositions of kind <Datatype> ~>
(that is, using the '(~>)' 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 '(@@)'.Type
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.
elimBool :: forall (p :: (~>) Bool Type) (s :: Bool). Sing s -> (@@) p False -> (@@) p True -> (@@) 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 -> (@@) p (Left f0)) -> (forall (f0 :: b). Sing f0 -> (@@) p (Right f0)) -> (@@) p s Source #
elimList :: forall (a :: Type) (p :: (~>) ([] a) Type) (s :: [] a). Sing s -> (@@) p [] -> (forall (f0 :: a). Sing f0 -> forall (f1 :: [a]). Sing f1 -> (@@) p f1 -> (@@) p ((:) f0 f1)) -> (@@) p s Source #
elimMaybe :: forall (a :: Type) (p :: (~>) (Maybe a) Type) (s :: Maybe a). Sing s -> (@@) p Nothing -> (forall (f0 :: a). Sing f0 -> (@@) p (Just f0)) -> (@@) p s Source #
elimNat :: forall (p :: (~>) Nat Type) (s :: Nat). Sing s -> (@@) p Z -> (forall (f0 :: Nat). Sing f0 -> (@@) p f0 -> (@@) p (S f0)) -> (@@) 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 -> (@@) p ((:|) f0 f1)) -> (@@) p s Source #
elimOrdering :: forall (p :: (~>) Ordering Type) (s :: Ordering). Sing s -> (@@) p LT -> (@@) p EQ -> (@@) p GT -> (@@) p s Source #
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 -> (@@) p ((,) f0 f1)) -> (@@) p s Source #
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 -> (@@) p ((,,) f0 f1 f2)) -> (@@) p s Source #
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 -> (@@) p ((,,,) f0 f1 f2 f3)) -> (@@) p s Source #
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 -> (@@) p ((,,,,) f0 f1 f2 f3 f4)) -> (@@) p s Source #
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 -> (@@) p ((,,,,,) f0 f1 f2 f3 f4 f5)) -> (@@) p s 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) (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 -> (@@) p ((,,,,,,) f0 f1 f2 f3 f4 f5 f6)) -> (@@) p s Source #