eliminators 0.9 → 0.9.1

raw patch · 22 files changed

+77/−126 lines, 22 filesdep +textdep ~basedep ~template-haskelldep ~th-desugar

Dependencies added: text

Dependency ranges changed: base, template-haskell, th-desugar

Files

CHANGELOG.md +6/−0
eliminators.cabal +12/−10
src/Data/Eliminator.hs +0/−10
src/Data/Eliminator/Functor.hs +1/−5
src/Data/Eliminator/Monoid.hs +1/−5
src/Data/Eliminator/Semigroup.hs +1/−5
src/Data/Eliminator/TH.hs +1/−3
src/Data/Eliminator/TypeLits.hs +47/−0
src/Data/Eliminator/TypeNats.hs +8/−10
tests/DecideSpec.hs +0/−8
tests/DecideTypes.hs +0/−8
tests/EqualitySpec.hs +0/−7
tests/EqualityTypes.hs +0/−7
tests/GADTSpec.hs +0/−7
tests/Internal.hs +0/−1
tests/ListSpec.hs +0/−7
tests/ListTypes.hs +0/−4
tests/MatchabilizeSpec.hs +0/−5
tests/MatchabilizeTypes.hs +0/−4
tests/PolyRecTypes.hs +0/−7
tests/VecSpec.hs +0/−4
tests/VecTypes.hs +0/−9

CHANGELOG.md view

@@ -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`.

eliminators.cabal view

@@ -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

src/Data/Eliminator.hs view

@@ -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

src/Data/Eliminator/Functor.hs view

@@ -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

src/Data/Eliminator/Monoid.hs view

@@ -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

src/Data/Eliminator/Semigroup.hs view

@@ -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

src/Data/Eliminator/TH.hs view

@@ -1,7 +1,5 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TemplateHaskellQuotes #-} {-# LANGUAGE Unsafe #-} {-| Module:      Data.Eliminator.TH

+ src/Data/Eliminator/TypeLits.hs view

@@ -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))

src/Data/Eliminator/TypeNats.hs view

@@ -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))

tests/DecideSpec.hs view

@@ -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

tests/DecideTypes.hs view

@@ -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

tests/EqualitySpec.hs view

@@ -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

tests/EqualityTypes.hs view

@@ -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

tests/GADTSpec.hs view

@@ -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

tests/Internal.hs view

@@ -1,4 +1,3 @@-{-# LANGUAGE StandaloneKindSignatures #-} module Internal where  import Data.Kind

tests/ListSpec.hs view

@@ -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

tests/ListTypes.hs view

@@ -1,10 +1,6 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module ListTypes where

tests/MatchabilizeSpec.hs view

@@ -1,9 +1,4 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE StandaloneKindSignatures #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-} module MatchabilizeSpec where  import Data.Eliminator

tests/MatchabilizeTypes.hs view

@@ -1,9 +1,5 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -Wno-unused-foralls #-} module MatchabilizeTypes where

tests/PolyRecTypes.hs view

@@ -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

tests/VecSpec.hs view

@@ -1,10 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE NoStarIsType #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeOperators #-} module VecSpec where  import Data.Eliminator

tests/VecTypes.hs view

@@ -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