diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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. diff --git a/eliminators.cabal b/eliminators.cabal --- a/eliminators.cabal +++ b/eliminators.cabal @@ -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 diff --git a/src/Data/Eliminator.hs b/src/Data/Eliminator.hs --- a/src/Data/Eliminator.hs +++ b/src/Data/Eliminator.hs @@ -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 @\ -> '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 @\ ~> '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)) diff --git a/src/Data/Eliminator/TH.hs b/src/Data/Eliminator/TH.hs new file mode 100644 --- /dev/null +++ b/src/Data/Eliminator/TH.hs @@ -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 @\ '~>' 'Type'@ + (@p@, in the above example). + + 3. Finally, a type variable of kind @\@ (@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) diff --git a/tests/EqualitySpec.hs b/tests/EqualitySpec.hs --- a/tests/EqualitySpec.hs +++ b/tests/EqualitySpec.hs @@ -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 diff --git a/tests/GADTSpec.hs b/tests/GADTSpec.hs --- a/tests/GADTSpec.hs +++ b/tests/GADTSpec.hs @@ -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 diff --git a/tests/ListSpec.hs b/tests/ListSpec.hs --- a/tests/ListSpec.hs +++ b/tests/ListSpec.hs @@ -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))) diff --git a/tests/PeanoSpec.hs b/tests/PeanoSpec.hs --- a/tests/PeanoSpec.hs +++ b/tests/PeanoSpec.hs @@ -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)) diff --git a/tests/PeanoTypes.hs b/tests/PeanoTypes.hs --- a/tests/PeanoTypes.hs +++ b/tests/PeanoTypes.hs @@ -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 diff --git a/tests/VecSpec.hs b/tests/VecSpec.hs --- a/tests/VecSpec.hs +++ b/tests/VecSpec.hs @@ -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