eliminators 0.1 → 0.2

raw patch · 10 files changed

+588/−687 lines, 10 filesdep +extradep +template-haskelldep +th-abstractionPVP ok

version bump matches the API change (PVP)

Dependencies added: extra, template-haskell, th-abstraction, th-desugar

API changes (from Hackage documentation)

Files

• CHANGELOG.md +8/−1
• eliminators.cabal +8/−3
• src/Data/Eliminator.hs +34/−452
• src/Data/Eliminator/TH.hs +359/−0
• tests/EqualitySpec.hs +73/−93
• tests/GADTSpec.hs +30/−34
• tests/ListSpec.hs +5/−5
• tests/PeanoSpec.hs +36/−35
• tests/PeanoTypes.hs +26/−56
• tests/VecSpec.hs +9/−8

@@ -1,2 +1,9 @@-# 0.1 [2017-07-02]+## 0.2 [2017-07-22]+* Introduce the `Data.Eliminator.TH` module, which provides functionality for+  generating eliminator functions using Template Haskell. Currently, only+  simple algebraic data types that do not use polymorphic recursion are+  supported.+* All eliminators now use predicates with `(~>)`.++## 0.1 [2017-07-02] * Initial release.

@@ -1,5 +1,5 @@ name:                eliminators-version:             0.1+version:             0.2 synopsis:            Dependently typed elimination functions using singletons description:         This library provides eliminators for inductive data types,                      leveraging the power of the @singletons@ library to allow@@ -24,8 +24,13 @@  library   exposed-modules:     Data.Eliminator-  build-depends:       base       >= 4.10 && < 4.11-                     , singletons >= 2.3  && < 2.4+                       Data.Eliminator.TH+  build-depends:       base             >= 4.10  && < 4.11+                     , extra            >= 1.4.2 && < 1.7+                     , singletons       >= 2.3   && < 2.4+                     , template-haskell >= 2.12  && < 2.13+                     , th-abstraction   >= 0.2.3 && < 0.3+                     , th-desugar       >= 1.7   && < 1.8   hs-source-dirs:      src   default-language:    Haskell2010   ghc-options:         -Wall -Wno-unticked-promoted-constructors

