diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,9 @@ +### 0.9.1 [2022.08.23] +* Require GHC 9.4. +* Add `Data.Eliminator.TypeLits`, which re-exports + `Data.Eliminator.TypeNats.elimNat` and adds a new `elimSymbol` eliminator + for `GHC.TypeLits.Symbol`. + ## 0.9 [2021.10.31] * Require `singletons-base-3.1` and GHC 9.2. * Add `{e,E}limProxy` to `Data.Eliminator`. diff --git a/eliminators.cabal b/eliminators.cabal --- a/eliminators.cabal +++ b/eliminators.cabal @@ -1,5 +1,5 @@ name: eliminators -version: 0.9 +version: 0.9.1 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 @@ -16,7 +16,7 @@ build-type: Simple extra-source-files: CHANGELOG.md, README.md cabal-version: >=1.10 -tested-with: GHC == 9.2.1 +tested-with: GHC == 9.4.1 source-repository head type: git @@ -28,17 +28,19 @@ Data.Eliminator.Monoid Data.Eliminator.Semigroup Data.Eliminator.TH + Data.Eliminator.TypeLits Data.Eliminator.TypeNats - build-depends: base >= 4.16 && < 4.17 + build-depends: base >= 4.17 && < 4.18 , extra >= 1.4.2 && < 1.8 , singletons-base >= 3.1 && < 3.2 , singleton-nats >= 0.4.2 && < 0.5 - , template-haskell >= 2.18 && < 2.19 + , template-haskell >= 2.19 && < 2.20 + , text >= 2.0.1 && < 2.1 , th-abstraction >= 0.4 && < 0.5 - , th-desugar >= 1.13 && < 1.14 + , th-desugar >= 1.14 && < 1.15 hs-source-dirs: src - default-language: Haskell2010 - ghc-options: -Wall -Wcompat -Wno-unticked-promoted-constructors + default-language: GHC2021 + ghc-options: -Wall -Wcompat -Wno-unticked-promoted-constructors -fenable-th-splice-warnings test-suite spec type: exitcode-stdio-1.0 @@ -56,12 +58,12 @@ PolyRecTypes VecTypes VecSpec - build-depends: base >= 4.16 && < 4.17 + build-depends: base >= 4.17 && < 4.18 , eliminators , hspec >= 2 && < 3 , singletons-base >= 3.1 && < 3.2 , singleton-nats >= 0.4.2 && < 0.5 build-tool-depends: hspec-discover:hspec-discover hs-source-dirs: tests - default-language: Haskell2010 - ghc-options: -Wall -Wcompat -Wno-unticked-promoted-constructors -threaded -rtsopts + default-language: GHC2021 + ghc-options: -Wall -Wcompat -Wno-unticked-promoted-constructors -fenable-th-splice-warnings -threaded -rtsopts diff --git a/src/Data/Eliminator.hs b/src/Data/Eliminator.hs --- a/src/Data/Eliminator.hs +++ b/src/Data/Eliminator.hs @@ -1,18 +1,8 @@ {-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE EmptyCase #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE Trustworthy #-} -{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-| Module: Data.Eliminator diff --git a/src/Data/Eliminator/Functor.hs b/src/Data/Eliminator/Functor.hs --- a/src/Data/Eliminator/Functor.hs +++ b/src/Data/Eliminator/Functor.hs @@ -1,11 +1,7 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeFamilies #-} {-| Module: Data.Eliminator.Functor diff --git a/src/Data/Eliminator/Monoid.hs b/src/Data/Eliminator/Monoid.hs --- a/src/Data/Eliminator/Monoid.hs +++ b/src/Data/Eliminator/Monoid.hs @@ -1,11 +1,7 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeFamilies #-} {-| Module: Data.Eliminator.Monoid diff --git a/src/Data/Eliminator/Semigroup.hs b/src/Data/Eliminator/Semigroup.hs --- a/src/Data/Eliminator/Semigroup.hs +++ b/src/Data/Eliminator/Semigroup.hs @@ -1,11 +1,7 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeFamilies #-} {-| Module: Data.Eliminator.Semigroup diff --git a/src/Data/Eliminator/TH.hs b/src/Data/Eliminator/TH.hs --- a/src/Data/Eliminator/TH.hs +++ b/src/Data/Eliminator/TH.hs @@ -1,7 +1,5 @@ {-# LANGUAGE DataKinds #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TemplateHaskellQuotes #-} {-# LANGUAGE Unsafe #-} {-| Module: Data.Eliminator.TH diff --git a/src/Data/Eliminator/TypeLits.hs b/src/Data/Eliminator/TypeLits.hs new file mode 100644 --- /dev/null +++ b/src/Data/Eliminator/TypeLits.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE Trustworthy #-} +{-| +Module: Data.Eliminator.TypeLits +Copyright: (C) 2022 Ryan Scott +License: BSD-style (see the file LICENSE) +Maintainer: Ryan Scott +Stability: Experimental +Portability: GHC + +Crude imitations of eliminator functions for 'GHC.TypeLits.Nat' and +'GHC.TypeLits.Symbol'. +-} +module Data.Eliminator.TypeLits + ( elimNat + , elimSymbol + ) where + +import Data.Eliminator.TypeNats +import Data.Kind (Type) +import Data.Singletons +import qualified Data.Text as T + +import GHC.TypeLits.Singletons () +import GHC.TypeLits + +import Unsafe.Coerce (unsafeCoerce) + +-- | Although 'Nat' is not actually an inductive data type in GHC, we can +-- (crudely) pretend that it is using this eliminator. +elimSymbol :: forall (p :: Symbol ~> Type) (s :: Symbol). + Sing s + -> Apply p "" + -> (forall (c :: Char) (ss :: Symbol). + Sing c -> Sing ss -> Apply p ss -> + Apply p (ConsSymbol c ss)) + -> Apply p s +elimSymbol ssym pNil pCons = go @s ssym + where + go :: forall (s' :: Symbol). Sing s' -> Apply p s' + go ssym' = + case T.uncons (fromSing ssym') of + Nothing -> unsafeCoerce pNil + Just (c, ss) -> withSomeSing c $ \(sc :: Sing c) -> + withSomeSing ss $ \(sss :: Sing ss) -> + unsafeCoerce (pCons sc sss (go @ss sss)) diff --git a/src/Data/Eliminator/TypeNats.hs b/src/Data/Eliminator/TypeNats.hs --- a/src/Data/Eliminator/TypeNats.hs +++ b/src/Data/Eliminator/TypeNats.hs @@ -1,11 +1,6 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE Trustworthy #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeOperators #-} {-| Module: Data.Eliminator.TypeNats Copyright: (C) 2017 Ryan Scott @@ -33,8 +28,11 @@ -> Apply p 0 -> (forall (k :: Nat). Sing k -> Apply p k -> Apply p (k + 1)) -> Apply p n -elimNat snat pZ pS = - case fromSing snat of - 0 -> unsafeCoerce pZ - nPlusOne -> withSomeSing (pred nPlusOne) $ \(sn :: Sing k) -> - unsafeCoerce (pS sn (elimNat @p @k sn pZ pS)) +elimNat snat pZ pS = go @n snat + where + go :: forall (n' :: Nat). Sing n' -> Apply p n' + go snat' = + case fromSing snat' of + 0 -> unsafeCoerce pZ + nPlusOne -> withSomeSing (pred nPlusOne) $ \(sk :: Sing k) -> + unsafeCoerce (pS sk (go @k sk)) diff --git a/tests/DecideSpec.hs b/tests/DecideSpec.hs --- a/tests/DecideSpec.hs +++ b/tests/DecideSpec.hs @@ -1,12 +1,4 @@ {-# LANGUAGE DataKinds #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} module DecideSpec where import Data.Eliminator diff --git a/tests/DecideTypes.hs b/tests/DecideTypes.hs --- a/tests/DecideTypes.hs +++ b/tests/DecideTypes.hs @@ -1,15 +1,7 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-unused-foralls #-} module DecideTypes where diff --git a/tests/EqualitySpec.hs b/tests/EqualitySpec.hs --- a/tests/EqualitySpec.hs +++ b/tests/EqualitySpec.hs @@ -1,13 +1,6 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} module EqualitySpec where import Data.Kind diff --git a/tests/EqualityTypes.hs b/tests/EqualityTypes.hs --- a/tests/EqualityTypes.hs +++ b/tests/EqualityTypes.hs @@ -1,14 +1,7 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} module EqualityTypes where diff --git a/tests/GADTSpec.hs b/tests/GADTSpec.hs --- a/tests/GADTSpec.hs +++ b/tests/GADTSpec.hs @@ -1,14 +1,7 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module GADTSpec where diff --git a/tests/Internal.hs b/tests/Internal.hs --- a/tests/Internal.hs +++ b/tests/Internal.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE StandaloneKindSignatures #-} module Internal where import Data.Kind diff --git a/tests/ListSpec.hs b/tests/ListSpec.hs --- a/tests/ListSpec.hs +++ b/tests/ListSpec.hs @@ -1,12 +1,5 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} module ListSpec where import Data.Eliminator diff --git a/tests/ListTypes.hs b/tests/ListTypes.hs --- a/tests/ListTypes.hs +++ b/tests/ListTypes.hs @@ -1,10 +1,6 @@ {-# LANGUAGE DataKinds #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module ListTypes where diff --git a/tests/MatchabilizeSpec.hs b/tests/MatchabilizeSpec.hs --- a/tests/MatchabilizeSpec.hs +++ b/tests/MatchabilizeSpec.hs @@ -1,9 +1,4 @@ {-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE StandaloneKindSignatures #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} module MatchabilizeSpec where import Data.Eliminator diff --git a/tests/MatchabilizeTypes.hs b/tests/MatchabilizeTypes.hs --- a/tests/MatchabilizeTypes.hs +++ b/tests/MatchabilizeTypes.hs @@ -1,9 +1,5 @@ {-# LANGUAGE DataKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -Wno-unused-foralls #-} module MatchabilizeTypes where diff --git a/tests/PolyRecTypes.hs b/tests/PolyRecTypes.hs --- a/tests/PolyRecTypes.hs +++ b/tests/PolyRecTypes.hs @@ -1,14 +1,7 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module PolyRecTypes where diff --git a/tests/VecSpec.hs b/tests/VecSpec.hs --- a/tests/VecSpec.hs +++ b/tests/VecSpec.hs @@ -1,10 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE NoStarIsType #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeOperators #-} module VecSpec where import Data.Eliminator diff --git a/tests/VecTypes.hs b/tests/VecTypes.hs --- a/tests/VecTypes.hs +++ b/tests/VecTypes.hs @@ -1,17 +1,8 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE EmptyCase #-} -{-# LANGUAGE GADTs #-} {-# LANGUAGE NoStarIsType #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module VecTypes where