{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-| Module: Data.Eliminator Copyright: (C) 2017 Ryan Scott License: BSD-style (see the file LICENSE) Maintainer: Ryan Scott Stability: Experimental Portability: GHC Dependently typed elimination functions using @singletons@. -} module Data.Eliminator ( -- * Eliminator functions -- ** Eliminators using '(->)' -- $eliminators elimBool , elimEither , elimList , elimMaybe , elimNat , elimNonEmpty , elimOrdering , elimTuple0 , elimTuple2 , elimTuple3 , elimTuple4 , elimTuple5 , elimTuple6 , elimTuple7 -- ** Eliminators using '(~>)' -- $eliminators-TyFun , elimBoolTyFun , elimEitherTyFun , elimListTyFun , elimMaybeTyFun , elimNatTyFun , elimNonEmptyTyFun , elimOrderingTyFun , elimTuple0TyFun , elimTuple2TyFun , elimTuple3TyFun , elimTuple4TyFun , elimTuple5TyFun , elimTuple6TyFun , elimTuple7TyFun -- ** Arrow-polymorphic eliminators (very experimental) -- $eliminators-Poly , FunArrow(..) , FunType(..) , type (-?>) , AppType(..) , FunApp , elimBoolPoly , elimEitherPoly , elimListPoly , elimMaybePoly , elimNonEmptyPoly , elimNatPoly , elimOrderingPoly , elimTuple0Poly , elimTuple2Poly , elimTuple3Poly , elimTuple4Poly , elimTuple5Poly , elimTuple6Poly , elimTuple7Poly ) where import Data.Kind (Type) import Data.List.NonEmpty (NonEmpty(..)) import Data.Singletons.Prelude import Data.Singletons.Prelude.List.NonEmpty (Sing(..)) import Data.Singletons.TypeLits import Unsafe.Coerce (unsafeCoerce) {- $eliminators These eliminators are defined with propositions of kind @\ -> '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 elimBool = elimBoolPoly @(:->) 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 elimEither = elimEitherPoly @(:->) 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 elimList = elimListPoly @(:->) 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 elimMaybe = elimMaybePoly @(:->) elimNat :: forall (p :: Nat -> Type) (n :: Nat). Sing n -> p 0 -> (forall (k :: Nat). Sing k -> p k -> p (k :+ 1)) -> p n elimNat = elimNatPoly @(:->) 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 elimNonEmpty = elimNonEmptyPoly @(:->) elimOrdering :: forall (p :: Ordering -> Type) (o :: Ordering). Sing o -> p LT -> p EQ -> p GT -> p o elimOrdering = elimOrderingPoly @(:->) elimTuple0 :: forall (p :: () -> Type) (u :: ()). Sing u -> p '() -> p u elimTuple0 = elimTuple0Poly @(:->) 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 elimTuple2 = elimTuple2Poly @(:->) 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 elimTuple3 = elimTuple3Poly @(:->) 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 elimTuple4 = elimTuple4Poly @(:->) 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 elimTuple5 = elimTuple5Poly @(:->) 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 elimTuple6 = elimTuple6Poly @(:->) 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 elimTuple7 = elimTuple7Poly @(:->) {- $eliminators-TyFun These eliminators are defined with propositions of kind @\ ~> '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 elimBoolTyFun = elimBoolPoly @(:~>) @p 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 elimEitherTyFun = elimEitherPoly @(:~>) @_ @_ @p 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 elimListTyFun = elimListPoly @(:~>) @_ @p 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 elimMaybeTyFun = elimMaybePoly @(:~>) @_ @p elimNatTyFun :: forall (p :: Nat ~> Type) (n :: Nat). Sing n -> p @@ 0 -> (forall (k :: Nat). Sing k -> p @@ k -> p @@ (k :+ 1)) -> p @@ n elimNatTyFun = elimNatPoly @(:~>) @p 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 elimNonEmptyTyFun = elimNonEmptyPoly @(:~>) @_ @p elimOrderingTyFun :: forall (p :: Ordering ~> Type) (o :: Ordering). Sing o -> p @@ LT -> p @@ EQ -> p @@ GT -> p @@ o elimOrderingTyFun = elimOrderingPoly @(:~>) @p elimTuple0TyFun :: forall (p :: () ~> Type) (u :: ()). Sing u -> p @@ '() -> p @@ u elimTuple0TyFun = elimTuple0Poly @(:~>) @p 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 elimTuple2TyFun = elimTuple2Poly @(:~>) @_ @_ @p 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 elimTuple3TyFun = elimTuple3Poly @(:~>) @_ @_ @_ @p 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 elimTuple4TyFun = elimTuple4Poly @(:~>) @_ @_ @_ @_ @p 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 elimTuple5TyFun = elimTuple5Poly @(:~>) @_ @_ @_ @_ @_ @p 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 elimTuple6TyFun = elimTuple6Poly @(:~>) @_ @_ @_ @_ @_ @_ @p 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 elimTuple7TyFun = elimTuple7Poly @(:~>) @_ @_ @_ @_ @_ @_ @_ @p {- $eliminators-Poly 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. data FunArrow = (:->) -- ^ '(->)' | (:~>) -- ^ '(~>)' -- | Things which have arrow kinds. class FunType (arr :: FunArrow) where -- | An arrow kind. type Fun (k1 :: Type) arr (k2 :: Type) :: Type -- | Things which can be applied. class FunType arr => AppType (arr :: FunArrow) where -- | 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. type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2 -- | Something which has both a 'Fun' and an 'App'. type FunApp arr = (FunType arr, AppType arr) instance FunType (:->) where type Fun k1 (:->) k2 = k1 -> k2 instance AppType (:->) where type App k1 (:->) k2 (f :: k1 -> k2) x = f x instance FunType (:~>) where type Fun k1 (:~>) k2 = k1 ~> k2 instance AppType (:~>) where type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x -- | An infix synonym for 'Fun'. infixr 0 -?> type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2 -- Note: it would be nice to have an infix synonym for 'App' as well, but -- the order in which the type variable dependencies occur makes this awkward -- to achieve. 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 elimBoolPoly SFalse pF _ = pF elimBoolPoly STrue _ pT = pT 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 elimEitherPoly (SLeft sl) pLeft _ = pLeft sl elimEitherPoly (SRight sr) _ pRight = pRight sr 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 elimListPoly SNil pNil _ = pNil elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons) 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 elimMaybePoly SNothing pNothing _ = pNothing elimMaybePoly (SJust sx) _ pJust = pJust sx 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 elimNatPoly snat pZ pS = case fromSing snat of 0 -> unsafeCoerce pZ nPlusOne -> case toSing (pred nPlusOne) of SomeSing (sn :: Sing k) -> unsafeCoerce (pS sn (elimNatPoly @arr @p @k sn pZ pS)) 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 elimNonEmptyPoly (sx :%| sxs) pNECons = pNECons sx sxs 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 elimOrderingPoly SLT pLT _ _ = pLT elimOrderingPoly SEQ _ pEQ _ = pEQ elimOrderingPoly SGT _ _ pGT = pGT elimTuple0Poly :: forall (arr :: FunArrow) (p :: (() -?> Type) arr) (u :: ()). FunApp arr => Sing u -> App () arr Type p '() -> App () arr Type p u elimTuple0Poly STuple0 pTuple0 = pTuple0 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 elimTuple2Poly (STuple2 sa sb) pTuple2 = pTuple2 sa sb 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 elimTuple3Poly (STuple3 sa sb sc) pTuple3 = pTuple3 sa sb sc 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 elimTuple4Poly (STuple4 sa sb sc sd) pTuple4 = pTuple4 sa sb sc sd 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 elimTuple5Poly (STuple5 sa sb sc sd se) pTuple5 = pTuple5 sa sb sc sd se 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 elimTuple6Poly (STuple6 sa sb sc sd se sf) pTuple6 = pTuple6 sa sb sc sd se sf 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 elimTuple7Poly (STuple7 sa sb sc sd se sf sg) pTuple7 = pTuple7 sa sb sc sd se sf sg