@@ -4,6 +4,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}@@ -21,7 +22,6 @@ -} module Data.Eliminator (     -- * Eliminator functions-    -- ** Eliminators using '(->)'     -- $eliminators     elimBool   , elimEither@@ -37,474 +37,56 @@   , 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 @\<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-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 @(:->)+import           Control.Monad.Extra -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 @(:->)+import           Data.Eliminator.TH+import           Data.Kind (Type)+import           Data.List.NonEmpty (NonEmpty(..))+import           Data.Singletons.Prelude+import           Data.Singletons.Prelude.List.NonEmpty (Sing(..))+import           Data.Singletons.TypeLits -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 @(:->)+import qualified GHC.TypeLits as TL -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 @(:->)+import           Language.Haskell.TH.Desugar (tupleNameDegree_maybe) -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 @(:->)+import           Unsafe.Coerce (unsafeCoerce) -{- $eliminators-TyFun+{- $eliminators  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,+defunctionalized (i.e., \"partially applied\") types 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.+The naming conventions are: -Not all eliminators are known to work under this generalized scheme yet (for-instance, eliminators for GADTs).+* If the datatype has an alphanumeric name, its eliminator will have that name+  with @elim@ prepended. -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.+* If the datatype has a symbolic name, its eliminator will have that name+  with @~>@ prepended. -} --- | 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)+$(concatMapM deriveElim [''Bool, ''Either, ''Maybe, ''NonEmpty, ''Ordering])+$(deriveElimNamed "elimList" ''[])+$(concatMapM (\n -> let Just deg = tupleNameDegree_maybe n+                    in deriveElimNamed ("elimTuple" ++ show deg) n)+             [''(), ''(,), ''(,,), ''(,,,), ''(,,,,), ''(,,,,,), ''(,,,,,,)]) -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+-- This is the grimy one we can't define using Template Haskell. -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 =+-- | Although 'Nat' is not actually an inductive data type in GHC, we can+-- pretend that it is using this eliminator.+elimNat :: forall (p :: Nat ~> Type) (n :: Nat).+           Sing n+        -> p @@ 0+        -> (forall (k :: Nat). Sing k -> p @@ k -> p @@ (k TL.+ 1))+        -> p @@ n+elimNat 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+    nPlusOne -> withSomeSing (pred nPlusOne) $ \(sn :: Sing k) ->+                  unsafeCoerce (pS sn (elimNat @p @k sn pZ pS))

@@ -0,0 +1,359 @@+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE Unsafe #-}+{-|+Module:      Data.Eliminator.TH+Copyright:   (C) 2017 Ryan Scott+License:     BSD-style (see the file LICENSE)+Maintainer:  Ryan Scott+Stability:   Experimental+Portability: GHC++Generate dependently typed elimination functions using Template Haskell.+-}+module Data.Eliminator.TH (+    -- * Eliminator generation+    -- $conventions+    deriveElim+  , deriveElimNamed+  ) where++import           Control.Applicative+import           Control.Monad++import           Data.Char (isUpper)+import           Data.Foldable+import qualified Data.Kind as Kind (Type)+import           Data.List.NonEmpty (NonEmpty(..))+import           Data.Maybe+import           Data.Singletons.Prelude++import           Language.Haskell.TH+import           Language.Haskell.TH.Datatype+import           Language.Haskell.TH.Desugar (tupleNameDegree_maybe, unboxedTupleNameDegree_maybe)++{- $conventions+'deriveElim' and 'deriveElimNamed' provide a way to automate the creation of+eliminator functions, which are mostly boilerplate. Here is a complete example+showing how one might use 'deriveElim':++@+$('singletons' [d| data MyList a = MyNil | MyCons a (MyList a) |])+$('deriveElim' ''MyList)+@++This will produce an eliminator function that looks roughly like the following:++@+elimMyList :: forall (a :: 'Type') (p :: MyList a '~>' 'Type') (l :: MyList a).+              'Sing' l+           -> p '@@' MyNil+           -> (forall (x :: a). 'Sing' x+                -> forall (xs :: MyList a). 'Sing' xs -> p '@@' xs+                -> p '@@' (MyCons x xs))+           -> p '@@' l+elimMyList SMyNil pMyNil _ = pMyNil+elimMyList (SMyCons (x' :: 'Sing' x) (xs' :: 'Sing' xs)) pMyNil pMyCons+  = pMyCons x' xs' (elimMyList @a @p @xs pMyNil pMyCons)+@++There are some important things to note here:++* Because these eliminators use 'Sing' under the hood, in order for+  'deriveElim' to work, the 'Sing' instance for the data type given as an+  argument must be in scope. Moreover, 'deriveElim' assumes the naming+  conventions for singled constructors used by the @singletons@ library.+  (This is why the 'singletons' function is used in the example above).++* There is a convention for the order in which the arguments appear.+  The quantified type variables appear in this order:++    1. First, the type variables of the data type itself (@a@, in the above example).++    2. Second, a predicate type variable of kind @\<Datatype\> '~>' 'Type'@+       (@p@, in the above example).++    3. Finally, a type variable of kind @\<Datatype\>@ (@l@, in the above example).++  The function arguments appear in this order:++    1. First, a 'Sing' argument (@'Sing' l@, in the above example).++    2. Next, there are arguments that correspond to each constructor. More on this+       in a second.++  The return type is the predicate type variable applied to the data type+  (@p '@@' (MyCons x xs)@, the above example).++  The type of each constructor argument also follows certain conventions:++    1. For each field, there will be a rank-2 type variable whose kind matches+       the type of the field, followed by a matching 'Sing' type. For instance,+       in the above example, @forall (x :: a). 'Sing' x@ corresponds to the+       first field of @MyCons@.++    2. In addition, if the field is a recursive occurrence of the data type,+       an additional argument will follow the 'Sing' type. This is best+       explained using the above example. In the @MyCons@ constructor, the second+       field (of type @MyCons a@) is a recursive occurrence of @MyCons@, so+       that corresponds to the type+       @forall (xs :: MyList a). 'Sing' xs -> p '@@' xs@, where @p '@@' xs@+       is only present due to the recursion.++    3. Finally, the return type will be the predicate type variable applied+       to a saturated occurrence of the data constructor+       (@p '@@' (MyCons x xs)@, in the above example).++* You'll need to enable lots of GHC extensions in order for the code generated+  by 'deriveElim' to typecheck. You'll need at least the following:++    * @AllowAmbiguousTypes@++    * @GADTs@++    * @RankNTypes@++    * @ScopedTypeVariables@++    * @TemplateHaskell@++    * @TypeApplications@++    * @TypeInType@++* 'deriveElim' doesn't support every possible data type at the moment.+  It is known not to work for the following:++    * Data types defined using @GADTs@ or @ExistentialQuantification@++    * Data family instances++    * Data types which use polymorphic recursion+      (e.g., @data Foo a = Foo (Foo a)@)+-}++-- | @'deriveElim' dataName@ generates a top-level elimination function for the+-- datatype @dataName@. The eliminator will follow these naming conventions:+-- 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.+deriveElim :: Name -> Q [Dec]+deriveElim dataName = deriveElimNamed (eliminatorName dataName) dataName++-- | @'deriveElimNamed' funName dataName@ generates a top-level elimination+-- function named @funName@ for the datatype @dataName@.+deriveElimNamed :: String -> Name -> Q [Dec]+deriveElimNamed funName dataName = do+  info@(DatatypeInfo { datatypeVars    = vars+                     , datatypeVariant = variant+                     , datatypeCons    = cons+                     }) <- reifyDatatype dataName+  let noDataFamilies =+        fail "Eliminators for data family instances are currently not supported"+  case variant of+    DataInstance    -> noDataFamilies+    NewtypeInstance -> noDataFamilies+    Datatype        -> pure ()+    Newtype         -> pure ()+  predVar <- newName "p"+  singVar <- newName "s"+  let elimN = mkName funName+      dataVarBndrs = catMaybes $ map typeToTyVarBndr vars+      promDataKind = datatypeType info+      predVarBndr = KindedTV predVar (InfixT promDataKind ''(~>) (ConT ''Kind.Type))+      singVarBndr = KindedTV singVar promDataKind+  caseTypes <- traverse (caseType dataName predVar) cons+  let returnType  = predType predVar (VarT singVar)+      bndrsPrefix = dataVarBndrs ++ [predVarBndr]+      allBndrs    = bndrsPrefix ++ [singVarBndr]+      elimType = ForallT allBndrs []+                   (ravel (singType singVar:caseTypes) returnType)+      qelimDef+        | null cons+        = do singVal <- newName "singVal"+             pure $ FunD elimN [Clause [VarP singVal] (NormalB (CaseE (VarE singVal) [])) []]++        | otherwise+        = do caseClauses+               <- itraverse (\i -> caseClause dataName elimN+                                              (map tyVarBndrName bndrsPrefix)+                                              i (length cons)) cons+             pure $ FunD elimN caseClauses+  elimDef <- qelimDef+  pure [SigD elimN elimType, elimDef]++caseType :: Name -> Name -> ConstructorInfo -> Q Type+caseType dataName predVar+         (ConstructorInfo { constructorName    = conName+                          , constructorVars    = conVars+                          , constructorContext = conContext+                          , constructorFields  = fieldTypes })+  = do unless (null conVars && null conContext) $+         fail $ unlines+           [ "Eliminators for GADTs or datatypes with existentially quantified"+           , "data constructors currently not supported"+           ]+       vars <- newNameList "f" $ length fieldTypes+       let returnType = predType predVar+                                 (foldl' AppT (ConT conName) (map VarT vars))+           mbInductiveType var varType =+             let inductiveArg = predType predVar (VarT var)+             in mbInductiveCase dataName varType inductiveArg+       pure $ foldr' (\(var, varType) t ->+                        ForallT [KindedTV var varType]+                                []+                                (ravel (singType var:maybeToList (mbInductiveType var varType)) t))+                     returnType+                     (zip vars fieldTypes)++caseClause :: Name -> Name -> [Name] -> Int -> Int+           -> ConstructorInfo -> Q Clause+caseClause dataName elimN bndrNamesPrefix conIndex numCons+    (ConstructorInfo { constructorName   = conName+                     , constructorFields = fieldTypes })+  = do let numFields = length fieldTypes+       singVars    <- newNameList "s"   numFields+       singVarSigs <- newNameList "sTy" numFields+       usedCaseVar <- newName "useThis"+       caseVars    <- ireplicateA numCons $ \i ->+                        if i == conIndex+                        then pure usedCaseVar+                        else newName ("_p" ++ show i)+       let singConName = singDataConName conName+           mkSingVarPat var varSig = SigP (VarP var) (singType varSig)+           singVarPats = zipWith mkSingVarPat singVars singVarSigs++           mbInductiveArg singVar singVarSig varType =+             let prefix = foldAppType (VarE elimN)+                             $ map VarT bndrNamesPrefix+                            ++ [VarT singVarSig]+                 inductiveArg = foldExp prefix+                                  $ VarE singVar:map VarE caseVars+             in mbInductiveCase dataName varType inductiveArg+           mkArg f (singVar, singVarSig, varType) =+             foldExp f $ VarE singVar+                       : maybeToList (mbInductiveArg singVar singVarSig varType)+           rhs = foldl' mkArg (VarE usedCaseVar) $+                        zip3 singVars singVarSigs fieldTypes+       pure $ Clause (ConP singConName singVarPats : map VarP caseVars)+                     (NormalB rhs)+                     []++-- TODO: Rule out polymorphic recursion+mbInductiveCase :: Name -> Type -> a -> Maybe a+mbInductiveCase dataName varType inductiveArg+  = case unfoldType varType of+      headTy :| _+          -- Annoying special case for lists+        | ListT <- headTy+        , dataName == ''[]+       -> Just inductiveArg++        | ConT n <- headTy+        , dataName == n+       -> Just inductiveArg++        | otherwise+       -> Nothing++-- | Construct a type of the form @'Sing' x@ given @x@.+singType :: Name -> Type+singType x = ConT ''Sing `AppT` VarT x++-- | Construct a type of the form @p '@@' ty@ given @p@ and @ty@.+predType :: Name -> Type -> Type+predType p ty = InfixT (VarT p) ''(@@) ty++-- | Generate a list of fresh names with a common prefix, and numbered suffixes.+newNameList :: String -> Int -> Q [Name]+newNameList prefix n = ireplicateA n $ newName . (prefix ++) . show++eliminatorName :: Name -> String+eliminatorName n+  | first:_ <- nStr+  , isUpper first+  = "elim" ++ nStr++  | otherwise+  = "~>" ++ nStr+  where+    nStr = nameBase n++typeToTyVarBndr :: Type -> Maybe TyVarBndr+typeToTyVarBndr (SigT (VarT n) k) = Just $ KindedTV n k+typeToTyVarBndr _                 = Nothing++-- Reconstruct and arrow type from the list of types+ravel :: [Type] -> Type -> Type+ravel []    res = res+ravel (h:t) res = AppT (AppT ArrowT h) (ravel t res)++-- apply an expression to a list of expressions+foldExp :: Exp -> [Exp] -> Exp+foldExp = foldl' AppE++-- apply an expression to a list of types+foldAppType :: Exp -> [Type] -> Exp+foldAppType = foldl' AppTypeE++-- | Decompose an applied type into its individual components. For example, this:+--+-- @+-- Either Int Char+-- @+--+-- would be unfolded to this:+--+-- @+-- Either :| [Int, Char]+-- @+unfoldType :: Type -> NonEmpty Type+unfoldType = go []+  where+    go :: [Type] -> Type -> NonEmpty Type+    go acc (AppT t1 t2)    = go (t2:acc) t1+    go acc (SigT t _)      = go acc t+    go acc (ForallT _ _ t) = go acc t+    go acc t               = t :| acc++tyVarBndrName :: TyVarBndr -> Name+tyVarBndrName (PlainTV  n)   = n+tyVarBndrName (KindedTV n _) = n++itraverse :: Applicative f => (Int -> a -> f b) -> [a] -> f [b]+itraverse f xs0 = go xs0 0 where+  go [] _ = pure []+  go (x:xs) n = (:) <$> f n x <*> (go xs $! (n + 1))++ireplicateA :: Applicative f => Int -> (Int -> f a) -> f [a]+ireplicateA cnt0 f =+    loop cnt0 0+  where+    loop cnt n+        | cnt <= 0  = pure []+        | otherwise = liftA2 (:) (f n) (loop (cnt - 1) $! (n + 1))++-----+-- Taken directly from singletons+-----++singDataConName :: Name -> Name+singDataConName nm+  | nm == '[]                                      = 'SNil+  | nm == '(:)                                     = 'SCons+  | Just degree <- tupleNameDegree_maybe nm        = mkTupleDataName degree+  | Just degree <- unboxedTupleNameDegree_maybe nm = mkTupleDataName degree+  | otherwise                                      = prefixUCName "S" ":%" nm++mkTupleDataName :: Int -> Name+mkTupleDataName n = mkName $ "STuple" ++ (show n)++-- put an uppercase prefix on a name. Takes two prefixes: one for identifiers+-- and one for symbols+prefixUCName :: String -> String -> Name -> Name+prefixUCName pre tyPre n = case (nameBase n) of+    (':' : rest) -> mkName (tyPre ++ rest)+    alpha -> mkName (pre ++ alpha)

@@ -10,7 +10,6 @@ {-# OPTIONS_GHC -fno-warn-orphans #-} module EqualitySpec where -import           Data.Eliminator import           Data.Kind import           Data.Singletons import qualified Data.Type.Equality as DTE@@ -34,6 +33,7 @@  data instance Sing (z :: a :~: b) where   SRefl :: Sing Refl+type (%:~:) = (Sing :: (a :: k) :~: (b :: k) -> Type)  instance SingKind (a :~: b) where   type Demote (a :~: b) = a :~: b@@ -43,22 +43,15 @@ instance SingI Refl where   sing = SRefl -(->:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y -> Type).-           Sing r-        -> p Refl-        -> p r-(->:~:) SRefl pRefl = pRefl- (~>:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y ~> Type).            Sing r         -> p @@ Refl         -> p @@ r (~>:~:) SRefl pRefl = pRefl --- (-?>:~:)- data instance Sing (z :: a :~~: b) where   SHRefl :: Sing HRefl+type (%:~~:) = (Sing :: (a :: j) :~~: (b :: k) -> Type)  instance SingKind (a :~~: b) where   type Demote (a :~~: b) = a :~~: b@@ -68,37 +61,34 @@ instance SingI HRefl where   sing = SHRefl -(->:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).-            Sing r-         -> p HRefl-         -> p r-(->:~~:) SHRefl pHRefl = pHRefl--{--This doesn't typecheck at the moment due to GHC Trac #13879.-TODO: Uncomment this when the fix becomes available.- (~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y ~> Type).             Sing r          -> p @@ HRefl          -> p @@ r (~>:~~:) SHRefl pHRefl = pHRefl--} --- (-?>:~~:)- -----  type WhySym (a :: t) (y :: t) (e :: a :~: y) = y :~: a data WhySymSym (a :: t) :: forall (y :: t). a :~: y ~> Type-type instance Apply (WhySymSym z :: z :~: y ~> Type) x-  = WhySym z y x+type instance Apply (WhySymSym a :: a :~: y ~> Type) x+  = WhySym a y x  sym :: forall (t :: Type) (a :: t) (b :: t).        a :~: b -> b :~: a sym eq = withSomeSing eq $ \(singEq :: Sing r) ->            (~>:~:) @t @a @b @r @(WhySymSym a) singEq Refl +type WhyHsym (a :: j) (y :: z) (e :: a :~~: y) = y :~~: a+data WhyHsymSym (a :: j) :: forall (z :: Type) (y :: z). a :~~: y ~> Type+type instance Apply (WhyHsymSym a :: a :~~: y ~> Type) x+  = WhyHsym a y x++hsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k).+        a :~~: b -> b :~~: a+hsym eq = withSomeSing eq $ \(singEq :: Sing r) ->+            (~>:~~:) @j @k @a @b @r @(WhyHsymSym a) singEq HRefl+ type family Symmetry (x :: (a :: k) :~: (b :: k)) :: b :~: a where   Symmetry Refl = Refl @@ -113,86 +103,76 @@                  Sing e -> Symmetry (Symmetry e) :~: e symIdempotent se = (~>:~:) @t @a @b @e @(WhySymIdempotentSym a) se Refl -type WhyReplacePoly (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)-                    (y :: t) (e :: from :~: y) = App t arr Type p y-data WhyReplacePolySym (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)+type family Hsymmetry (x :: (a :: j) :~~: (b :: k)) :: b :~~: a where+  Hsymmetry HRefl = HRefl++type WhyHsymIdempotent (a :: j) (y :: z) (r :: a :~~: y)+  = Hsymmetry (Hsymmetry r) :~: r+data WhyHsymIdempotentSym (a :: j) :: forall (z :: Type) (y :: z). a :~~: y ~> Type+type instance Apply (WhyHsymIdempotentSym a :: a :~~: y ~> Type) r+  = WhyHsymIdempotent a y r++hsymIdempotent :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)+                         (e :: a :~~: b).+                  Sing e -> Hsymmetry (Hsymmetry e) :~: e+hsymIdempotent se = (~>:~~:) @j @k @a @b @e @(WhyHsymIdempotentSym a) se Refl++type WhyReplace (from :: t) (p :: t ~> Type)+                (y :: t) (e :: from :~: y) = p @@ y+data WhyReplaceSym (from :: t) (p :: t ~> Type)   :: forall (y :: t). from :~: y ~> Type-type instance Apply (WhyReplacePolySym arr from p :: from :~: y ~> Type) x-  = WhyReplacePoly arr from p y x+type instance Apply (WhyReplaceSym from p :: from :~: y ~> Type) x+  = WhyReplace from p y x -replace :: forall (t :: Type) (from :: t) (to :: t) (p :: t -> Type).-           p from+replace :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type).+           p @@ from         -> from :~: to-        -> p to-replace = replacePoly @(:->)+        -> p @@ to+replace from eq =+  withSomeSing eq $ \(singEq :: Sing r) ->+    (~>:~:) @t @from @to @r @(WhyReplaceSym from p) singEq from -replaceTyFun :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type).-                p @@ from-             -> from :~: to-             -> p @@ to-replaceTyFun = replacePoly @(:~>) @_ @_ @_ @p+{-+type WhyHreplace (from :: j) (p :: forall (z :: Type). z ~> Type)+                 (y :: k) (e :: from :~~: y) = p @@ y+data WhyHreplaceSym (from :: j) (p :: forall (z :: Type). z ~> Type)+  :: forall (k :: Type) (y :: k). from :~~: y ~> Type+type instance Apply (WhyHreplaceSym from p :: from :~~: y ~> Type) x+  = WhyHreplace from p y x -replacePoly :: forall (arr :: FunArrow) (t :: Type) (from :: t) (to :: t)-                      (p :: (t -?> Type) arr).-               FunApp arr-            => App t arr Type p from-            -> from :~: to-            -> App t arr Type p to-replacePoly from eq =+hreplace :: forall (j :: Type) (k :: Type) (from :: j) (to :: k)+                   (p :: forall (z :: Type). z ~> Type).+            p @@ from+         -> from :~~: to+         -> p @@ to+hreplace from heq =   withSomeSing eq $ \(singEq :: Sing r) ->-    (~>:~:) @t @from @to @r @(WhyReplacePolySym arr from p) singEq from+    (~>:~~:) @j @k @from @to @(WhyHreplaceSym from p) singEq from+-} -type WhyLeibnizPoly (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t) (z :: t)-  = App t arr Type f a -> App t arr Type f z-data WhyLeibnizPolySym (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t)-  :: t ~> Type-type instance Apply (WhyLeibnizPolySym arr f a) z = WhyLeibnizPoly arr f a z+type WhyLeibniz (f :: t ~> Type) (a :: t) (z :: t)+  = f @@ a -> f @@ z+data WhyLeibnizSym (f :: t ~> Type) (a :: t) :: t ~> Type+type instance Apply (WhyLeibnizSym f a) z = WhyLeibniz f a z -leibniz :: forall (t :: Type) (f :: t -> Type) (a :: t) (b :: t).+leibniz :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).            a :~: b-        -> f a-        -> f b-leibniz = leibnizPoly @(:->)--leibnizTyFun :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).-                a :~: b-             -> f @@ a-             -> f @@ b-leibnizTyFun = leibnizPoly @(:~>) @_ @f--leibnizPoly :: forall (arr :: FunArrow) (t :: Type) (f :: (t -?> Type) arr)-                      (a :: t) (b :: t).-               FunApp arr-            => a :~: b-            -> App t arr Type f a-            -> App t arr Type f b-leibnizPoly = replaceTyFun @t @a @b @(WhyLeibnizPolySym arr f a) id+        -> f @@ a+        -> f @@ b+leibniz = replace @t @a @b @(WhyLeibnizSym f a) id -type WhyCongPoly (arr :: FunArrow) (x :: Type) (y :: Type) (f :: (x -?> y) arr)-                 (a :: x) (z :: x) (e :: a :~: z)-  = App x arr y f a :~: App x arr y f z-data WhyCongPolySym (arr :: FunArrow) (x :: Type) (y :: Type) (f :: (x -?> y) arr)-                    (a :: x) :: forall (z :: x). a :~: z ~> Type-type instance Apply (WhyCongPolySym arr x y f a :: a :~: z ~> Type) asdf-  = WhyCongPoly arr x y f a z asdf+type WhyCong (x :: Type) (y :: Type) (f :: x ~> y)+             (a :: x) (z :: x) (e :: a :~: z)+  = f @@ a :~: f @@ z+data WhyCongSym (x :: Type) (y :: Type) (f :: x ~> y)+                (a :: x) :: forall (z :: x). a :~: z ~> Type+type instance Apply (WhyCongSym x y f a :: a :~: z ~> Type) e+  = WhyCong x y f a z e -cong :: forall (x :: Type) (y :: Type) (f :: x -> y)+cong :: forall (x :: Type) (y :: Type) (f :: x ~> y)                (a :: x) (b :: x).         a :~: b-     -> f a :~: f b-cong = congPoly @(:->) @_ @_ @f--congTyFun :: forall (x :: Type) (y :: Type) (f :: x ~> y)-                    (a :: x) (b :: x).-             a :~: b-          -> f @@ a :~: f @@ b-congTyFun = congPoly @(:~>) @_ @_ @f--congPoly :: forall (arr :: FunArrow) (x :: Type) (y :: Type) (f :: (x -?> y) arr)-                   (a :: x) (b :: x).-            FunApp arr-         => a :~: b-         -> App x arr y f a :~: App x arr y f b-congPoly eq =+     -> f @@ a :~: f @@ b+cong eq =   withSomeSing eq $ \(singEq :: Sing r) ->-    (~>:~:) @x @a @b @r @(WhyCongPolySym arr x y f a) singEq Refl+    (~>:~:) @x @a @b @r @(WhyCongSym x y f a) singEq Refl

@@ -8,7 +8,6 @@ {-# LANGUAGE TypeOperators #-} module GADTSpec where -import Data.Eliminator import Data.Kind import Data.Singletons @@ -27,49 +26,46 @@  data instance Sing (z :: So what) where   SOh :: Sing Oh+type SSo = (Sing :: So what -> Type) -elimSo :: forall (what :: Bool) (s :: So what) (p :: forall (long_sucker :: Bool). So long_sucker -> Type).+elimSo :: forall (what :: Bool) (s :: So what) (p :: forall (long_sucker :: Bool). So long_sucker ~> Type).           Sing s-       -> p Oh-       -> p s+       -> p @@ Oh+       -> p @@ s elimSo SOh pOh = pOh -elimSoTyFun :: forall (what :: Bool) (s :: So what) (p :: forall (long_sucker :: Bool). So long_sucker ~> Type).-               Sing s-            -> p @@ Oh-            -> p @@ s-elimSoTyFun SOh pOh = pOh+data Flarble (a :: Type) (b :: Type) where+  MkFlarble1 :: a -> Flarble a b+  MkFlarble2 :: a ~ Bool => Flarble a (Maybe b) -{--I don't know how to make this kind-check :(-elimSoPoly :: forall (arr :: FunArrow) (what :: Bool) (s :: So what)-                     (p :: forall (long_sucker :: Bool). (So long_sucker -?> Type) arr).-              Sing s-           -> App (So True) arr Type p Oh-           -> App (So what) arr Type p s-elimSoPoly SOh pOh = pOh--}+data instance Sing (z :: Flarble a b) where+  SMkFlarble1 :: Sing x -> Sing (MkFlarble1 x)+  SMkFlarble2 :: Sing MkFlarble2+type SFlarble = (Sing :: Flarble a b -> Type) +elimFlarble :: forall (a :: Type) (b :: Type)+                      (p :: forall (x :: Type) (y :: Type). Flarble x y ~> Type)+                      (f :: Flarble a b).+               Sing f+            -> (forall (a' :: Type) (b' :: Type) (x :: a'). Sing x -> p @@ (MkFlarble1 x :: Flarble a' b'))+            -> (forall (b' :: Type). p @@ (MkFlarble2 :: Flarble Bool (Maybe b')))+            -> p @@ f+elimFlarble s@(SMkFlarble1 sx) pMkFlarble1 _ =+  case s of+    (_ :: Sing (MkFlarble1 x :: Flarble a' b')) -> pMkFlarble1 @a' @b' @x sx+elimFlarble s@SMkFlarble2 _ pMkFlarble2 =+  case s of+    (_ :: Sing (MkFlarble2 :: Flarble Bool (Maybe b'))) -> pMkFlarble2 @b'+ data Obj :: Type where   MkObj :: o -> Obj  data instance Sing (z :: Obj) where   SMkObj :: forall (obj :: obiwan). Sing obj -> Sing (MkObj obj)+type SObj = (Sing :: Obj -> Type) -elimObj :: forall (o :: Obj) (p :: Obj -> Type).+elimObj :: forall (o :: Obj) (p :: Obj ~> Type).            Sing o-        -> (forall (obj :: Type) (x :: obj). Sing x -> p (MkObj x))-        -> p o-elimObj = elimObjPoly @(:->) @o @p--elimObjTyFun :: forall (o :: Obj) (p :: Obj ~> Type).-                Sing o-             -> (forall (obj :: Type) (x :: obj). Sing x -> p @@ (MkObj x))-             -> p @@ o-elimObjTyFun = elimObjPoly @(:~>) @o @p--elimObjPoly :: forall (arr :: FunArrow) (o :: Obj) (p :: (Obj -?> Type) arr).-               Sing o-            -> (forall (obj :: Type) (x :: obj). Sing x -> App Obj arr Type p (MkObj x))-            -> App Obj arr Type p o-elimObjPoly (SMkObj (x :: Sing (obj :: obiwan))) pMkObj = pMkObj @obiwan @obj x+        -> (forall (obj :: Type) (x :: obj). Sing x -> p @@ (MkObj x))+        -> p @@ o+elimObj (SMkObj (x :: Sing (obj :: obiwan))) pMkObj = pMkObj @obiwan @obj x

@@ -14,7 +14,7 @@ import Data.Singletons.Prelude.List import Data.Type.Equality -import EqualitySpec (congTyFun)+import EqualitySpec (cong)  import ListTypes @@ -32,7 +32,7 @@                       SingI l                    => Length l :~: Length (Map f l) mapPreservesLength-  = elimListTyFun @x @(WhyMapPreservesLengthSym1 f) @l (sing @_ @l) base step+  = elimList @x @(WhyMapPreservesLengthSym1 f) @l (sing @_ @l) base step   where     base :: WhyMapPreservesLength f '[]     base = Refl@@ -41,14 +41,14 @@             Sing s -> Sing ss          -> WhyMapPreservesLength f ss          -> WhyMapPreservesLength f (s:ss)-    step _ _ = congTyFun @_ @_ @((:+$$) 1)+    step _ _ = cong @_ @_ @((:+$$) 1)  mapFusion :: forall (x :: Type) (y :: Type) (z :: Type)                     (f :: y ~> z) (g :: x ~> y) (l :: [x]).                     SingI l                  => Map f (Map g l) :~: Map (f :.$$$ g) l mapFusion-  = elimListTyFun @x @(WhyMapFusionSym2 f g) @l (sing @_ @l) base step+  = elimList @x @(WhyMapFusionSym2 f g) @l (sing @_ @l) base step   where     base :: WhyMapFusion f g '[]     base = Refl@@ -57,4 +57,4 @@             Sing s -> Sing ss          -> WhyMapFusion f g ss          -> WhyMapFusion f g (s:ss)-    step _ _ = congTyFun @_ @_ @((:$$) (f @@ (g @@ s)))+    step _ _ = cong @_ @_ @((:$$) (f @@ (g @@ s)))

@@ -1,6 +1,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-} module PeanoSpec where  import Data.Kind@@ -19,63 +20,63 @@     it "works with empty lists" $       replicateVec SZ () `shouldBe` VNil     it "works with non-empty lists" $-      replicateVec (SS SZ) () `shouldBe` VCons () VNil+      replicateVec (SS SZ) () `shouldBe` () :# VNil   describe "mapVec" $ do     it "maps over a Vec" $ do-      mapVec reverse ("hello" `VCons` "world" `VCons` VNil)-        `shouldBe` ("olleh" `VCons` "dlrow" `VCons` VNil)+      mapVec reverse ("hello" :# "world" :# VNil)+          `shouldBe` ("olleh" :# "dlrow" :# VNil)   describe "zipWithVec" $ do     it "zips two Vecs" $ do-      zipWithVec (,) ((2 :: Int) `VCons` 22 `VCons` VNil)-                     ("chicken-of-the-woods" `VCons` "hen-of-woods" `VCons` VNil)-        `shouldBe` ((2, "chicken-of-the-woods") `VCons` (22, "hen-of-woods")-                                                `VCons` VNil)+      zipWithVec (,) ((2 :: Int) :# 22 :# VNil)+                     ("chicken-of-the-woods" :# "hen-of-woods" :# VNil)+        `shouldBe` ((2, "chicken-of-the-woods") :# (22, "hen-of-woods")+                                                :# VNil)   describe "appendVec" $ do     it "appends two Vecs" $ do-      appendVec ("portabello" `VCons` "bay-bolete"-                              `VCons` "funnel-chantrelle"-                              `VCons` VNil)-                ("sheathed-woodtuft" `VCons` "puffball" `VCons` VNil)-        `shouldBe` ("portabello" `VCons` "bay-bolete"-                                 `VCons` "funnel-chantrelle"-                                 `VCons` "sheathed-woodtuft"-                                 `VCons` "puffball"-                                 `VCons` VNil)+      appendVec ("portabello" :# "bay-bolete"+                              :# "funnel-chantrelle"+                              :# VNil)+                ("sheathed-woodtuft" :# "puffball" :# VNil)+        `shouldBe` ("portabello" :# "bay-bolete"+                                 :# "funnel-chantrelle"+                                 :# "sheathed-woodtuft"+                                 :# "puffball"+                                 :# VNil)   describe "transposeVec" $ do     it "transposes a Vec" $ do-      transposeVec (('a' `VCons` 'b' `VCons` 'c' `VCons` VNil)-            `VCons` ('d' `VCons` 'e' `VCons` 'f' `VCons` VNil)-            `VCons` VNil)+      transposeVec (('a' :# 'b' :# 'c' :# VNil)+                 :# ('d' :# 'e' :# 'f' :# VNil)+                 :# VNil)         `shouldBe`-                   (('a' `VCons` 'd' `VCons` VNil)-            `VCons` ('b' `VCons` 'e' `VCons` VNil)-            `VCons` ('c' `VCons` 'f' `VCons` VNil)-            `VCons` VNil)+                   (('a' :# 'd' :# VNil)+                 :# ('b' :# 'e' :# VNil)+                 :# ('c' :# 'f' :# VNil)+                 :# VNil)  -----  replicateVec :: forall (e :: Type) (howMany :: Peano).                 Sing howMany -> e -> Vec e howMany-replicateVec s e = elimPeano @howMany @(Vec e) s VNil step+replicateVec s e = elimPeano @(TyCon1 (Vec e)) @howMany s VNil step   where     step :: forall (k :: Peano). Sing k -> Vec e k -> Vec e (S k)-    step _ = VCons e+    step _ = (e :#)  mapVec :: forall (a :: Type) (b :: Type) (n :: Peano).           SingI n        => (a -> b) -> Vec a n -> Vec b n-mapVec f = elimPeanoTyFun @n @(WhyMapVecSym2 a b) (sing @_ @n) base step+mapVec f = elimPeano @(WhyMapVecSym2 a b) @n (sing @_ @n) base step   where     base :: WhyMapVec a b Z     base _ = VNil      step :: forall (k :: Peano). Sing k -> WhyMapVec a b k -> WhyMapVec a b (S k)-    step _ mapK vK = VCons (f (vhead vK)) (mapK (vtail vK))+    step _ mapK vK = f (vhead vK) :# mapK (vtail vK)  zipWithVec :: forall (a :: Type) (b :: Type) (c :: Type) (n :: Peano).               SingI n            => (a -> b -> c) -> Vec a n -> Vec b n -> Vec c n-zipWithVec f = elimPeanoTyFun @n @(WhyZipWithVecSym3 a b c) (sing @_ @n) base step+zipWithVec f = elimPeano @(WhyZipWithVecSym3 a b c) @n (sing @_ @n) base step   where     base :: WhyZipWithVec a b c Z     base _ _ = VNil@@ -84,13 +85,13 @@             Sing k          -> WhyZipWithVec a b c k          -> WhyZipWithVec a b c (S k)-    step _ zwK vaK vbK = VCons (f   (vhead vaK) (vhead vbK))-                               (zwK (vtail vaK) (vtail vbK))+    step _ zwK vaK vbK = f   (vhead vaK) (vhead vbK)+                      :# zwK (vtail vaK) (vtail vbK)  appendVec :: forall (e :: Type) (n :: Peano) (m :: Peano).              SingI n-          => Vec e n -> Vec e m -> Vec e (Plus n m)-appendVec = elimPeanoTyFun @n @(WhyAppendVecSym2 e m) (sing @_ @n) base step+          => Vec e n -> Vec e m -> Vec e (n `Plus` m)+appendVec = elimPeano @(WhyAppendVecSym2 e m) @n (sing @_ @n) base step   where     base :: WhyAppendVec e m Z     base _ = id@@ -99,12 +100,12 @@             Sing k          -> WhyAppendVec e m k          -> WhyAppendVec e m (S k)-    step _ avK vK1 vK2 = VCons (vhead vK1) (avK (vtail vK1) vK2)+    step _ avK vK1 vK2 = vhead vK1 :# avK (vtail vK1) vK2  transposeVec :: forall (e :: Type) (n :: Peano) (m :: Peano).                 (SingI n, SingI m)              => Vec (Vec e m) n -> Vec (Vec e n) m-transposeVec = elimPeanoTyFun @n @(WhyTransposeVecSym2 e m) (sing @_ @n) base step+transposeVec = elimPeano @(WhyTransposeVecSym2 e m) @n (sing @_ @n) base step   where     base :: WhyTransposeVec e m Z     base _ = replicateVec (sing @_ @m) VNil@@ -113,4 +114,4 @@             Sing k          -> WhyTransposeVec e m k          -> WhyTransposeVec e m (S k)-    step _ transK vK = zipWithVec VCons (vhead vK) (transK (vtail vK))+    step _ transK vK = zipWithVec (:#) (vhead vK) (transK (vtail vK))

@@ -1,106 +1,76 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module PeanoTypes where -import Data.Eliminator+import Data.Eliminator.TH import Data.Kind import Data.Singletons.TH  $(singletons [d|   data Peano = Z | S Peano +  infixl 6 `plus`   plus :: Peano -> Peano -> Peano   plus Z     m = m   plus (S k) m = S (plus k m) +  infixl 7 `times`   times :: Peano -> Peano -> Peano   times Z     _ = Z   times (S k) m = plus m (times k m)   |])--elimPeano :: forall (n :: Peano) (p :: Peano -> Type).-             Sing n-          -> p Z-          -> (forall (k :: Peano). Sing k -> p k -> p (S k))-          -> p n-elimPeano = elimPeanoPoly @(:->) @n @p--elimPeanoTyFun :: forall (n :: Peano) (p :: Peano ~> Type).-                  Sing n-               -> p @@ Z-               -> (forall (k :: Peano). Sing k -> p @@ k -> p @@ (S k))-               -> p @@ n-elimPeanoTyFun = elimPeanoPoly @(:~>) @n @p--elimPeanoPoly :: forall (arr :: FunArrow) (n :: Peano) (p :: (Peano -?> Type) arr).-                 FunApp arr-              => Sing n-              -> App Peano arr Type p Z-              -> (forall (k :: Peano). Sing k -> App Peano arr Type p k-                                              -> App Peano arr Type p (S k))-              -> App Peano arr Type p n-elimPeanoPoly SZ pZ _ = pZ-elimPeanoPoly (SS (sk :: Sing k)) pZ pS = pS sk (elimPeanoPoly @arr @k @p sk pZ pS)+$(deriveElim ''Peano)  data Vec a (n :: Peano) where-  VNil  :: Vec a Z-  VCons :: { vhead :: a, vtail :: Vec a n } -> Vec a (S n)-infixr 5 `VCons`+  VNil :: Vec a Z+  (:#) :: { vhead :: a, vtail :: Vec a n } -> Vec a (S n)+infixr 5 :# deriving instance Eq a   => Eq (Vec a n) deriving instance Ord a  => Ord (Vec a n) deriving instance Show a => Show (Vec a n)  data instance Sing (z :: Vec a n) where-  SVNil  :: Sing VNil-  SVCons :: { sVhead :: Sing x, sVtail :: Sing xs } -> Sing (VCons x xs)+  SVNil :: Sing VNil+  (:%#) :: { sVhead :: Sing x, sVtail :: Sing xs } -> Sing (x :# xs)+type SVec = (Sing :: Vec a n -> Type)+infixr 5 :%#  instance SingKind a => SingKind (Vec a n) where   type Demote (Vec a n) = Vec (Demote a) n-  fromSing SVNil         = VNil-  fromSing (SVCons x xs) = VCons (fromSing x) (fromSing xs)+  fromSing SVNil      = VNil+  fromSing (x :%# xs) = fromSing x :# fromSing xs   toSing VNil = SomeSing SVNil-  toSing (VCons x xs) =+  toSing (x :# xs) =     withSomeSing x $ \sx ->       withSomeSing xs $ \sxs ->-        SomeSing $ SVCons sx sxs+        SomeSing $ sx :%# sxs  instance SingI VNil where   sing = SVNil -instance (SingI x, SingI xs) => SingI (VCons x xs) where-  sing = SVCons sing sing+instance (SingI x, SingI xs) => SingI (x :# xs) where+  sing = sing :%# sing  elimVec :: forall (a :: Type) (n :: Peano)-                  (p :: forall (k :: Peano). Vec a k -> Type) (v :: Vec a n).+                  (p :: forall (k :: Peano). Vec a k ~> Type) (v :: Vec a n).            Sing v-        -> p VNil+        -> p @@ VNil         -> (forall (k :: Peano) (x :: a) (xs :: Vec a k).-                   Sing x -> Sing xs -> p xs -> p (VCons x xs))-        -> p v+                   Sing x -> Sing xs -> p @@ xs -> p @@ (x :# xs))+        -> p @@ v elimVec SVNil pVNil _ = pVNil-elimVec (SVCons sx (sxs :: Sing (xs :: Vec a k))) pVNil pVCons =+elimVec (sx :%# (sxs :: Sing (xs :: Vec a k))) pVNil pVCons =   pVCons sx sxs (elimVec @a @k @p @xs sxs pVNil pVCons) -elimVecTyFun :: forall (a :: Type) (n :: Peano)-                       (p :: forall (k :: Peano). Vec a k ~> Type) (v :: Vec a n).-                Sing v-             -> p @@ VNil-             -> (forall (k :: Peano) (x :: a) (xs :: Vec a k).-                        Sing x -> Sing xs -> p @@ xs -> p @@ (VCons x xs))-             -> p @@ v-elimVecTyFun SVNil pVNil _ = pVNil-elimVecTyFun (SVCons sx (sxs :: Sing (xs :: Vec a k))) pVNil pVCons =-  pVCons sx sxs (elimVecTyFun @a @k @p @xs sxs pVNil pVCons)- type WhyMapVec (a :: Type) (b :: Type) (n :: Peano) = Vec a n -> Vec b n $(genDefunSymbols [''WhyMapVec]) @@ -109,7 +79,7 @@ $(genDefunSymbols [''WhyZipWithVec])  type WhyAppendVec (e :: Type) (m :: Peano) (n :: Peano)-  = Vec e n -> Vec e m -> Vec e (Plus n m)+  = Vec e n -> Vec e m -> Vec e (n `Plus` m) $(genDefunSymbols [''WhyAppendVec])  type WhyTransposeVec (e :: Type) (m :: Peano) (n :: Peano)@@ -117,7 +87,7 @@ $(genDefunSymbols [''WhyTransposeVec])  type WhyConcatVec (e :: Type) (j :: Peano) (n :: Peano) (l :: Vec (Vec e j) n)-  = Vec e (Times n j)+  = Vec e (n `Times` j) data WhyConcatVecSym (e :: Type) (j :: Peano)   :: forall (n :: Peano). Vec (Vec e j) n ~> Type type instance Apply (WhyConcatVecSym e j :: Vec (Vec e j) n ~> Type) l

@@ -2,6 +2,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-} module VecSpec where  import Data.Kind@@ -19,19 +20,19 @@ spec = parallel $ do   describe "concatVec" $ do     it "concats a Vec of Vecs" $ do-      concatVec ((False `VCons` True  `VCons` False `VCons` VNil)-         `VCons` (True  `VCons` False `VCons` True  `VCons` VNil)-         `VCons` VNil)-        `shouldBe` (False `VCons` True  `VCons` False `VCons` True-                          `VCons` False `VCons` True  `VCons` VNil)+      concatVec ((False :# True  :# False :# VNil)+              :# (True  :# False :# True  :# VNil)+              :# VNil)+        `shouldBe` (False :# True  :# False :# True+                          :# False :# True  :# VNil)  -----  concatVec :: forall (e :: Type) (n :: Peano) (j :: Peano).              (SingKind e, SingI j, e ~ Demote e)-          => Vec (Vec e j) n -> Vec e (Times n j)+          => Vec (Vec e j) n -> Vec e (n `Times` j) concatVec l = withSomeSing l $ \(singL :: Sing l) ->-                elimVecTyFun @(Vec e j) @n @(WhyConcatVecSym e j) @l singL base step+                elimVec @(Vec e j) @n @(WhyConcatVecSym e j) @l singL base step   where     base :: WhyConcatVec e j Z VNil     base = VNil@@ -39,5 +40,5 @@     step :: forall (k :: Peano) (x :: Vec e j) (xs :: Vec (Vec e j) k).                    Sing x -> Sing xs                 -> WhyConcatVec e j k     xs-                -> WhyConcatVec e j (S k) (VCons x xs)+                -> WhyConcatVec e j (S k) (x :# xs)     step h _ vKJ = appendVec (fromSing h) vKJ