eliminators-0.1: Dependently typed elimination functions using singletons

Copyright(C) 2017 Ryan Scott
LicenseBSD-style (see the file LICENSE)
MaintainerRyan Scott
StabilityExperimental
PortabilityGHC
Safe HaskellTrustworthy
LanguageHaskell2010

Data.Eliminator

Contents

Description

Dependently typed elimination functions using singletons.

Synopsis

Eliminator functions

Eliminators using '(->)'

These eliminators are defined with propositions of kind <Datatype> -> Type (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.

elimBool :: forall (p :: Bool -> Type) (b :: Bool). Sing b -> p False -> p True -> p b Source #

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> ~> Type (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 '(@@)'.

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.

data FunArrow Source #

An enumeration which represents the possible choices of arrow kind for eliminator functions.

Constructors

(:->)

'(->)'

(:~>)

'(~>)'

class FunType (arr :: FunArrow) Source #

Things which have arrow kinds.

Associated Types

type Fun (k1 :: Type) arr (k2 :: Type) :: Type Source #

An arrow kind.

Instances

FunType (:->) Source # 

Associated Types

type Fun k1 ((:->) :: FunArrow) k2 :: Type Source #

FunType (:~>) Source # 

Associated Types

type Fun k1 ((:~>) :: FunArrow) k2 :: Type Source #

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.

Associated Types

type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2 Source #

An application of a Fun to an argument.

Note that this can't be defined in the same class as Fun due to GHC restrictions on associated type families.

Instances

AppType (:->) Source # 

Associated Types

type App k1 ((:->) :: FunArrow) k2 (f :: Fun k1 (:->) k2) (x :: k1) :: k2 Source #

AppType (:~>) Source # 

Associated Types

type App k1 ((:~>) :: FunArrow) k2 (f :: Fun k1 (:~>) k2) (x :: k1) :: k2 Source #

type FunApp arr = (FunType arr, AppType arr) Source #

Something which has both a Fun and an App.

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 #