sop-core (empty) → 0.4.0.0
raw patch · 13 files changed
+4028/−0 lines, 13 filesdep +basedep +deepseqsetup-changed
Dependencies added: base, deepseq
Files
- CHANGELOG.md +263/−0
- LICENSE +27/−0
- Setup.hs +2/−0
- doctest.sh +24/−0
- sop-core.cabal +76/−0
- src/Data/SOP.hs +151/−0
- src/Data/SOP/BasicFunctors.hs +376/−0
- src/Data/SOP/Classes.hs +678/−0
- src/Data/SOP/Constraint.hs +281/−0
- src/Data/SOP/Dict.hs +159/−0
- src/Data/SOP/NP.hs +900/−0
- src/Data/SOP/NS.hs +980/−0
- src/Data/SOP/Sing.hs +111/−0
+ CHANGELOG.md view
@@ -0,0 +1,263 @@+# 0.4.0.0 (2018-10-20)++* Split into `sop-core` and `generics-sop` packages.++* Drop support for GHC < 8.0.2, bump `base` dependency+ to `>= 4.9` and remove dependency on `transformers`.++* Simplify `All2 c` to `All (All c)` and simplify+ `SListI xs` to `All Top xs`, and some implied+ refactoring.++* Add `Semigroup` and `Monoid` instances for various+ datatypes.++# 0.3.2.0 (2018-01-08)++* Make TH `deriveGenericFunctions` work properly with+ parameterized types (note that the more widely used+ `deriveGeneric` was already working correctly).++* Make TH `deriveGeneric` work properly with empty+ types.++* Add `compare_NS`, `ccompare_NS`, `compare_SOP`, and+ `ccompare_SOP` to better support comparison of sum+ structures.++* Add `hctraverse_` and `hctraverse'` as well as their+ unconstrained variants and a number of derived functions,+ to support effectful traversals.++# 0.3.1.0 (2017-06-11)++* Add `AllZip`, `htrans`, `hcoerce`, `hfromI`, `htoI`.+ These functions are for converting between related+ structures that do not have common signatures.++ The most common application of these functions seems+ to be the scenario where a datatype has components+ that are all wrapped in a common type constructor+ application, e.g. a datatype where every component+ is a `Maybe`. Then we can use `hfromI` after `from`+ to turn the generically derived `SOP` of `I`s into+ an `SOP` of `Maybe`s (and back).++* Add `IsProductType`, `IsEnumType`, `IsWrappedType`+ and `IsNewtype` constraint synonyms capturing+ specific classes of datypes.++# 0.3.0.0 (2017-04-29)++* No longer compatible with GHC 7.6, due to the lack of+ support for type-level literals.++* Support type-level metadata. This is provided by the+ `Generics.SOP.Type.Metadata` module. The two modules+ `Generics.SOP.Metadata` and `Generics.SOP.Type.Metadata`+ export nearly the same names, so for backwards compatibility,+ we keep exporting `Generics.SOP.Metadata` directly from+ `Generics.SOP`, whereas `Generics.SOP.Type.Metadata` is+ supposed to be imported explicitly (and qualified).++ Term-level metadata is still available, but is now usually+ computed automatically from the type-level metadata which+ contains the same information, using the function+ `demoteDatatypeInfo`. Term-level metadata is unchanged+ from generics-sop-0.2, so in most cases, even if your+ code makes use of metadata, you should not need to change+ anything.++ If you use TH deriving, then both type-level metadata and+ term-level metadata is generated for you automatically,+ for all supported GHC versions.++ If you use GGP deriving, then type-level metadata is+ available if you use GHC 8.0 or newer. If you use GHC 7.x,+ then GHC.Generics supports only term-level metadata, so+ we cannot translate that into type-level metadata. In+ this combination, you cannot use code that relies on+ type-level metadata, so you should either upgrade GHC or+ switch to TH-based deriving.++# 0.2.5.0 (2017-04-21)++* GHC 8.2 compatibility.++* Make `:.:` an instance of `Applicative`, `Foldable` and+ `Traversable`.++* Add functions `apInjs'_NP` and `apInjs'_POP`. These are+ variants of `apInjs_NP` and `apInjs'_POP` that return their+ result as an n-ary product, rather than collapsing it into+ a list.++* Add `hexpand` (and `expand_NS` and `expand_SOP`). These+ functions expand sums into products, given a default value+ to fill the other slots.++* Add utility functions such as `mapII` or `mapIK` that lift+ functions into different combinations of identity and+ constant functors.++* Add `NFData` (and lifted variants) instances for basic functors,+ products and sums.++# 0.2.4.0 (2017-02-02)++* Add `hindex` (and `index_NS` and `index_SOP`).++* Add `hapInjs` as a generalization of `apInjs_NP` and `apInjs_POP`.++* Make basic functors instances of lifted classes (such as `Eq1` etc).++# 0.2.3.0 (2016-12-04)++* Add various metadata getters++* Add `hdicts`.++* Add catamorphisms and anamorphisms for `NP` and `NS`.++* TH compatibility changes for GHC 8.1 (master).++# 0.2.2.0 (2016-07-10)++* Introduced `unZ` to destruct a unary sum.++* Add Haddock `@since` annotations for various functions.++# 0.2.1.0 (2016-02-08)++* Now includes a CHANGELOG.++* Should now work with ghc-8.0.1-rc1 and -rc2 (thanks to+ Oleg Grenrus).++* Introduced `hd` and `tl` to project out of a product, and+ `Projection` and `projections` as duals of `Injection` and+ `injections`.++# 0.2.0.0 (2015-10-23)++* Now tested with ghc-7.10++* Introduced names `hmap`, `hcmap`, `hzipWith`, `hczipWith` for+ `hliftA`, `hcliftA`, `hliftA2`, `hcliftA2`, respectively.+ Similarly for the specialized versions of these functions.++* The constraint transformers `All` and `All2` are now defined+ as type classes, not type families. As a consequence, the+ partial applications `All c` and `All2 c` are now possible.++* Because of the redefinition of `All` and `All2`, some special+ cases are no longer necessary. For example, `cpure_POP` can+ now be implemented as a nested application of `pure_NP`.++* Because of the redefinition of `All` and `All2`, the functions+ `hcliftA'` and variants (with prime!) are now deprecated.+ One can easily use the normal versions instead.+ For example, the definition of `hcliftA'` is now simply++ hcliftA' p = hcliftA (allP p)+ where+ allP :: proxy c -> Proxy (All c)+ allP _ = Proxy++* Because `All` and `All2` are now type classes, they now have+ superclass constraints implying that the type-level lists they+ are ranging over must have singletons.++ class (SListI xs, ...) => All c xs+ class (SListI xss, ...) => All2 c xss++ Some type signatures can be simplified due to this.++* The `SingI` typeclass and `Sing` datatypes are now deprecated.+ The replacements are called `SListI` and `SList`.+ The `sing` method is now called `sList`. The difference+ is that the new versions reveal only the spine of the list, and+ contain no singleton representation for the elements anymore.++ For one-dimensional type-level lists, replace++ SingI xs => ...++ by++ SListI xs => ...++ For two-dimensional type-level lists, replace++ SingI xss => ...++ by++ All SListI xss => ...++ Because All itself implies `SListI xss` (see above), this+ constraint is equivalent to the old `Sing xss`.++ The old names are provided for (limited) backward+ compatibility. They map to the new constructs. This will+ work in some, but not all scenarios.++ The function `lengthSing` has also been renamed to+ `lengthSList` for consistency, and the old name is+ deprecated.++* All `Proxy c` arguments have been replaced by `proxy c`+ flexible arguments, so that other type constructors can be+ used as proxies.++* Class-level composition (`Compose`), pairing (`And`), and+ a trivial constraint (`Top`) have been added. Type-level map+ (`Map`) has been removed. Occurrences such as++ All c (Map f xs)++ should now be replaced with++ All (c `Compose` f) xs++* There is a new module called `Generics.SOP.Dict` that contains+ functions for manipulating dictionaries explicitly. These can+ be used to prove theorems about non-trivial class constraints+ such as the ones that get built using `All` and `All2`. Some+ such theorems are provided.++* There is a new TH function `deriveGenericFunctions` that+ derives the code of a datatype and conversion functions, but+ does not create a class instance. (Contributed by Oleg Grenrus.)++* There is a new TH function `deriveMetadataValue` that+ derives a `DatatypeInfo` value for a datatype, but does+ not create an instance of `HasDatatypeInfo`. (Contributed by+ Oleg Grenrus.)++* There is a very simple example file. (Contributed by Oleg+ Grenrus.)++* The function `hcollapse` for `NS` now results in an `a` rather+ than an `I a`, matching the specialized version `collapse_NS`.+ (Suggested by Roman Cheplyaka.)++# 0.1.1.2 (2015-03-27)++* Updated version bounds for ghc-prim (for ghc-7.10).++# 0.1.1.1 (2015-03-20)++* Preparations for ghc-7.10.++* Documentation fix. (Contributed by Roman Cheplyaka.)++# 0.1.1 (2015-01-06)++* Documentation fixes.++* Add superclass constraint (TODO).++* Now derive tuple instance for tuples up to 30 components.+ (Contributed by Michael Orlitzky.)+
+ LICENSE view
@@ -0,0 +1,27 @@+Copyright (c) 2014-2015, Well-Typed LLP, Edsko de Vries, Andres Löh+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyright notice,+ this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright notice,+ this list of conditions and the following disclaimer in the documentation+ and/or other materials provided with the distribution.++3. Neither the name of the copyright holder nor the names of its contributors+ may be used to endorse or promote products derived from this software+ without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ doctest.sh view
@@ -0,0 +1,24 @@+#!/bin/sh++set -ex++doctest --preserve-it \+ -XCPP \+ -XScopedTypeVariables \+ -XTypeFamilies \+ -XRankNTypes \+ -XTypeOperators \+ -XGADTs \+ -XConstraintKinds \+ -XMultiParamTypeClasses \+ -XTypeSynonymInstances \+ -XFlexibleInstances \+ -XFlexibleContexts \+ -XDeriveFunctor \+ -XDeriveFoldable \+ -XDeriveTraversable \+ -XDefaultSignatures \+ -XKindSignatures \+ -XDataKinds \+ -XFunctionalDependencies \+ $(find src -name '*.hs')
+ sop-core.cabal view
@@ -0,0 +1,76 @@+name: sop-core+version: 0.4.0.0+synopsis: True Sums of Products+description:+ Implementation of n-ary sums and n-ary products.+ .+ The module "Data.SOP" is the main module of this library and contains+ more detailed documentation.+ .+ The main use case of this package is to serve as the core of+ @<https://hackage.haskell.org/package/generics-sop generics-sop>@.+ .+ A detailed description of the ideas behind this library is provided by+ the paper:+ .+ * Edsko de Vries and Andres Löh.+ <http://www.andres-loeh.de/TrueSumsOfProducts True Sums of Products>.+ Workshop on Generic Programming (WGP) 2014.+ .+license: BSD3+license-file: LICENSE+author: Edsko de Vries <edsko@well-typed.com>, Andres Löh <andres@well-typed.com>+maintainer: andres@well-typed.com+category: Data+build-type: Simple+cabal-version: >=1.10+extra-source-files: CHANGELOG.md doctest.sh+tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3, GHC == 8.6.1++source-repository head+ type: git+ location: https://github.com/well-typed/generics-sop++library+ exposed-modules: Data.SOP+ Data.SOP.Dict+ -- exposed via Data.SOP:+ Data.SOP.BasicFunctors+ Data.SOP.Classes+ Data.SOP.Constraint+ Data.SOP.NP+ Data.SOP.NS+ Data.SOP.Sing+ build-depends: base >= 4.9 && < 5,+ deepseq >= 1.3 && < 1.5+ hs-source-dirs: src+ default-language: Haskell2010+ ghc-options: -Wall+ default-extensions: CPP+ ScopedTypeVariables+ TypeFamilies+ RankNTypes+ TypeOperators+ GADTs+ ConstraintKinds+ MultiParamTypeClasses+ TypeSynonymInstances+ FlexibleInstances+ FlexibleContexts+ DeriveFunctor+ DeriveFoldable+ DeriveTraversable+ DefaultSignatures+ KindSignatures+ DataKinds+ FunctionalDependencies+ AutoDeriveTypeable+ -- if impl(ghc >= 8.6)+ -- default-extensions: NoStarIsType+ other-extensions: PolyKinds+ UndecidableInstances+ DeriveGeneric+ StandaloneDeriving+ EmptyCase+ UndecidableSuperClasses+ BangPatterns
+ src/Data/SOP.hs view
@@ -0,0 +1,151 @@+{-# LANGUAGE PolyKinds, UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-unused-binds #-}+-- | Main module of @sop-core@+module Data.SOP (+ -- * n-ary datatypes+ NP(..)+ , NS(..)+ , SOP(..)+ , unSOP+ , POP(..)+ , unPOP+ -- * Combinators+ -- ** Constructing products+ , HPure(..)+ -- ** Destructing products+ , hd+ , tl+ , Projection+ , projections+ , shiftProjection+ -- ** Application+ , type (-.->)(..)+ , fn+ , fn_2+ , fn_3+ , fn_4+ , Prod+ , HAp(..)+ -- ** Lifting / mapping+ , hliftA+ , hliftA2+ , hliftA3+ , hcliftA+ , hcliftA2+ , hcliftA3+ , hmap+ , hzipWith+ , hzipWith3+ , hcmap+ , hczipWith+ , hczipWith3+ -- ** Constructing sums+ , Injection+ , injections+ , shift+ , shiftInjection+ , UnProd+ , HApInjs(..)+ , apInjs_NP -- deprecated export+ , apInjs_POP -- deprecated export+ -- ** Destructing sums+ , unZ+ , HIndex(..)+ -- ** Dealing with @'All' c@+ , hcliftA'+ , hcliftA2'+ , hcliftA3'+ -- ** Comparison+ , compare_NS+ , ccompare_NS+ , compare_SOP+ , ccompare_SOP+ -- ** Collapsing+ , CollapseTo+ , HCollapse(..)+ -- ** Folding and sequencing+ , HTraverse_(..)+ , hcfoldMap+ , hcfor_+ , HSequence(..)+ , hsequence+ , hsequenceK+ , hctraverse+ , hcfor+ -- ** Expanding sums to products+ , HExpand(..)+ -- ** Transformation of index lists and coercions+ , HTrans(..)+ , hfromI+ , htoI+ -- ** Partial operations+ , fromList+ -- * Utilities+ -- ** Basic functors+ , K(..)+ , unK+ , I(..)+ , unI+ , (:.:)(..)+ , unComp+ -- *** Mapping functions+ , mapII+ , mapIK+ , mapKI+ , mapKK+ , mapIII+ , mapIIK+ , mapIKI+ , mapIKK+ , mapKII+ , mapKIK+ , mapKKI+ , mapKKK+ -- ** Mapping constraints+ , All+ , All2+ , cpara_SList+ , ccase_SList+ , AllZip+ , AllZip2+ , AllN+ , AllZipN+ -- ** Other constraints+ , Compose+ , And+ , Top+ , LiftedCoercible+ , SameShapeAs+ -- ** Singletons+ , SList(..)+ , SListI+ , SListI2+ , sList+ , para_SList+ , case_SList+ -- *** Shape of type-level lists+ , Shape(..)+ , shape+ , lengthSList+ -- ** Re-exports++-- Workaround for lack of MIN_TOOL_VERSION macro in Cabal 1.18, see:+-- https://github.com/well-typed/generics-sop/issues/3+#ifndef MIN_TOOL_VERSION_haddock+#define MIN_TOOL_VERSION_haddock(x,y,z) 0+#endif++#if !(defined(__HADDOCK_VERSION__)) || MIN_TOOL_VERSION_haddock(2,14,0)+ , Proxy(..) -- hidden from old Haddock versions, because it triggers an internal error+#endif+ ) where++import Data.Proxy (Proxy(..))++import Data.SOP.BasicFunctors+import Data.SOP.Classes+import Data.SOP.Constraint+import Data.SOP.NP+import Data.SOP.NS+import Data.SOP.Sing+
+ src/Data/SOP/BasicFunctors.hs view
@@ -0,0 +1,376 @@+{-# LANGUAGE PolyKinds, DeriveGeneric #-}+-- | Basic functors.+--+-- Definitions of the type-level equivalents of+-- 'const', 'id', and ('.'), and a definition of+-- the lifted function space.+--+-- These datatypes are generally useful, but in this+-- library, they're primarily used as parameters for+-- the 'NP', 'NS', 'POP', and 'SOP' types.+--+-- We define own variants of 'Control.Applicative.Const',+-- 'Data.Functor.Identity.Identity' and 'Data.Functor.Compose.Compose' for+-- various reasons.+--+-- * 'Control.Applicative.Const' and 'Data.Functor.Compose.Compose' become+-- kind polymorphic only in @base-4.9.0.0@ (@transformers-0.5.0.0@).+--+-- * Shorter names are convenient, and pattern synonyms aren't+-- (yet) powerful enough, particularly exhaustiveness check doesn't work+-- properly. See <https://ghc.haskell.org/trac/ghc/ticket/8779>.+--+module Data.SOP.BasicFunctors+ ( -- * Basic functors+ K(..)+ , unK+ , I(..)+ , unI+ , (:.:)(..)+ , unComp+ -- * Mapping functions+ , mapII+ , mapIK+ , mapKI+ , mapKK+ , mapIII+ , mapIIK+ , mapIKI+ , mapIKK+ , mapKII+ , mapKIK+ , mapKKI+ , mapKKK+ ) where++import Data.Semigroup (Semigroup (..))+import Data.Kind (Type)+import qualified GHC.Generics as GHC++import Data.Functor.Classes++import Control.DeepSeq (NFData(..))+#if MIN_VERSION_deepseq(1,4,3)+import Control.DeepSeq (NFData1(..), NFData2(..))+#endif++-- * Basic functors++-- | The constant type functor.+--+-- Like 'Data.Functor.Constant.Constant', but kind-polymorphic+-- in its second argument and with a shorter name.+--+newtype K (a :: Type) (b :: k) = K a+ deriving (Functor, Foldable, Traversable, GHC.Generic)++-- | @since 0.2.4.0+instance Eq2 K where+ liftEq2 eq _ (K x) (K y) = eq x y+-- | @since 0.2.4.0+instance Ord2 K where+ liftCompare2 comp _ (K x) (K y) = comp x y+-- | @since 0.2.4.0+instance Read2 K where+ liftReadsPrec2 rp _ _ _ = readsData $+ readsUnaryWith rp "K" K+-- | @since 0.2.4.0+instance Show2 K where+ liftShowsPrec2 sp _ _ _ d (K x) = showsUnaryWith sp "K" d x++-- | @since 0.2.4.0+instance (Eq a) => Eq1 (K a) where+ liftEq = liftEq2 (==)+-- | @since 0.2.4.0+instance (Ord a) => Ord1 (K a) where+ liftCompare = liftCompare2 compare+-- | @since 0.2.4.0+instance (Read a) => Read1 (K a) where+ liftReadsPrec = liftReadsPrec2 readsPrec readList+-- | @since 0.2.4.0+instance (Show a) => Show1 (K a) where+ liftShowsPrec = liftShowsPrec2 showsPrec showList++-- This have to be implemented manually, K is polykinded.+instance (Eq a) => Eq (K a b) where+ K x == K y = x == y+instance (Ord a) => Ord (K a b) where+ compare (K x) (K y) = compare x y+instance (Read a) => Read (K a b) where+ readsPrec = readsData $ readsUnaryWith readsPrec "K" K+instance (Show a) => Show (K a b) where+ showsPrec d (K x) = showsUnaryWith showsPrec "K" d x++-- | @since 0.4.0.0+instance Semigroup a => Semigroup (K a b) where+ K x <> K y = K (x <> y)++-- | @since 0.4.0.0+instance Monoid a => Monoid (K a b) where+ mempty = K mempty+ mappend (K x) (K y) = K (mappend x y)++instance Monoid a => Applicative (K a) where+ pure _ = K mempty+ K x <*> K y = K (mappend x y)++-- | Extract the contents of a 'K' value.+unK :: K a b -> a+unK (K x) = x++-- | The identity type functor.+--+-- Like 'Data.Functor.Identity.Identity', but with a shorter name.+--+newtype I (a :: Type) = I a+ deriving (Functor, Foldable, Traversable, GHC.Generic)++-- | @since 0.4.0.0+instance Semigroup a => Semigroup (I a) where+ I x <> I y = I (x <> y)++-- | @since 0.4.0.0+instance Monoid a => Monoid (I a) where+ mempty = I mempty+ mappend (I x) (I y) = I (mappend x y)++instance Applicative I where+ pure = I+ I f <*> I x = I (f x)++instance Monad I where+ return = I+ I x >>= f = f x+++-- | @since 0.2.4.0+instance Eq1 I where+ liftEq eq (I x) (I y) = eq x y+-- | @since 0.2.4.0+instance Ord1 I where+ liftCompare comp (I x) (I y) = comp x y+-- | @since 0.2.4.0+instance Read1 I where+ liftReadsPrec rp _ = readsData $+ readsUnaryWith rp "I" I+-- | @since 0.2.4.0+instance Show1 I where+ liftShowsPrec sp _ d (I x) = showsUnaryWith sp "I" d x++instance (Eq a) => Eq (I a) where (==) = eq1+instance (Ord a) => Ord (I a) where compare = compare1+instance (Read a) => Read (I a) where readsPrec = readsPrec1+instance (Show a) => Show (I a) where showsPrec = showsPrec1++-- | Extract the contents of an 'I' value.+unI :: I a -> a+unI (I x) = x++-- | Composition of functors.+--+-- Like 'Data.Functor.Compose.Compose', but kind-polymorphic+-- and with a shorter name.+--+newtype (:.:) (f :: l -> Type) (g :: k -> l) (p :: k) = Comp (f (g p))+ deriving (GHC.Generic)++infixr 7 :.:++-- | @since 0.4.0.0+instance (Semigroup (f (g x))) => Semigroup ((f :.: g) x) where+ Comp x <> Comp y = Comp (x <> y)++-- | @since 0.4.0.0+instance (Monoid (f (g x))) => Monoid ((f :.: g) x) where+ mempty = Comp mempty+ mappend (Comp x) (Comp y) = Comp (mappend x y)++instance (Functor f, Functor g) => Functor (f :.: g) where+ fmap f (Comp x) = Comp (fmap (fmap f) x)++-- | @since 0.2.5.0+instance (Applicative f, Applicative g) => Applicative (f :.: g) where+ pure x = Comp (pure (pure x))+ Comp f <*> Comp x = Comp ((<*>) <$> f <*> x)++-- | @since 0.2.5.0+instance (Foldable f, Foldable g) => Foldable (f :.: g) where+ foldMap f (Comp t) = foldMap (foldMap f) t++-- | @since 0.2.5.0+instance (Traversable f, Traversable g) => Traversable (f :.: g) where+ traverse f (Comp t) = Comp <$> traverse (traverse f) t+++-- Instances of lifted Prelude classes++-- | @since 0.2.4.0+instance (Eq1 f, Eq1 g) => Eq1 (f :.: g) where+ liftEq eq (Comp x) (Comp y) = liftEq (liftEq eq) x y++-- | @since 0.2.4.0+instance (Ord1 f, Ord1 g) => Ord1 (f :.: g) where+ liftCompare comp (Comp x) (Comp y) =+ liftCompare (liftCompare comp) x y++-- | @since 0.2.4.0+instance (Read1 f, Read1 g) => Read1 (f :.: g) where+ liftReadsPrec rp rl = readsData $+ readsUnaryWith (liftReadsPrec rp' rl') "Comp" Comp+ where+ rp' = liftReadsPrec rp rl+ rl' = liftReadList rp rl++-- | @since 0.2.4.0+instance (Show1 f, Show1 g) => Show1 (f :.: g) where+ liftShowsPrec sp sl d (Comp x) =+ showsUnaryWith (liftShowsPrec sp' sl') "Comp" d x+ where+ sp' = liftShowsPrec sp sl+ sl' = liftShowList sp sl++instance (Eq1 f, Eq1 g, Eq a) => Eq ((f :.: g) a) where (==) = eq1+instance (Ord1 f, Ord1 g, Ord a) => Ord ((f :.: g) a) where compare = compare1+instance (Read1 f, Read1 g, Read a) => Read ((f :.: g) a) where readsPrec = readsPrec1+instance (Show1 f, Show1 g, Show a) => Show ((f :.: g) a) where showsPrec = showsPrec1++-- NFData Instances++-- | @since 0.2.5.0+instance NFData a => NFData (I a) where+ rnf (I x) = rnf x++-- | @since 0.2.5.0+instance NFData a => NFData (K a b) where+ rnf (K x) = rnf x++-- | @since 0.2.5.0+instance NFData (f (g a)) => NFData ((f :.: g) a) where+ rnf (Comp x) = rnf x++#if MIN_VERSION_deepseq(1,4,3)+-- | @since 0.2.5.0+instance NFData1 I where+ liftRnf r (I x) = r x++-- | @since 0.2.5.0+instance NFData a => NFData1 (K a) where+ liftRnf _ (K x) = rnf x++-- | @since 0.2.5.0+instance NFData2 K where+ liftRnf2 r _ (K x) = r x++-- | @since 0.2.5.0+instance (NFData1 f, NFData1 g) => NFData1 (f :.: g) where+ liftRnf r (Comp x) = liftRnf (liftRnf r) x+#endif++-- | Extract the contents of a 'Comp' value.+unComp :: (f :.: g) p -> f (g p)+unComp (Comp x) = x++-- * Mapping functions++-- Implementation note:+--+-- All of these functions are just type specializations of+-- 'coerce'. However, we currently still support GHC 7.6+-- which does not support 'coerce', so we write them+-- explicitly.++-- | Lift the given function.+--+-- @since 0.2.5.0+--+mapII :: (a -> b) -> I a -> I b+mapII = \ f (I a) -> I (f a)+{-# INLINE mapII #-}++-- | Lift the given function.+--+-- @since 0.2.5.0+--+mapIK :: (a -> b) -> I a -> K b c+mapIK = \ f (I a) -> K (f a)+{-# INLINE mapIK #-}++-- | Lift the given function.+--+-- @since 0.2.5.0+--+mapKI :: (a -> b) -> K a c -> I b+mapKI = \ f (K a) -> I (f a)+{-# INLINE mapKI #-}++-- | Lift the given function.+--+-- @since 0.2.5.0+--+mapKK :: (a -> b) -> K a c -> K b d+mapKK = \ f (K a) -> K (f a)+{-# INLINE mapKK #-}++-- | Lift the given function.+--+-- @since 0.2.5.0+--+mapIII :: (a -> b -> c) -> I a -> I b -> I c+mapIII = \ f (I a) (I b) -> I (f a b)+{-# INLINE mapIII #-}++-- | Lift the given function.+--+-- @since 0.2.5.0+--+mapIIK :: (a -> b -> c) -> I a -> I b -> K c d+mapIIK = \ f (I a) (I b) -> K (f a b)+{-# INLINE mapIIK #-}++-- | Lift the given function.+--+-- @since 0.2.5.0+--+mapIKI :: (a -> b -> c) -> I a -> K b d -> I c+mapIKI = \ f (I a) (K b) -> I (f a b)+{-# INLINE mapIKI #-}++-- | Lift the given function.+--+-- @since 0.2.5.0+--+mapIKK :: (a -> b -> c) -> I a -> K b d -> K c e+mapIKK = \ f (I a) (K b) -> K (f a b)+{-# INLINE mapIKK #-}++-- | Lift the given function.+--+-- @since 0.2.5.0+--+mapKII :: (a -> b -> c) -> K a d -> I b -> I c+mapKII = \ f (K a) (I b) -> I (f a b)+{-# INLINE mapKII #-}++-- | Lift the given function.+--+-- @since 0.2.5.0+--+mapKIK :: (a -> b -> c) -> K a d -> I b -> K c e+mapKIK = \ f (K a) (I b) -> K (f a b)+{-# INLINE mapKIK #-}++-- | Lift the given function.+--+-- @since 0.2.5.0+--+mapKKI :: (a -> b -> c) -> K a d -> K b e -> I c+mapKKI = \ f (K a) (K b) -> I (f a b)+{-# INLINE mapKKI #-}++-- | Lift the given function.+--+-- @since 0.2.5.0+--+mapKKK :: (a -> b -> c) -> K a d -> K b e -> K c f+mapKKK = \ f (K a) (K b) -> K (f a b)+{-# INLINE mapKKK #-}
+ src/Data/SOP/Classes.hs view
@@ -0,0 +1,678 @@+{-# LANGUAGE PolyKinds #-}+-- | Classes for generalized combinators on SOP types.+--+-- In the SOP approach to generic programming, we're predominantly+-- concerned with four structured datatypes:+--+-- @+-- 'Data.SOP.NP.NP' :: (k -> 'Type') -> ( [k] -> 'Type') -- n-ary product+-- 'Data.SOP.NS.NS' :: (k -> 'Type') -> ( [k] -> 'Type') -- n-ary sum+-- 'Data.SOP.NP.POP' :: (k -> 'Type') -> ([[k]] -> 'Type') -- product of products+-- 'Data.SOP.NS.SOP' :: (k -> 'Type') -> ([[k]] -> 'Type') -- sum of products+-- @+--+-- All of these have a kind that fits the following pattern:+--+-- @+-- (k -> 'Type') -> (l -> 'Type')+-- @+--+-- These four types support similar interfaces. In order to allow+-- reusing the same combinator names for all of these types, we define+-- various classes in this module that allow the necessary+-- generalization.+--+-- The classes typically lift concepts that exist for kinds @'Type'@ or+-- @'Type' -> 'Type'@ to datatypes of kind @(k -> 'Type') -> (l -> 'Type')@. This module+-- also derives a number of derived combinators.+--+-- The actual instances are defined in "Data.SOP.NP" and+-- "Data.SOP.NS".+--+module Data.SOP.Classes+ ( -- * Generalized applicative functor structure+ -- ** Generalized 'Control.Applicative.pure'+ HPure(..)+ -- ** Generalized 'Control.Applicative.<*>'+ , type (-.->)(..)+ , fn+ , fn_2+ , fn_3+ , fn_4+ , Same+ , Prod+ , HAp(..)+ -- ** Derived functions+ , hliftA+ , hliftA2+ , hliftA3+ , hmap+ , hzipWith+ , hzipWith3+ , hcliftA+ , hcliftA2+ , hcliftA3+ , hcmap+ , hczipWith+ , hczipWith3+ -- * Collapsing homogeneous structures+ , CollapseTo+ , HCollapse(..)+ -- * Folding and sequencing+ , HTraverse_(..)+ , HSequence(..)+ -- ** Derived functions+ , hcfoldMap+ , hcfor_+ , hsequence+ , hsequenceK+ , hctraverse+ , hcfor+ -- * Indexing into sums+ , HIndex(..)+ -- * Applying all injections+ , UnProd+ , HApInjs(..)+ -- * Expanding sums to products+ , HExpand(..)+ -- * Transformation of index lists and coercions+ , HTrans(..)+ , hfromI+ , htoI+ ) where++import Data.Kind (Type)+import Data.SOP.BasicFunctors+import Data.SOP.Constraint++-- * Generalized applicative functor structure++-- ** Generalized 'Control.Applicative.pure'++-- | A generalization of 'Control.Applicative.pure' or+-- 'Control.Monad.return' to higher kinds.+class HPure (h :: (k -> Type) -> (l -> Type)) where+ -- | Corresponds to 'Control.Applicative.pure' directly.+ --+ -- /Instances:/+ --+ -- @+ -- 'hpure', 'Data.SOP.NP.pure_NP' :: 'Data.SOP.Sing.SListI' xs => (forall a. f a) -> 'Data.SOP.NP.NP' f xs+ -- 'hpure', 'Data.SOP.NP.pure_POP' :: 'SListI2' xss => (forall a. f a) -> 'Data.SOP.NP.POP' f xss+ -- @+ --+ hpure :: SListIN h xs => (forall a. f a) -> h f xs++ -- | A variant of 'hpure' that allows passing in a constrained+ -- argument.+ --+ -- Calling @'hcpure' f s@ where @s :: h f xs@ causes @f@ to be+ -- applied at all the types that are contained in @xs@. Therefore,+ -- the constraint @c@ has to be satisfied for all elements of @xs@,+ -- which is what @'AllN' h c xs@ states.+ --+ -- /Instances:/+ --+ -- @+ -- 'hcpure', 'Data.SOP.NP.cpure_NP' :: ('All' c xs ) => proxy c -> (forall a. c a => f a) -> 'Data.SOP.NP.NP' f xs+ -- 'hcpure', 'Data.SOP.NP.cpure_POP' :: ('All2' c xss) => proxy c -> (forall a. c a => f a) -> 'Data.SOP.NP.POP' f xss+ -- @+ --+ hcpure :: (AllN h c xs) => proxy c -> (forall a. c a => f a) -> h f xs++-- ** Generalized 'Control.Applicative.<*>'++-- | Lifted functions.+newtype (f -.-> g) a = Fn { apFn :: f a -> g a }+infixr 1 -.->++-- | Construct a lifted function.+--+-- Same as 'Fn'. Only available for uniformity with the+-- higher-arity versions.+--+fn :: (f a -> f' a) -> (f -.-> f') a++-- | Construct a binary lifted function.+fn_2 :: (f a -> f' a -> f'' a) -> (f -.-> f' -.-> f'') a++-- | Construct a ternary lifted function.+fn_3 :: (f a -> f' a -> f'' a -> f''' a) -> (f -.-> f' -.-> f'' -.-> f''') a++-- | Construct a quarternary lifted function.+fn_4 :: (f a -> f' a -> f'' a -> f''' a -> f'''' a) -> (f -.-> f' -.-> f'' -.-> f''' -.-> f'''') a++fn f = Fn $ \x -> f x+fn_2 f = Fn $ \x -> Fn $ \x' -> f x x'+fn_3 f = Fn $ \x -> Fn $ \x' -> Fn $ \x'' -> f x x' x''+fn_4 f = Fn $ \x -> Fn $ \x' -> Fn $ \x'' -> Fn $ \x''' -> f x x' x'' x'''++-- | Maps a structure to the same structure.+type family Same (h :: (k1 -> Type) -> (l1 -> Type)) :: (k2 -> Type) -> (l2 -> Type)++-- | Maps a structure containing sums to the corresponding+-- product structure.+type family Prod (h :: (k -> Type) -> (l -> Type)) :: (k -> Type) -> (l -> Type)++-- | A generalization of 'Control.Applicative.<*>'.+class (Prod (Prod h) ~ Prod h, HPure (Prod h)) => HAp (h :: (k -> Type) -> (l -> Type)) where++ -- | Corresponds to 'Control.Applicative.<*>'.+ --+ -- For products ('Data.SOP.NP.NP') as well as products of products+ -- ('Data.SOP.NP.POP'), the correspondence is rather direct. We combine+ -- a structure containing (lifted) functions and a compatible structure+ -- containing corresponding arguments into a compatible structure+ -- containing results.+ --+ -- The same combinator can also be used to combine a product+ -- structure of functions with a sum structure of arguments, which then+ -- results in another sum structure of results. The sum structure+ -- determines which part of the product structure will be used.+ --+ -- /Instances:/+ --+ -- @+ -- 'hap', 'Data.SOP.NP.ap_NP' :: 'Data.SOP.NP.NP' (f -.-> g) xs -> 'Data.SOP.NP.NP' f xs -> 'Data.SOP.NP.NP' g xs+ -- 'hap', 'Data.SOP.NS.ap_NS' :: 'Data.SOP.NS.NP' (f -.-> g) xs -> 'Data.SOP.NS.NS' f xs -> 'Data.SOP.NS.NS' g xs+ -- 'hap', 'Data.SOP.NP.ap_POP' :: 'Data.SOP.NP.POP' (f -.-> g) xss -> 'Data.SOP.NP.POP' f xss -> 'Data.SOP.NP.POP' g xss+ -- 'hap', 'Data.SOP.NS.ap_SOP' :: 'Data.SOP.NS.POP' (f -.-> g) xss -> 'Data.SOP.NS.SOP' f xss -> 'Data.SOP.NS.SOP' g xss+ -- @+ --+ hap :: Prod h (f -.-> g) xs -> h f xs -> h g xs++-- ** Derived functions++-- | A generalized form of 'Control.Applicative.liftA',+-- which in turn is a generalized 'map'.+--+-- Takes a lifted function and applies it to every element of+-- a structure while preserving its shape.+--+-- /Specification:/+--+-- @+-- 'hliftA' f xs = 'hpure' ('fn' f) \` 'hap' \` xs+-- @+--+-- /Instances:/+--+-- @+-- 'hliftA', 'Data.SOP.NP.liftA_NP' :: 'Data.SOP.Sing.SListI' xs => (forall a. f a -> f' a) -> 'Data.SOP.NP.NP' f xs -> 'Data.SOP.NP.NP' f' xs+-- 'hliftA', 'Data.SOP.NS.liftA_NS' :: 'Data.SOP.Sing.SListI' xs => (forall a. f a -> f' a) -> 'Data.SOP.NS.NS' f xs -> 'Data.SOP.NS.NS' f' xs+-- 'hliftA', 'Data.SOP.NP.liftA_POP' :: 'SListI2' xss => (forall a. f a -> f' a) -> 'Data.SOP.NP.POP' f xss -> 'Data.SOP.NP.POP' f' xss+-- 'hliftA', 'Data.SOP.NS.liftA_SOP' :: 'SListI2' xss => (forall a. f a -> f' a) -> 'Data.SOP.NS.SOP' f xss -> 'Data.SOP.NS.SOP' f' xss+-- @+--+hliftA :: (SListIN (Prod h) xs, HAp h) => (forall a. f a -> f' a) -> h f xs -> h f' xs++-- | A generalized form of 'Control.Applicative.liftA2',+-- which in turn is a generalized 'zipWith'.+--+-- Takes a lifted binary function and uses it to combine two+-- structures of equal shape into a single structure.+--+-- It either takes two product structures to a product structure,+-- or one product and one sum structure to a sum structure.+--+-- /Specification:/+--+-- @+-- 'hliftA2' f xs ys = 'hpure' ('fn_2' f) \` 'hap' \` xs \` 'hap' \` ys+-- @+--+-- /Instances:/+--+-- @+-- 'hliftA2', 'Data.SOP.NP.liftA2_NP' :: 'Data.SOP.Sing.SListI' xs => (forall a. f a -> f' a -> f'' a) -> 'Data.SOP.NP.NP' f xs -> 'Data.SOP.NP.NP' f' xs -> 'Data.SOP.NP.NP' f'' xs+-- 'hliftA2', 'Data.SOP.NS.liftA2_NS' :: 'Data.SOP.Sing.SListI' xs => (forall a. f a -> f' a -> f'' a) -> 'Data.SOP.NP.NP' f xs -> 'Data.SOP.NS.NS' f' xs -> 'Data.SOP.NS.NS' f'' xs+-- 'hliftA2', 'Data.SOP.NP.liftA2_POP' :: 'SListI2' xss => (forall a. f a -> f' a -> f'' a) -> 'Data.SOP.NP.POP' f xss -> 'Data.SOP.NP.POP' f' xss -> 'Data.SOP.NP.POP' f'' xss+-- 'hliftA2', 'Data.SOP.NS.liftA2_SOP' :: 'SListI2' xss => (forall a. f a -> f' a -> f'' a) -> 'Data.SOP.NP.POP' f xss -> 'Data.SOP.NS.SOP' f' xss -> 'Data.SOP.NS.SOP' f'' xss+-- @+--+hliftA2 :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs++-- | A generalized form of 'Control.Applicative.liftA3',+-- which in turn is a generalized 'zipWith3'.+--+-- Takes a lifted ternary function and uses it to combine three+-- structures of equal shape into a single structure.+--+-- It either takes three product structures to a product structure,+-- or two product structures and one sum structure to a sum structure.+--+-- /Specification:/+--+-- @+-- 'hliftA3' f xs ys zs = 'hpure' ('fn_3' f) \` 'hap' \` xs \` 'hap' \` ys \` 'hap' \` zs+-- @+--+-- /Instances:/+--+-- @+-- 'hliftA3', 'Data.SOP.NP.liftA3_NP' :: 'Data.SOP.Sing.SListI' xs => (forall a. f a -> f' a -> f'' a -> f''' a) -> 'Data.SOP.NP.NP' f xs -> 'Data.SOP.NP.NP' f' xs -> 'Data.SOP.NP.NP' f'' xs -> 'Data.SOP.NP.NP' f''' xs+-- 'hliftA3', 'Data.SOP.NS.liftA3_NS' :: 'Data.SOP.Sing.SListI' xs => (forall a. f a -> f' a -> f'' a -> f''' a) -> 'Data.SOP.NP.NP' f xs -> 'Data.SOP.NP.NP' f' xs -> 'Data.SOP.NS.NS' f'' xs -> 'Data.SOP.NS.NS' f''' xs+-- 'hliftA3', 'Data.SOP.NP.liftA3_POP' :: 'SListI2' xss => (forall a. f a -> f' a -> f'' a -> f''' a) -> 'Data.SOP.NP.POP' f xss -> 'Data.SOP.NP.POP' f' xss -> 'Data.SOP.NP.POP' f'' xss -> 'Data.SOP.NP.POP' f''' xs+-- 'hliftA3', 'Data.SOP.NS.liftA3_SOP' :: 'SListI2' xss => (forall a. f a -> f' a -> f'' a -> f''' a) -> 'Data.SOP.NP.POP' f xss -> 'Data.SOP.NP.POP' f' xss -> 'Data.SOP.NS.SOP' f'' xss -> 'Data.SOP.NP.SOP' f''' xs+-- @+--+hliftA3 :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs++hliftA f xs = hpure (fn f) `hap` xs+hliftA2 f xs ys = hpure (fn_2 f) `hap` xs `hap` ys+hliftA3 f xs ys zs = hpure (fn_3 f) `hap` xs `hap` ys `hap` zs++-- | Another name for 'hliftA'.+--+-- @since 0.2+--+hmap :: (SListIN (Prod h) xs, HAp h) => (forall a. f a -> f' a) -> h f xs -> h f' xs++-- | Another name for 'hliftA2'.+--+-- @since 0.2+--+hzipWith :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs++-- | Another name for 'hliftA3'.+--+-- @since 0.2+--+hzipWith3 :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs++hmap = hliftA+hzipWith = hliftA2+hzipWith3 = hliftA3++-- | Variant of 'hliftA' that takes a constrained function.+--+-- /Specification:/+--+-- @+-- 'hcliftA' p f xs = 'hcpure' p ('fn' f) \` 'hap' \` xs+-- @+--+hcliftA :: (AllN (Prod h) c xs, HAp h) => proxy c -> (forall a. c a => f a -> f' a) -> h f xs -> h f' xs++-- | Variant of 'hcliftA2' that takes a constrained function.+--+-- /Specification:/+--+-- @+-- 'hcliftA2' p f xs ys = 'hcpure' p ('fn_2' f) \` 'hap' \` xs \` 'hap' \` ys+-- @+--+hcliftA2 :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs++-- | Variant of 'hcliftA3' that takes a constrained function.+--+-- /Specification:/+--+-- @+-- 'hcliftA3' p f xs ys zs = 'hcpure' p ('fn_3' f) \` 'hap' \` xs \` 'hap' \` ys \` 'hap' \` zs+-- @+--+hcliftA3 :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs++hcliftA p f xs = hcpure p (fn f) `hap` xs+hcliftA2 p f xs ys = hcpure p (fn_2 f) `hap` xs `hap` ys+hcliftA3 p f xs ys zs = hcpure p (fn_3 f) `hap` xs `hap` ys `hap` zs++-- | Another name for 'hcliftA'.+--+-- @since 0.2+--+hcmap :: (AllN (Prod h) c xs, HAp h) => proxy c -> (forall a. c a => f a -> f' a) -> h f xs -> h f' xs++-- | Another name for 'hcliftA2'.+--+-- @since 0.2+--+hczipWith :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs++-- | Another name for 'hcliftA3'.+--+-- @since 0.2+--+hczipWith3 :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs++hcmap = hcliftA+hczipWith = hcliftA2+hczipWith3 = hcliftA3++-- * Collapsing homogeneous structures++-- | Maps products to lists, and sums to identities.+type family CollapseTo (h :: (k -> Type) -> (l -> Type)) (x :: Type) :: Type++-- | A class for collapsing a heterogeneous structure into+-- a homogeneous one.+class HCollapse (h :: (k -> Type) -> (l -> Type)) where++ -- | Collapse a heterogeneous structure with homogeneous elements+ -- into a homogeneous structure.+ --+ -- If a heterogeneous structure is instantiated to the constant+ -- functor 'K', then it is in fact homogeneous. This function+ -- maps such a value to a simpler Haskell datatype reflecting that.+ -- An @'Data.SOP.NS' ('K' a)@ contains a single @a@, and an @'Data.SOP.NP' ('K' a)@ contains+ -- a list of @a@s.+ --+ -- /Instances:/+ --+ -- @+ -- 'hcollapse', 'Data.SOP.NP.collapse_NP' :: 'Data.SOP.NP.NP' ('K' a) xs -> [a]+ -- 'hcollapse', 'Data.SOP.NS.collapse_NS' :: 'Data.SOP.NS.NS' ('K' a) xs -> a+ -- 'hcollapse', 'Data.SOP.NP.collapse_POP' :: 'Data.SOP.NP.POP' ('K' a) xss -> [[a]]+ -- 'hcollapse', 'Data.SOP.NS.collapse_SOP' :: 'Data.SOP.NP.SOP' ('K' a) xss -> [a]+ -- @+ --+ hcollapse :: SListIN h xs => h (K a) xs -> CollapseTo h a++-- | A generalization of 'Data.Foldable.traverse_' or 'Data.Foldable.foldMap'.+--+-- @since 0.3.2.0+--+class HTraverse_ (h :: (k -> Type) -> (l -> Type)) where++ -- | Corresponds to 'Data.Foldable.traverse_'.+ --+ -- /Instances:/+ --+ -- @+ -- 'hctraverse_', 'Data.SOP.NP.ctraverse__NP' :: ('All' c xs , 'Applicative' g) => proxy c -> (forall a. c a => f a -> g ()) -> 'Data.SOP.NP.NP' f xs -> g ()+ -- 'hctraverse_', 'Data.SOP.NS.ctraverse__NS' :: ('All2' c xs , 'Applicative' g) => proxy c -> (forall a. c a => f a -> g ()) -> 'Data.SOP.NS.NS' f xs -> g ()+ -- 'hctraverse_', 'Data.SOP.NP.ctraverse__POP' :: ('All' c xss, 'Applicative' g) => proxy c -> (forall a. c a => f a -> g ()) -> 'Data.SOP.NP.POP' f xss -> g ()+ -- 'hctraverse_', 'Data.SOP.NS.ctraverse__SOP' :: ('All2' c xss, 'Applicative' g) => proxy c -> (forall a. c a => f a -> g ()) -> 'Data.SOP.NS.SOP' f xss -> g ()+ -- @+ --+ -- @since 0.3.2.0+ --+ hctraverse_ :: (AllN h c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g ()) -> h f xs -> g ()++ -- | Unconstrained version of 'hctraverse_'.+ --+ -- /Instances:/+ --+ -- @+ -- 'traverse_', 'Data.SOP.NP.traverse__NP' :: ('SListI' xs , 'Applicative' g) => (forall a. f a -> g ()) -> 'Data.SOP.NP.NP' f xs -> g ()+ -- 'traverse_', 'Data.SOP.NS.traverse__NS' :: ('SListI' xs , 'Applicative' g) => (forall a. f a -> g ()) -> 'Data.SOP.NS.NS' f xs -> g ()+ -- 'traverse_', 'Data.SOP.NP.traverse__POP' :: ('SListI2' xss, 'Applicative' g) => (forall a. f a -> g ()) -> 'Data.SOP.NP.POP' f xss -> g ()+ -- 'traverse_', 'Data.SOP.NS.traverse__SOP' :: ('SListI2' xss, 'Applicative' g) => (forall a. f a -> g ()) -> 'Data.SOP.NS.SOP' f xss -> g ()+ -- @+ --+ -- @since 0.3.2.0+ --+ htraverse_ :: (SListIN h xs, Applicative g) => (forall a. f a -> g ()) -> h f xs -> g ()++-- | Flipped version of 'hctraverse_'.+--+-- @since 0.3.2.0+--+hcfor_ :: (HTraverse_ h, AllN h c xs, Applicative g) => proxy c -> h f xs -> (forall a. c a => f a -> g ()) -> g ()+hcfor_ p xs f = hctraverse_ p f xs++-- | Special case of 'hctraverse_'.+--+-- @since 0.3.2.0+--+hcfoldMap :: (HTraverse_ h, AllN h c xs, Monoid m) => proxy c -> (forall a. c a => f a -> m) -> h f xs -> m+hcfoldMap p f = unK . hctraverse_ p (K . f)++-- * Sequencing effects++-- | A generalization of 'Data.Traversable.sequenceA'.+class HAp h => HSequence (h :: (k -> Type) -> (l -> Type)) where++ -- | Corresponds to 'Data.Traversable.sequenceA'.+ --+ -- Lifts an applicative functor out of a structure.+ --+ -- /Instances:/+ --+ -- @+ -- 'hsequence'', 'Data.SOP.NP.sequence'_NP' :: ('Data.SOP.Sing.SListI' xs , 'Applicative' f) => 'Data.SOP.NP.NP' (f ':.:' g) xs -> f ('Data.SOP.NP.NP' g xs )+ -- 'hsequence'', 'Data.SOP.NS.sequence'_NS' :: ('Data.SOP.Sing.SListI' xs , 'Applicative' f) => 'Data.SOP.NS.NS' (f ':.:' g) xs -> f ('Data.SOP.NS.NS' g xs )+ -- 'hsequence'', 'Data.SOP.NP.sequence'_POP' :: ('SListI2' xss, 'Applicative' f) => 'Data.SOP.NP.POP' (f ':.:' g) xss -> f ('Data.SOP.NP.POP' g xss)+ -- 'hsequence'', 'Data.SOP.NS.sequence'_SOP' :: ('SListI2' xss, 'Applicative' f) => 'Data.SOP.NS.SOP' (f ':.:' g) xss -> f ('Data.SOP.NS.SOP' g xss)+ -- @+ --+ hsequence' :: (SListIN h xs, Applicative f) => h (f :.: g) xs -> f (h g xs)+++ -- | Corresponds to 'Data.Traversable.traverse'.+ --+ -- /Instances:/+ --+ -- @+ -- 'hctraverse'', 'Data.SOP.NP.ctraverse'_NP' :: ('All' c xs , 'Applicative' g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> 'Data.SOP.NP.NP' f xs -> g ('Data.SOP.NP.NP' f' xs )+ -- 'hctraverse'', 'Data.SOP.NS.ctraverse'_NS' :: ('All2' c xs , 'Applicative' g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> 'Data.SOP.NS.NS' f xs -> g ('Data.SOP.NS.NS' f' xs )+ -- 'hctraverse'', 'Data.SOP.NP.ctraverse'_POP' :: ('All' c xss, 'Applicative' g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> 'Data.SOP.NP.POP' f xss -> g ('Data.SOP.NP.POP' f' xss)+ -- 'hctraverse'', 'Data.SOP.NS.ctraverse'_SOP' :: ('All2' c xss, 'Applicative' g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> 'Data.SOP.NS.SOP' f xss -> g ('Data.SOP.NS.SOP' f' xss)+ -- @+ --+ -- @since 0.3.2.0+ --+ hctraverse' :: (AllN h c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> h f xs -> g (h f' xs)++ -- | Unconstrained variant of `htraverse'`.+ --+ -- /Instances:/+ --+ -- @+ -- 'htraverse'', 'Data.SOP.NP.traverse'_NP' :: ('SListI' xs , 'Applicative' g) => (forall a. c a => f a -> g (f' a)) -> 'Data.SOP.NP.NP' f xs -> g ('Data.SOP.NP.NP' f' xs )+ -- 'htraverse'', 'Data.SOP.NS.traverse'_NS' :: ('SListI2' xs , 'Applicative' g) => (forall a. c a => f a -> g (f' a)) -> 'Data.SOP.NS.NS' f xs -> g ('Data.SOP.NS.NS' f' xs )+ -- 'htraverse'', 'Data.SOP.NP.traverse'_POP' :: ('SListI' xss, 'Applicative' g) => (forall a. c a => f a -> g (f' a)) -> 'Data.SOP.NP.POP' f xss -> g ('Data.SOP.NP.POP' f' xss)+ -- 'htraverse'', 'Data.SOP.NS.traverse'_SOP' :: ('SListI2' xss, 'Applicative' g) => (forall a. c a => f a -> g (f' a)) -> 'Data.SOP.NS.SOP' f xss -> g ('Data.SOP.NS.SOP' f' xss)+ -- @+ --+ -- @since 0.3.2.0+ --+ htraverse' :: (SListIN h xs, Applicative g) => (forall a. f a -> g (f' a)) -> h f xs -> g (h f' xs)++-- ** Derived functions++-- | Special case of 'hctraverse'' where @f' = 'I'@.+--+-- @since 0.3.2.0+--+hctraverse :: (HSequence h, AllN h c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> h f xs -> g (h I xs)+hctraverse p f = hctraverse' p (fmap I . f)++-- | Flipped version of 'hctraverse'.+--+-- @since 0.3.2.0+--+hcfor :: (HSequence h, AllN h c xs, Applicative g) => proxy c -> h f xs -> (forall a. c a => f a -> g a) -> g (h I xs)+hcfor p xs f = hctraverse p f xs++-- | Special case of 'hsequence'' where @g = 'I'@.+hsequence :: (SListIN h xs, SListIN (Prod h) xs, HSequence h) => Applicative f => h f xs -> f (h I xs)+hsequence = hsequence' . hliftA (Comp . fmap I)++-- | Special case of 'hsequence'' where @g = 'K' a@.+hsequenceK :: (SListIN h xs, SListIN (Prod h) xs, Applicative f, HSequence h) => h (K (f a)) xs -> f (h (K a) xs)+hsequenceK = hsequence' . hliftA (Comp . fmap K . unK)++-- * Indexing into sums++-- | A class for determining which choice in a sum-like structure+-- a value represents.+--+class HIndex (h :: (k -> Type) -> (l -> Type)) where++ -- | If 'h' is a sum-like structure representing a choice+ -- between @n@ different options, and @x@ is a value of+ -- type @h f xs@, then @'hindex' x@ returns a number between+ -- @0@ and @n - 1@ representing the index of the choice+ -- made by @x@.+ --+ -- /Instances:/+ --+ -- @+ -- 'hindex', 'Data.SOP.NS.index_NS' :: 'Data.SOP.NS.NS' f xs -> Int+ -- 'hindex', 'Data.SOP.NS.index_SOP' :: 'Data.SOP.NS.SOP' f xs -> Int+ -- @+ --+ -- /Examples:/+ --+ -- >>> hindex (S (S (Z (I False))))+ -- 2+ -- >>> hindex (Z (K ()))+ -- 0+ -- >>> hindex (SOP (S (Z (I True :* I 'x' :* Nil))))+ -- 1+ --+ -- @since 0.2.4.0+ --+ hindex :: h f xs -> Int++-- * Applying all injections++-- | Maps a structure containing products to the corresponding+-- sum structure.+--+-- @since 0.2.4.0+--+type family UnProd (h :: (k -> Type) -> (l -> Type)) :: (k -> Type) -> (l -> Type)++-- | A class for applying all injections corresponding to a sum-like+-- structure to a table containing suitable arguments.+--+class (UnProd (Prod h) ~ h) => HApInjs (h :: (k -> Type) -> (l -> Type)) where++ -- | For a given table (product-like structure), produce a list where+ -- each element corresponds to the application of an injection function+ -- into the corresponding sum-like structure.+ --+ -- /Instances:/+ --+ -- @+ -- 'hapInjs', 'Data.SOP.NS.apInjs_NP' :: 'Data.SOP.Sing.SListI' xs => 'Data.SOP.NP.NP' f xs -> ['Data.SOP.NS.NS' f xs ]+ -- 'hapInjs', 'Data.SOP.NS.apInjs_SOP' :: 'SListI2' xss => 'Data.SOP.NP.POP' f xs -> ['Data.SOP.NS.SOP' f xss]+ -- @+ --+ -- /Examples:/+ --+ -- >>> hapInjs (I 'x' :* I True :* I 2 :* Nil) :: [NS I '[Char, Bool, Int]]+ -- [Z (I 'x'),S (Z (I True)),S (S (Z (I 2)))]+ --+ -- >>> hapInjs (POP ((I 'x' :* Nil) :* (I True :* I 2 :* Nil) :* Nil)) :: [SOP I '[ '[Char], '[Bool, Int]]]+ -- [SOP (Z (I 'x' :* Nil)),SOP (S (Z (I True :* I 2 :* Nil)))]+ --+ -- Unfortunately the type-signatures are required in GHC-7.10 and older.+ --+ -- @since 0.2.4.0+ --+ hapInjs :: (SListIN h xs) => Prod h f xs -> [h f xs]++-- * Expanding sums to products++-- | A class for expanding sum structures into corresponding product+-- structures, filling in the slots not targeted by the sum with+-- default values.+--+-- @since 0.2.5.0+--+class HExpand (h :: (k -> Type) -> (l -> Type)) where++ -- | Expand a given sum structure into a corresponding product+ -- structure by placing the value contained in the sum into the+ -- corresponding position in the product, and using the given+ -- default value for all other positions.+ --+ -- /Instances:/+ --+ -- @+ -- 'hexpand', 'Data.SOP.NS.expand_NS' :: 'Data.SOP.Sing.SListI' xs => (forall x . f x) -> 'Data.SOP.NS.NS' f xs -> 'Data.SOP.NS.NP' f xs+ -- 'hexpand', 'Data.SOP.NS.expand_SOP' :: 'SListI2' xss => (forall x . f x) -> 'Data.SOP.NS.SOP' f xss -> 'Data.SOP.NP.POP' f xss+ -- @+ --+ -- /Examples:/+ --+ -- >>> hexpand Nothing (S (Z (Just 3))) :: NP Maybe '[Char, Int, Bool]+ -- Nothing :* Just 3 :* Nothing :* Nil+ -- >>> hexpand [] (SOP (S (Z ([1,2] :* "xyz" :* Nil)))) :: POP [] '[ '[Bool], '[Int, Char] ]+ -- POP (([] :* Nil) :* ([1,2] :* "xyz" :* Nil) :* Nil)+ --+ -- @since 0.2.5.0+ --+ hexpand :: (SListIN (Prod h) xs) => (forall x . f x) -> h f xs -> Prod h f xs++ -- | Variant of 'hexpand' that allows passing a constrained default.+ --+ -- /Instances:/+ --+ -- @+ -- 'hcexpand', 'Data.SOP.NS.cexpand_NS' :: 'All' c xs => proxy c -> (forall x . c x => f x) -> 'Data.SOP.NS.NS' f xs -> 'Data.SOP.NP.NP' f xs+ -- 'hcexpand', 'Data.SOP.NS.cexpand_SOP' :: 'All2' c xss => proxy c -> (forall x . c x => f x) -> 'Data.SOP.NS.SOP' f xss -> 'Data.SOP.NP.POP' f xss+ -- @+ --+ -- /Examples:/+ --+ -- >>> hcexpand (Proxy :: Proxy Bounded) (I minBound) (S (Z (I 20))) :: NP I '[Bool, Int, Ordering]+ -- I False :* I 20 :* I LT :* Nil+ -- >>> hcexpand (Proxy :: Proxy Num) (I 0) (SOP (S (Z (I 1 :* I 2 :* Nil)))) :: POP I '[ '[Double], '[Int, Int] ]+ -- POP ((I 0.0 :* Nil) :* (I 1 :* I 2 :* Nil) :* Nil)+ --+ -- @since 0.2.5.0+ --+ hcexpand :: (AllN (Prod h) c xs) => proxy c -> (forall x . c x => f x) -> h f xs -> Prod h f xs++-- | A class for transforming structures into related structures with+-- a different index list, as long as the index lists have the same shape+-- and the elements and interpretation functions are suitably related.+--+-- @since 0.3.1.0+--+class (Same h1 ~ h2, Same h2 ~ h1) => HTrans (h1 :: (k1 -> Type) -> (l1 -> Type)) (h2 :: (k2 -> Type) -> (l2 -> Type)) where++ -- | Transform a structure into a related structure given a conversion+ -- function for the elements.+ --+ -- @since 0.3.1.0+ --+ htrans ::+ AllZipN (Prod h1) c xs ys+ => proxy c+ -> (forall x y . c x y => f x -> g y)+ -> h1 f xs -> h2 g ys++ -- | Safely coerce a structure into a representationally equal structure.+ --+ -- This is a special case of 'htrans', but can be implemented more efficiently;+ -- for example in terms of 'Unsafe.Coerce.unsafeCoerce'.+ --+ -- /Examples:/+ --+ -- >>> hcoerce (I (Just LT) :* I (Just 'x') :* I (Just True) :* Nil) :: NP Maybe '[Ordering, Char, Bool]+ -- Just LT :* Just 'x' :* Just True :* Nil+ -- >>> hcoerce (SOP (Z (K True :* K False :* Nil))) :: SOP I '[ '[Bool, Bool], '[Bool] ]+ -- SOP (Z (I True :* I False :* Nil))+ --+ -- @since 0.3.1.0+ --+ hcoerce ::+ (AllZipN (Prod h1) (LiftedCoercible f g) xs ys, HTrans h1 h2)+ => h1 f xs -> h2 g ys++-- | Specialization of 'hcoerce'.+--+-- @since 0.3.1.0+--+hfromI ::+ (AllZipN (Prod h1) (LiftedCoercible I f) xs ys, HTrans h1 h2)+ => h1 I xs -> h2 f ys+hfromI = hcoerce++-- | Specialization of 'hcoerce'.+--+-- @since 0.3.1.0+--+htoI ::+ (AllZipN (Prod h1) (LiftedCoercible f I) xs ys, HTrans h1 h2)+ => h1 f xs -> h2 I ys+htoI = hcoerce++-- $setup+-- >>> import Data.SOP
+ src/Data/SOP/Constraint.hs view
@@ -0,0 +1,281 @@+{-# LANGUAGE PolyKinds, UndecidableInstances #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# OPTIONS_GHC -fno-warn-orphans -fno-warn-deprecations #-}+-- | Constraints for indexed datatypes.+--+-- This module contains code that helps to specify that all+-- elements of an indexed structure must satisfy a particular+-- constraint.+--+module Data.SOP.Constraint+ ( module Data.SOP.Constraint+ , Constraint+ ) where++import Data.Coerce+import Data.Kind (Type, Constraint)++-- import Data.SOP.Sing++-- | Require a constraint for every element of a list.+--+-- If you have a datatype that is indexed over a type-level+-- list, then you can use 'All' to indicate that all elements+-- of that type-level list must satisfy a given constraint.+--+-- /Example:/ The constraint+--+-- > All Eq '[ Int, Bool, Char ]+--+-- is equivalent to the constraint+--+-- > (Eq Int, Eq Bool, Eq Char)+--+-- /Example:/ A type signature such as+--+-- > f :: All Eq xs => NP I xs -> ...+--+-- means that 'f' can assume that all elements of the n-ary+-- product satisfy 'Eq'.+--+-- Note on superclasses: ghc cannot deduce superclasses from 'All'+-- constraints.+-- You might expect the following to compile+--+-- > class (Eq a) => MyClass a+-- >+-- > foo :: (All Eq xs) => NP f xs -> z+-- > foo = [..]+-- >+-- > bar :: (All MyClass xs) => NP f xs -> x+-- > bar = foo+-- but it will fail with an error saying that it was unable to+-- deduce the class constraint @'AllF' 'Eq' xs@ (or similar) in the+-- definition of 'bar'.+-- In cases like this you can use 'Data.SOP.Dict.Dict' from "Data.SOP.Dict"+-- to prove conversions between constraints.+-- See [this answer on SO for more details](https://stackoverflow.com/questions/50777865/super-classes-with-all-from-generics-sop).++--+class (AllF c xs, SListI xs) => All (c :: k -> Constraint) (xs :: [k]) where++ -- | Constrained paramorphism for a type-level list.+ --+ -- The advantage of writing functions in terms of 'cpara_SList' is that+ -- they are then typically not recursive, and can be unfolded statically if+ -- the type-level list is statically known.+ --+ -- @since 0.4.0.0+ --+ cpara_SList ::+ proxy c+ -> r '[]+ -> (forall y ys . (c y, All c ys) => r ys -> r (y ': ys))+ -> r xs++instance All c '[] where+ cpara_SList _p nil _cons = nil+ {-# INLINE cpara_SList #-}++instance (c x, All c xs) => All c (x ': xs) where+ cpara_SList p nil cons =+ cons (cpara_SList p nil cons)+ {-# INLINE cpara_SList #-}++-- | Constrained case distinction on a type-level list.+--+-- @since 0.4.0.0+--+ccase_SList ::+ All c xs+ => proxy c+ -> r '[]+ -> (forall y ys . (c y, All c ys) => r (y ': ys))+ -> r xs+ccase_SList p nil cons =+ cpara_SList p nil (const cons)+{-# INLINE ccase_SList #-}++-- | Type family used to implement 'All'.+--+type family+ AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint where+ AllF _c '[] = ()+ AllF c (x ': xs) = (c x, All c xs)++-- | Require a singleton for every inner list in a list of lists.+type SListI2 = All SListI++-- | Implicit singleton list.+--+-- A singleton list can be used to reveal the structure of+-- a type-level list argument that the function is quantified+-- over.+--+-- Since 0.4.0.0, this is now defined in terms of 'All'.+-- A singleton list provides a witness for a type-level list+-- where the elements need not satisfy any additional+-- constraints.+--+-- @since 0.4.0.0+--+type SListI = All Top++-- | Require a constraint for every element of a list of lists.+--+-- If you have a datatype that is indexed over a type-level+-- list of lists, then you can use 'All2' to indicate that all+-- elements of the inner lists must satisfy a given constraint.+--+-- /Example:/ The constraint+--+-- > All2 Eq '[ '[ Int ], '[ Bool, Char ] ]+--+-- is equivalent to the constraint+--+-- > (Eq Int, Eq Bool, Eq Char)+--+-- /Example:/ A type signature such as+--+-- > f :: All2 Eq xss => SOP I xs -> ...+--+-- means that 'f' can assume that all elements of the sum+-- of product satisfy 'Eq'.+--+-- Since 0.4.0.0, this is merely a synonym for+-- 'All (All c)'.+--+-- @since 0.4.0.0+--+type All2 c = All (All c)++-- | Require a constraint for pointwise for every pair of+-- elements from two lists.+--+-- /Example:/ The constraint+--+-- > All (~) '[ Int, Bool, Char ] '[ a, b, c ]+--+-- is equivalent to the constraint+--+-- > (Int ~ a, Bool ~ b, Char ~ c)+--+-- @since 0.3.1.0+--+class+ ( SListI xs, SListI ys+ , SameShapeAs xs ys, SameShapeAs ys xs+ , AllZipF c xs ys+ ) => AllZip (c :: a -> b -> Constraint) (xs :: [a]) (ys :: [b])+instance+ ( SListI xs, SListI ys+ , SameShapeAs xs ys, SameShapeAs ys xs+ , AllZipF c xs ys+ ) => AllZip c xs ys++-- | Type family used to implement 'AllZip'.+--+-- @since 0.3.1.0+--+type family+ AllZipF (c :: a -> b -> Constraint) (xs :: [a]) (ys :: [b])+ :: Constraint where+ AllZipF _c '[] '[] = ()+ AllZipF c (x ': xs) (y ': ys) = (c x y, AllZip c xs ys)++-- | Type family that forces a type-level list to be of the same+-- shape as the given type-level list.+--+-- The main use of this constraint is to help type inference to+-- learn something about otherwise unknown type-level lists.+--+-- @since 0.3.1.0+--+type family+ SameShapeAs (xs :: [a]) (ys :: [b]) :: Constraint where+ SameShapeAs '[] ys = (ys ~ '[])+ SameShapeAs (x ': xs) ys =+ (ys ~ (Head ys ': Tail ys), SameShapeAs xs (Tail ys))++-- | Utility function to compute the head of a type-level list.+--+-- @since 0.3.1.0+--+type family Head (xs :: [a]) :: a where+ Head (x ': xs) = x++-- | Utility function to compute the tail of a type-level list.+--+-- @since 0.3.1.0+--+type family Tail (xs :: [a]) :: [a] where+ Tail (x ': xs) = xs++-- | The constraint @'LiftedCoercible' f g x y@ is equivalent+-- to @'Data.Coerce.Coercible' (f x) (g y)@.+--+-- @since 0.3.1.0+--+class Coercible (f x) (g y) => LiftedCoercible f g x y+instance Coercible (f x) (g y) => LiftedCoercible f g x y++-- | Require a constraint for pointwise for every pair of+-- elements from two lists of lists.+--+--+class (AllZipF (AllZip f) xss yss, SListI xss, SListI yss, SameShapeAs xss yss, SameShapeAs yss xss) => AllZip2 f xss yss+instance (AllZipF (AllZip f) xss yss, SListI xss, SListI yss, SameShapeAs xss yss, SameShapeAs yss xss) => AllZip2 f xss yss++-- | Composition of constraints.+--+-- Note that the result of the composition must be a constraint,+-- and therefore, in @'Compose' f g@, the kind of @f@ is @k -> 'Constraint'@.+-- The kind of @g@, however, is @l -> k@ and can thus be an normal+-- type constructor.+--+-- A typical use case is in connection with 'All' on an 'Data.SOP.NP' or an+-- 'Data.SOP.NS'. For example, in order to denote that all elements on an+-- @'Data.SOP.NP' f xs@ satisfy 'Show', we can say @'All' ('Compose' 'Show' f) xs@.+--+-- @since 0.2+--+class (f (g x)) => (f `Compose` g) x+instance (f (g x)) => (f `Compose` g) x+infixr 9 `Compose`++-- | Pairing of constraints.+--+-- @since 0.2+--+class (f x, g x) => (f `And` g) x+instance (f x, g x) => (f `And` g) x+infixl 7 `And`++-- | A constraint that can always be satisfied.+--+-- @since 0.2+--+class Top x+instance Top x++-- | A generalization of 'All' and 'All2'.+--+-- The family 'AllN' expands to 'All' or 'All2' depending on whether+-- the argument is indexed by a list or a list of lists.+--+type family AllN (h :: (k -> Type) -> (l -> Type)) (c :: k -> Constraint) :: l -> Constraint++-- | A generalization of 'AllZip' and 'AllZip2'.+--+-- The family 'AllZipN' expands to 'AllZip' or 'AllZip2' depending on+-- whther the argument is indexed by a list or a list of lists.+--+type family AllZipN (h :: (k -> Type) -> (l -> Type)) (c :: k1 -> k2 -> Constraint) :: l1 -> l2 -> Constraint++-- | A generalization of 'SListI'.+--+-- The family 'SListIN' expands to 'SListI' or 'SListI2' depending+-- on whether the argument is indexed by a list or a list of lists.+--+type family SListIN (h :: (k -> Type) -> (l -> Type)) :: l -> Constraint+
+ src/Data/SOP/Dict.hs view
@@ -0,0 +1,159 @@+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE StandaloneDeriving #-}+-- | Explicit dictionaries.+--+-- When working with compound constraints such as constructed+-- using 'All' or 'All2', GHC cannot always prove automatically+-- what one would expect to hold.+--+-- This module provides a way of explicitly proving+-- conversions between such constraints to GHC. Such conversions+-- still have to be manually applied.+--+-- This module remains somewhat experimental.+-- It is therefore not exported via the main module and+-- has to be imported explicitly.+--+module Data.SOP.Dict where++import Data.Proxy+import Data.SOP.Classes+import Data.SOP.Constraint+import Data.SOP.NP++-- | An explicit dictionary carrying evidence of a+-- class constraint.+--+-- The constraint parameter is separated into a+-- second argument so that @'Dict' c@ is of the correct+-- kind to be used directly as a parameter to e.g. 'NP'.+--+-- @since 0.2+--+data Dict (c :: k -> Constraint) (a :: k) where+ Dict :: c a => Dict c a++deriving instance Show (Dict c a)++-- | A proof that the trivial constraint holds+-- over all type-level lists.+--+-- @since 0.2+--+pureAll :: SListI xs => Dict (All Top) xs+pureAll = all_NP (hpure Dict)++-- | A proof that the trivial constraint holds+-- over all type-level lists of lists.+--+-- @since 0.2+--+pureAll2 :: All SListI xss => Dict (All2 Top) xss+pureAll2 = all_POP (hpure Dict)++-- | Lifts a dictionary conversion over a type-level list.+--+-- @since 0.2+--+mapAll :: forall c d xs .+ (forall a . Dict c a -> Dict d a)+ -> Dict (All c) xs -> Dict (All d) xs+mapAll f Dict = (all_NP . hmap f . unAll_NP) Dict++-- | Lifts a dictionary conversion over a type-level list+-- of lists.+--+-- @since 0.2+--+mapAll2 :: forall c d xss .+ (forall a . Dict c a -> Dict d a)+ -> Dict (All2 c) xss -> Dict (All2 d) xss+mapAll2 f d @ Dict = (all2 . mapAll (mapAll f) . unAll2) d++-- | If two constraints 'c' and 'd' hold over a type-level+-- list 'xs', then the combination of both constraints holds+-- over that list.+--+-- @since 0.2+--+zipAll :: Dict (All c) xs -> Dict (All d) xs -> Dict (All (c `And` d)) xs+zipAll dc @ Dict dd = all_NP (hzipWith (\ Dict Dict -> Dict) (unAll_NP dc) (unAll_NP dd))++-- | If two constraints 'c' and 'd' hold over a type-level+-- list of lists 'xss', then the combination of both constraints+-- holds over that list of lists.+--+-- @since 0.2+--+zipAll2 :: All SListI xss => Dict (All2 c) xss -> Dict (All2 d) xss -> Dict (All2 (c `And` d)) xss+zipAll2 dc dd = all_POP (hzipWith (\ Dict Dict -> Dict) (unAll_POP dc) (unAll_POP dd))+-- TODO: I currently don't understand why the All constraint in the beginning+-- cannot be inferred.++-- | If we have a constraint 'c' that holds over a type-level+-- list 'xs', we can create a product containing proofs that+-- each individual list element satisfies 'c'.+--+-- @since 0.2+--+unAll_NP :: forall c xs . Dict (All c) xs -> NP (Dict c) xs+unAll_NP d = withDict d hdicts++-- | If we have a constraint 'c' that holds over a type-level+-- list of lists 'xss', we can create a product of products+-- containing proofs that all the inner elements satisfy 'c'.+--+-- @since 0.2+--+unAll_POP :: forall c xss . Dict (All2 c) xss -> POP (Dict c) xss+unAll_POP d = withDict d hdicts++-- | If we have a product containing proofs that each element+-- of 'xs' satisfies 'c', then @'All' c@ holds for 'xs'.+--+-- @since 0.2+--+all_NP :: NP (Dict c) xs -> Dict (All c) xs+all_NP Nil = Dict+all_NP (Dict :* ds) = withDict (all_NP ds) Dict++-- | If we have a product of products containing proofs that+-- each inner element of 'xss' satisfies 'c', then @'All2' c@+-- holds for 'xss'.+--+-- @since 0.2+--+all_POP :: SListI xss => POP (Dict c) xss -> Dict (All2 c) xss+all_POP = all2 . all_NP . hmap all_NP . unPOP+-- TODO: Is the constraint necessary?++-- | The constraint @'All2' c@ is convertible to @'All' ('All' c)@.+--+-- @since 0.2+--+unAll2 :: Dict (All2 c) xss -> Dict (All (All c)) xss+unAll2 = id+{-# DEPRECATED unAll2 "'All2 c' is now a synonym of 'All (All c)'" #-}++-- | The constraint @'All' ('All' c)@ is convertible to @'All2' c@.+--+-- @since 0.2+--+all2 :: Dict (All (All c)) xss -> Dict (All2 c) xss+all2 = id+{-# DEPRECATED all2 "'All2 c' is now a synonym of 'All (All c)'" #-}++-- | If we have an explicit dictionary, we can unwrap it and+-- pass a function that makes use of it.+--+-- @since 0.2+--+withDict :: Dict c a -> (c a => r) -> r+withDict Dict x = x++-- | A structure of dictionaries.+--+-- @since 0.2.3.0+--+hdicts :: forall h c xs . (AllN h c xs, HPure h) => h (Dict c) xs+hdicts = hcpure (Proxy :: Proxy c) Dict
+ src/Data/SOP/NP.hs view
@@ -0,0 +1,900 @@+{-# LANGUAGE PolyKinds, StandaloneDeriving, UndecidableInstances #-}+-- | n-ary products (and products of products)+module Data.SOP.NP+ ( -- * Datatypes+ NP(..)+ , POP(..)+ , unPOP+ -- * Constructing products+ , pure_NP+ , pure_POP+ , cpure_NP+ , cpure_POP+ -- ** Construction from a list+ , fromList+ -- * Application+ , ap_NP+ , ap_POP+ -- * Destructing products+ , hd+ , tl+ , Projection+ , projections+ , shiftProjection+ -- * Lifting / mapping+ , liftA_NP+ , liftA_POP+ , liftA2_NP+ , liftA2_POP+ , liftA3_NP+ , liftA3_POP+ , map_NP+ , map_POP+ , zipWith_NP+ , zipWith_POP+ , zipWith3_NP+ , zipWith3_POP+ , cliftA_NP+ , cliftA_POP+ , cliftA2_NP+ , cliftA2_POP+ , cliftA3_NP+ , cliftA3_POP+ , cmap_NP+ , cmap_POP+ , czipWith_NP+ , czipWith_POP+ , czipWith3_NP+ , czipWith3_POP+ -- * Dealing with @'All' c@+ , hcliftA'+ , hcliftA2'+ , hcliftA3'+ , cliftA2'_NP+ -- * Collapsing+ , collapse_NP+ , collapse_POP+ -- * Folding and sequencing+ , ctraverse__NP+ , ctraverse__POP+ , traverse__NP+ , traverse__POP+ , cfoldMap_NP+ , cfoldMap_POP+ , sequence'_NP+ , sequence'_POP+ , sequence_NP+ , sequence_POP+ , ctraverse'_NP+ , ctraverse'_POP+ , traverse'_NP+ , traverse'_POP+ , ctraverse_NP+ , ctraverse_POP+ -- * Catamorphism and anamorphism+ , cata_NP+ , ccata_NP+ , ana_NP+ , cana_NP+ -- * Transformation of index lists and coercions+ , trans_NP+ , trans_POP+ , coerce_NP+ , coerce_POP+ , fromI_NP+ , fromI_POP+ , toI_NP+ , toI_POP+ ) where++import Data.Coerce+import Data.Kind (Type)+import Data.Proxy (Proxy(..))+import Unsafe.Coerce+import Data.Semigroup (Semigroup (..))++import Control.DeepSeq (NFData(..))++import Data.SOP.BasicFunctors+import Data.SOP.Classes+import Data.SOP.Constraint+import Data.SOP.Sing++-- | An n-ary product.+--+-- The product is parameterized by a type constructor @f@ and+-- indexed by a type-level list @xs@. The length of the list+-- determines the number of elements in the product, and if the+-- @i@-th element of the list is of type @x@, then the @i@-th+-- element of the product is of type @f x@.+--+-- The constructor names are chosen to resemble the names of the+-- list constructors.+--+-- Two common instantiations of @f@ are the identity functor 'I'+-- and the constant functor 'K'. For 'I', the product becomes a+-- heterogeneous list, where the type-level list describes the+-- types of its components. For @'K' a@, the product becomes a+-- homogeneous list, where the contents of the type-level list are+-- ignored, but its length still specifies the number of elements.+--+-- In the context of the SOP approach to generic programming, an+-- n-ary product describes the structure of the arguments of a+-- single data constructor.+--+-- /Examples:/+--+-- > I 'x' :* I True :* Nil :: NP I '[ Char, Bool ]+-- > K 0 :* K 1 :* Nil :: NP (K Int) '[ Char, Bool ]+-- > Just 'x' :* Nothing :* Nil :: NP Maybe '[ Char, Bool ]+--+data NP :: (k -> Type) -> [k] -> Type where+ Nil :: NP f '[]+ (:*) :: f x -> NP f xs -> NP f (x ': xs)++infixr 5 :*++-- This is written manually,+-- because built-in deriving doesn't use associativity information!+instance All (Show `Compose` f) xs => Show (NP f xs) where+ showsPrec _ Nil = showString "Nil"+ showsPrec d (f :* fs) = showParen (d > 5)+ $ showsPrec (5 + 1) f+ . showString " :* "+ . showsPrec 5 fs++deriving instance All (Eq `Compose` f) xs => Eq (NP f xs)+deriving instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NP f xs)++-- | @since 0.4.0.0+instance All (Semigroup `Compose` f) xs => Semigroup (NP f xs) where+ (<>) = czipWith_NP (Proxy :: Proxy (Semigroup `Compose` f)) (<>)++-- | @since 0.4.0.0+instance (All (Monoid `Compose` f) xs+#if MIN_VERSION_base(4,11,0)+ , All (Semigroup `Compose` f) xs -- GHC isn't smart enough to figure this out+#endif+ ) => Monoid (NP f xs) where+ mempty = cpure_NP (Proxy :: Proxy (Monoid `Compose` f)) mempty+ mappend = czipWith_NP (Proxy :: Proxy (Monoid `Compose` f)) mappend++-- | @since 0.2.5.0+instance All (NFData `Compose` f) xs => NFData (NP f xs) where+ rnf Nil = ()+ rnf (x :* xs) = rnf x `seq` rnf xs++-- | A product of products.+--+-- This is a 'newtype' for an 'NP' of an 'NP'. The elements of the+-- inner products are applications of the parameter @f@. The type+-- 'POP' is indexed by the list of lists that determines the lengths+-- of both the outer and all the inner products, as well as the types+-- of all the elements of the inner products.+--+-- A 'POP' is reminiscent of a two-dimensional table (but the inner+-- lists can all be of different length). In the context of the SOP+-- approach to generic programming, a 'POP' is useful to represent+-- information that is available for all arguments of all constructors+-- of a datatype.+--+newtype POP (f :: (k -> Type)) (xss :: [[k]]) = POP (NP (NP f) xss)++deriving instance (Show (NP (NP f) xss)) => Show (POP f xss)+deriving instance (Eq (NP (NP f) xss)) => Eq (POP f xss)+deriving instance (Ord (NP (NP f) xss)) => Ord (POP f xss)++-- | @since 0.4.0.0+instance (Semigroup (NP (NP f) xss)) => Semigroup (POP f xss) where+ POP xss <> POP yss = POP (xss <> yss)++-- | @since 0.4.0.0+instance (Monoid (NP (NP f) xss)) => Monoid (POP f xss) where+ mempty = POP mempty+ mappend (POP xss) (POP yss) = POP (mappend xss yss)++-- | @since 0.2.5.0+instance (NFData (NP (NP f) xss)) => NFData (POP f xss) where+ rnf (POP xss) = rnf xss++-- | Unwrap a product of products.+unPOP :: POP f xss -> NP (NP f) xss+unPOP (POP xss) = xss++type instance AllN NP c = All c+type instance AllN POP c = All2 c++type instance AllZipN NP c = AllZip c+type instance AllZipN POP c = AllZip2 c++type instance SListIN NP = SListI+type instance SListIN POP = SListI2++-- * Constructing products++-- | Specialization of 'hpure'.+--+-- The call @'pure_NP' x@ generates a product that contains 'x' in every+-- element position.+--+-- /Example:/+--+-- >>> pure_NP [] :: NP [] '[Char, Bool]+-- "" :* [] :* Nil+-- >>> pure_NP (K 0) :: NP (K Int) '[Double, Int, String]+-- K 0 :* K 0 :* K 0 :* Nil+--+pure_NP :: forall f xs. SListI xs => (forall a. f a) -> NP f xs+pure_NP f = cpure_NP topP f+{-# INLINE pure_NP #-}++-- | Specialization of 'hpure'.+--+-- The call @'pure_POP' x@ generates a product of products that contains 'x'+-- in every element position.+--+pure_POP :: All SListI xss => (forall a. f a) -> POP f xss+pure_POP f = cpure_POP topP f+{-# INLINE pure_POP #-}++topP :: Proxy Top+topP = Proxy++-- | Specialization of 'hcpure'.+--+-- The call @'cpure_NP' p x@ generates a product that contains 'x' in every+-- element position.+--+cpure_NP :: forall c xs proxy f. All c xs+ => proxy c -> (forall a. c a => f a) -> NP f xs+cpure_NP p f = case sList :: SList xs of+ SNil -> Nil+ SCons -> f :* cpure_NP p f++-- | Specialization of 'hcpure'.+--+-- The call @'cpure_NP' p x@ generates a product of products that contains 'x'+-- in every element position.+--+cpure_POP :: forall c xss proxy f. All2 c xss+ => proxy c -> (forall a. c a => f a) -> POP f xss+cpure_POP p f = POP (cpure_NP (allP p) (cpure_NP p f))++allP :: proxy c -> Proxy (All c)+allP _ = Proxy++instance HPure NP where+ hpure = pure_NP+ hcpure = cpure_NP++instance HPure POP where+ hpure = pure_POP+ hcpure = cpure_POP++-- ** Construction from a list++-- | Construct a homogeneous n-ary product from a normal Haskell list.+--+-- Returns 'Nothing' if the length of the list does not exactly match the+-- expected size of the product.+--+fromList :: SListI xs => [a] -> Maybe (NP (K a) xs)+fromList = go sList+ where+ go :: SList xs -> [a] -> Maybe (NP (K a) xs)+ go SNil [] = return Nil+ go SCons (x:xs) = do ys <- go sList xs ; return (K x :* ys)+ go _ _ = Nothing++-- * Application++-- | Specialization of 'hap'.+--+-- Applies a product of (lifted) functions pointwise to a product of+-- suitable arguments.+--+ap_NP :: NP (f -.-> g) xs -> NP f xs -> NP g xs+ap_NP Nil Nil = Nil+ap_NP (Fn f :* fs) (x :* xs) = f x :* ap_NP fs xs++-- | Specialization of 'hap'.+--+-- Applies a product of (lifted) functions pointwise to a product of+-- suitable arguments.+--+ap_POP :: POP (f -.-> g) xss -> POP f xss -> POP g xss+ap_POP (POP fss') (POP xss') = POP (go fss' xss')+ where+ go :: NP (NP (f -.-> g)) xss -> NP (NP f) xss -> NP (NP g) xss+ go Nil Nil = Nil+ go (fs :* fss) (xs :* xss) = ap_NP fs xs :* go fss xss++-- The definition of 'ap_POP' is a more direct variant of+-- '_ap_POP_spec'. The direct definition has the advantage+-- that it avoids the 'SListI' constraint.+_ap_POP_spec :: SListI xss => POP (f -.-> g) xss -> POP f xss -> POP g xss+_ap_POP_spec (POP fs) (POP xs) = POP (liftA2_NP ap_NP fs xs)++type instance Same NP = NP+type instance Same POP = POP++type instance Prod NP = NP+type instance Prod POP = POP++instance HAp NP where hap = ap_NP+instance HAp POP where hap = ap_POP++-- * Destructing products++-- | Obtain the head of an n-ary product.+--+-- @since 0.2.1.0+--+hd :: NP f (x ': xs) -> f x+hd (x :* _xs) = x++-- | Obtain the tail of an n-ary product.+--+-- @since 0.2.1.0+--+tl :: NP f (x ': xs) -> NP f xs+tl (_x :* xs) = xs++-- | The type of projections from an n-ary product.+--+-- A projection is a function from the n-ary product to a single element.+--+type Projection (f :: k -> Type) (xs :: [k]) = K (NP f xs) -.-> f++-- | Compute all projections from an n-ary product.+--+-- Each element of the resulting product contains one of the projections.+--+projections :: forall xs f . SListI xs => NP (Projection f xs) xs+projections = case sList :: SList xs of+ SNil -> Nil+ SCons -> fn (hd . unK) :* liftA_NP shiftProjection projections++shiftProjection :: Projection f xs a -> Projection f (x ': xs) a+shiftProjection (Fn f) = Fn $ f . K . tl . unK++-- * Lifting / mapping++-- | Specialization of 'hliftA'.+liftA_NP :: SListI xs => (forall a. f a -> g a) -> NP f xs -> NP g xs+-- | Specialization of 'hliftA'.+liftA_POP :: All SListI xss => (forall a. f a -> g a) -> POP f xss -> POP g xss++liftA_NP = hliftA+liftA_POP = hliftA++-- | Specialization of 'hliftA2'.+liftA2_NP :: SListI xs => (forall a. f a -> g a -> h a) -> NP f xs -> NP g xs -> NP h xs+-- | Specialization of 'hliftA2'.+liftA2_POP :: All SListI xss => (forall a. f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss++liftA2_NP = hliftA2+liftA2_POP = hliftA2++-- | Specialization of 'hliftA3'.+liftA3_NP :: SListI xs => (forall a. f a -> g a -> h a -> i a) -> NP f xs -> NP g xs -> NP h xs -> NP i xs+-- | Specialization of 'hliftA3'.+liftA3_POP :: All SListI xss => (forall a. f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss++liftA3_NP = hliftA3+liftA3_POP = hliftA3++-- | Specialization of 'hmap', which is equivalent to 'hliftA'.+map_NP :: SListI xs => (forall a. f a -> g a) -> NP f xs -> NP g xs+-- | Specialization of 'hmap', which is equivalent to 'hliftA'.+map_POP :: All SListI xss => (forall a. f a -> g a) -> POP f xss -> POP g xss++map_NP = hmap+map_POP = hmap++-- | Specialization of 'hzipWith', which is equivalent to 'hliftA2'.+zipWith_NP :: SListI xs => (forall a. f a -> g a -> h a) -> NP f xs -> NP g xs -> NP h xs+-- | Specialization of 'hzipWith', which is equivalent to 'hliftA2'.+zipWith_POP :: All SListI xss => (forall a. f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss++zipWith_NP = hzipWith+zipWith_POP = hzipWith++-- | Specialization of 'hzipWith3', which is equivalent to 'hliftA3'.+zipWith3_NP :: SListI xs => (forall a. f a -> g a -> h a -> i a) -> NP f xs -> NP g xs -> NP h xs -> NP i xs+-- | Specialization of 'hzipWith3', which is equivalent to 'hliftA3'.+zipWith3_POP :: All SListI xss => (forall a. f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss++zipWith3_NP = hzipWith3+zipWith3_POP = hzipWith3++-- | Specialization of 'hcliftA'.+cliftA_NP :: All c xs => proxy c -> (forall a. c a => f a -> g a) -> NP f xs -> NP g xs+-- | Specialization of 'hcliftA'.+cliftA_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> POP f xss -> POP g xss++cliftA_NP = hcliftA+cliftA_POP = hcliftA++-- | Specialization of 'hcliftA2'.+cliftA2_NP :: All c xs => proxy c -> (forall a. c a => f a -> g a -> h a) -> NP f xs -> NP g xs -> NP h xs+-- | Specialization of 'hcliftA2'.+cliftA2_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss++cliftA2_NP = hcliftA2+cliftA2_POP = hcliftA2++-- | Specialization of 'hcliftA3'.+cliftA3_NP :: All c xs => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> NP f xs -> NP g xs -> NP h xs -> NP i xs+-- | Specialization of 'hcliftA3'.+cliftA3_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss++cliftA3_NP = hcliftA3+cliftA3_POP = hcliftA3++-- | Specialization of 'hcmap', which is equivalent to 'hcliftA'.+cmap_NP :: All c xs => proxy c -> (forall a. c a => f a -> g a) -> NP f xs -> NP g xs+-- | Specialization of 'hcmap', which is equivalent to 'hcliftA'.+cmap_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> POP f xss -> POP g xss++cmap_NP = hcmap+cmap_POP = hcmap++-- | Specialization of 'hczipWith', which is equivalent to 'hcliftA2'.+czipWith_NP :: All c xs => proxy c -> (forall a. c a => f a -> g a -> h a) -> NP f xs -> NP g xs -> NP h xs+-- | Specialization of 'hczipWith', which is equivalent to 'hcliftA2'.+czipWith_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss++czipWith_NP = hczipWith+czipWith_POP = hczipWith++-- | Specialization of 'hczipWith3', which is equivalent to 'hcliftA3'.+czipWith3_NP :: All c xs => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> NP f xs -> NP g xs -> NP h xs -> NP i xs+-- | Specialization of 'hczipWith3', which is equivalent to 'hcliftA3'.+czipWith3_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss++czipWith3_NP = hczipWith3+czipWith3_POP = hczipWith3++-- * Dealing with @'All' c@++-- | Lift a constrained function operating on a list-indexed structure+-- to a function on a list-of-list-indexed structure.+--+-- This is a variant of 'hcliftA'.+--+-- /Specification:/+--+-- @+-- 'hcliftA'' p f xs = 'hpure' ('fn_2' $ \\ 'AllDictC' -> f) \` 'hap' \` 'allDict_NP' p \` 'hap' \` xs+-- @+--+-- /Instances:/+--+-- @+-- 'hcliftA'' :: 'All2' c xss => proxy c -> (forall xs. 'All' c xs => f xs -> f' xs) -> 'NP' f xss -> 'NP' f' xss+-- 'hcliftA'' :: 'All2' c xss => proxy c -> (forall xs. 'All' c xs => f xs -> f' xs) -> 'Data.SOP.NS.NS' f xss -> 'Data.SOP.NS.NS' f' xss+-- @+--+{-# DEPRECATED hcliftA' "Use 'hcliftA' or 'hcmap' instead." #-}+hcliftA' :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. All c xs => f xs -> f' xs) -> h f xss -> h f' xss++-- | Like 'hcliftA'', but for binary functions.+{-# DEPRECATED hcliftA2' "Use 'hcliftA2' or 'hczipWith' instead." #-}+hcliftA2' :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. All c xs => f xs -> f' xs -> f'' xs) -> Prod h f xss -> h f' xss -> h f'' xss++-- | Like 'hcliftA'', but for ternay functions.+{-# DEPRECATED hcliftA3' "Use 'hcliftA3' or 'hczipWith3' instead." #-}+hcliftA3' :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. All c xs => f xs -> f' xs -> f'' xs -> f''' xs) -> Prod h f xss -> Prod h f' xss -> h f'' xss -> h f''' xss++hcliftA' p = hcliftA (allP p)+hcliftA2' p = hcliftA2 (allP p)+hcliftA3' p = hcliftA3 (allP p)++-- | Specialization of 'hcliftA2''.+{-# DEPRECATED cliftA2'_NP "Use 'cliftA2_NP' instead." #-}+cliftA2'_NP :: All2 c xss => proxy c -> (forall xs. All c xs => f xs -> g xs -> h xs) -> NP f xss -> NP g xss -> NP h xss++cliftA2'_NP = hcliftA2'++-- * Collapsing++-- | Specialization of 'hcollapse'.+--+-- /Example:/+--+-- >>> collapse_NP (K 1 :* K 2 :* K 3 :* Nil)+-- [1,2,3]+--+collapse_NP :: NP (K a) xs -> [a]++-- | Specialization of 'hcollapse'.+--+-- /Example:/+--+-- >>> collapse_POP (POP ((K 'a' :* Nil) :* (K 'b' :* K 'c' :* Nil) :* Nil) :: POP (K Char) '[ '[(a :: Type)], '[b, c] ])+-- ["a","bc"]+--+-- (The type signature is only necessary in this case to fix the kind of the type variables.)+--+collapse_POP :: SListI xss => POP (K a) xss -> [[a]]++collapse_NP Nil = []+collapse_NP (K x :* xs) = x : collapse_NP xs++collapse_POP = collapse_NP . hliftA (K . collapse_NP) . unPOP++type instance CollapseTo NP a = [a]+type instance CollapseTo POP a = [[a]]++instance HCollapse NP where hcollapse = collapse_NP+instance HCollapse POP where hcollapse = collapse_POP++-- * Folding++-- | Specialization of 'hctraverse_'.+--+-- @since 0.3.2.0+--+ctraverse__NP ::+ forall c proxy xs f g. (All c xs, Applicative g)+ => proxy c -> (forall a. c a => f a -> g ()) -> NP f xs -> g ()+ctraverse__NP _ f = go+ where+ go :: All c ys => NP f ys -> g ()+ go Nil = pure ()+ go (x :* xs) = f x *> go xs++-- | Specialization of 'htraverse_'.+--+-- @since 0.3.2.0+--+traverse__NP ::+ forall xs f g. (SListI xs, Applicative g)+ => (forall a. f a -> g ()) -> NP f xs -> g ()+traverse__NP f =+ ctraverse__NP topP f+{-# INLINE traverse__NP #-}++-- | Specialization of 'hctraverse_'.+--+-- @since 0.3.2.0+--+ctraverse__POP ::+ forall c proxy xss f g. (All2 c xss, Applicative g)+ => proxy c -> (forall a. c a => f a -> g ()) -> POP f xss -> g ()+ctraverse__POP p f = ctraverse__NP (allP p) (ctraverse__NP p f) . unPOP++-- | Specialization of 'htraverse_'.+--+-- @since 0.3.2.0+--+traverse__POP ::+ forall xss f g. (SListI2 xss, Applicative g)+ => (forall a. f a -> g ()) -> POP f xss -> g ()+traverse__POP f =+ ctraverse__POP topP f+{-# INLINE traverse__POP #-}++instance HTraverse_ NP where+ hctraverse_ = ctraverse__NP+ htraverse_ = traverse__NP++instance HTraverse_ POP where+ hctraverse_ = ctraverse__POP+ htraverse_ = traverse__POP++-- | Specialization of 'hcfoldMap'.+--+-- @since 0.3.2.0+--+cfoldMap_NP :: (All c xs, Monoid m) => proxy c -> (forall a. c a => f a -> m) -> NP f xs -> m+cfoldMap_NP = hcfoldMap++-- | Specialization of 'hcfoldMap'.+--+-- @since 0.3.2.0+--+cfoldMap_POP :: (All2 c xs, Monoid m) => proxy c -> (forall a. c a => f a -> m) -> POP f xs -> m+cfoldMap_POP = hcfoldMap++-- * Sequencing++-- | Specialization of 'hsequence''.+sequence'_NP :: Applicative f => NP (f :.: g) xs -> f (NP g xs)+sequence'_NP Nil = pure Nil+sequence'_NP (mx :* mxs) = (:*) <$> unComp mx <*> sequence'_NP mxs++-- | Specialization of 'hsequence''.+sequence'_POP :: (SListI xss, Applicative f) => POP (f :.: g) xss -> f (POP g xss)+sequence'_POP = fmap POP . sequence'_NP . hliftA (Comp . sequence'_NP) . unPOP++-- | Specialization of 'hctraverse''.+--+-- @since 0.3.2.0+--+ctraverse'_NP ::+ forall c proxy xs f f' g. (All c xs, Applicative g)+ => proxy c -> (forall a. c a => f a -> g (f' a)) -> NP f xs -> g (NP f' xs)+ctraverse'_NP _ f = go where+ go :: All c ys => NP f ys -> g (NP f' ys)+ go Nil = pure Nil+ go (x :* xs) = (:*) <$> f x <*> go xs++-- | Specialization of 'htraverse''.+--+-- @since 0.3.2.0+--+traverse'_NP ::+ forall xs f f' g. (SListI xs, Applicative g)+ => (forall a. f a -> g (f' a)) -> NP f xs -> g (NP f' xs)+traverse'_NP f =+ ctraverse'_NP topP f+{-# INLINE traverse'_NP #-}++-- | Specialization of 'hctraverse''.+--+-- @since 0.3.2.0+--+ctraverse'_POP :: (All2 c xss, Applicative g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> POP f xss -> g (POP f' xss)+ctraverse'_POP p f = fmap POP . ctraverse'_NP (allP p) (ctraverse'_NP p f) . unPOP++-- | Specialization of 'hctraverse''.+--+-- @since 0.3.2.0+--+traverse'_POP :: (SListI2 xss, Applicative g) => (forall a. f a -> g (f' a)) -> POP f xss -> g (POP f' xss)+traverse'_POP f =+ ctraverse'_POP topP f+{-# INLINE traverse'_POP #-}++instance HSequence NP where+ hsequence' = sequence'_NP+ hctraverse' = ctraverse'_NP+ htraverse' = traverse'_NP++instance HSequence POP where+ hsequence' = sequence'_POP+ hctraverse' = ctraverse'_POP+ htraverse' = traverse'_POP++-- | Specialization of 'hsequence'.+--+-- /Example:/+--+-- >>> sequence_NP (Just 1 :* Just 2 :* Nil)+-- Just (I 1 :* I 2 :* Nil)+--+sequence_NP :: (SListI xs, Applicative f) => NP f xs -> f (NP I xs)++-- | Specialization of 'hsequence'.+--+-- /Example:/+--+-- >>> sequence_POP (POP ((Just 1 :* Nil) :* (Just 2 :* Just 3 :* Nil) :* Nil))+-- Just (POP ((I 1 :* Nil) :* (I 2 :* I 3 :* Nil) :* Nil))+--+sequence_POP :: (All SListI xss, Applicative f) => POP f xss -> f (POP I xss)++sequence_NP = hsequence+sequence_POP = hsequence++-- | Specialization of 'hctraverse'.+--+-- @since 0.3.2.0+--+ctraverse_NP :: (All c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> NP f xs -> g (NP I xs)++-- | Specialization of 'hctraverse'.+--+-- @since 0.3.2.0+--+ctraverse_POP :: (All2 c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> POP f xs -> g (POP I xs)++ctraverse_NP = hctraverse+ctraverse_POP = hctraverse++-- * Catamorphism and anamorphism++-- | Catamorphism for 'NP'.+--+-- This is a suitable generalization of 'foldr'. It takes+-- parameters on what to do for 'Nil' and ':*'. Since the+-- input list is heterogeneous, the result is also indexed+-- by a type-level list.+--+-- @since 0.2.3.0+--+cata_NP ::+ forall r f xs .+ r '[]+ -> (forall y ys . f y -> r ys -> r (y ': ys))+ -> NP f xs+ -> r xs+cata_NP nil cons = go+ where+ go :: forall ys . NP f ys -> r ys+ go Nil = nil+ go (x :* xs) = cons x (go xs)++-- | Constrained catamorphism for 'NP'.+--+-- The difference compared to 'cata_NP' is that the function+-- for the cons-case can make use of the fact that the specified+-- constraint holds for all the types in the signature of the+-- product.+--+-- @since 0.2.3.0+--+ccata_NP ::+ forall c proxy r f xs . (All c xs)+ => proxy c+ -> r '[]+ -> (forall y ys . c y => f y -> r ys -> r (y ': ys))+ -> NP f xs+ -> r xs+ccata_NP _ nil cons = go+ where+ go :: forall ys . (All c ys) => NP f ys -> r ys+ go Nil = nil+ go (x :* xs) = cons x (go xs)++-- | Anamorphism for 'NP'.+--+-- In contrast to the anamorphism for normal lists, the+-- generating function does not return an 'Either', but+-- simply an element and a new seed value.+--+-- This is because the decision on whether to generate a+-- 'Nil' or a ':*' is determined by the types.+--+-- @since 0.2.3.0+--+ana_NP ::+ forall s f xs .+ SListI xs+ => (forall y ys . s (y ': ys) -> (f y, s ys))+ -> s xs+ -> NP f xs+ana_NP uncons =+ cana_NP topP uncons+{-# INLINE ana_NP #-}++-- | Constrained anamorphism for 'NP'.+--+-- Compared to 'ana_NP', the generating function can+-- make use of the specified constraint here for the+-- elements that it generates.+--+-- @since 0.2.3.0+--+cana_NP ::+ forall c proxy s f xs . (All c xs)+ => proxy c+ -> (forall y ys . c y => s (y ': ys) -> (f y, s ys))+ -> s xs+ -> NP f xs+cana_NP _ uncons = go sList+ where+ go :: forall ys . (All c ys) => SList ys -> s ys -> NP f ys+ go SNil _ = Nil+ go SCons s = case uncons s of+ (x, s') -> x :* go sList s'++-- | Specialization of 'htrans'.+--+-- @since 0.3.1.0+--+trans_NP ::+ AllZip c xs ys+ => proxy c+ -> (forall x y . c x y => f x -> g y)+ -> NP f xs -> NP g ys+trans_NP _ _t Nil = Nil+trans_NP p t (x :* xs) = t x :* trans_NP p t xs++-- | Specialization of 'htrans'.+--+-- @since 0.3.1.0+--+trans_POP ::+ AllZip2 c xss yss+ => proxy c+ -> (forall x y . c x y => f x -> g y)+ -> POP f xss -> POP g yss+trans_POP p t =+ POP . trans_NP (allZipP p) (trans_NP p t) . unPOP++allZipP :: proxy c -> Proxy (AllZip c)+allZipP _ = Proxy++-- | Specialization of 'hcoerce'.+--+-- @since 0.3.1.0+--+coerce_NP ::+ forall f g xs ys .+ AllZip (LiftedCoercible f g) xs ys+ => NP f xs -> NP g ys+coerce_NP =+ unsafeCoerce++-- | Safe version of 'coerce_NP'.+--+-- For documentation purposes only; not exported.+--+_safe_coerce_NP ::+ forall f g xs ys .+ AllZip (LiftedCoercible f g) xs ys+ => NP f xs -> NP g ys+_safe_coerce_NP =+ trans_NP (Proxy :: Proxy (LiftedCoercible f g)) coerce++-- | Specialization of 'hcoerce'.+--+-- @since 0.3.1.0+--+coerce_POP ::+ forall f g xss yss .+ AllZip2 (LiftedCoercible f g) xss yss+ => POP f xss -> POP g yss+coerce_POP =+ unsafeCoerce++-- | Safe version of 'coerce_POP'.+--+-- For documentation purposes only; not exported.+--+_safe_coerce_POP ::+ forall f g xss yss .+ AllZip2 (LiftedCoercible f g) xss yss+ => POP f xss -> POP g yss+_safe_coerce_POP =+ trans_POP (Proxy :: Proxy (LiftedCoercible f g)) coerce++-- | Specialization of 'hfromI'.+--+-- @since 0.3.1.0+--+fromI_NP ::+ forall f xs ys .+ AllZip (LiftedCoercible I f) xs ys+ => NP I xs -> NP f ys+fromI_NP = hfromI++-- | Specialization of 'htoI'.+--+-- @since 0.3.1.0+--+toI_NP ::+ forall f xs ys .+ AllZip (LiftedCoercible f I) xs ys+ => NP f xs -> NP I ys+toI_NP = htoI++-- | Specialization of 'hfromI'.+--+-- @since 0.3.1.0+--+fromI_POP ::+ forall f xss yss .+ AllZip2 (LiftedCoercible I f) xss yss+ => POP I xss -> POP f yss+fromI_POP = hfromI++-- | Specialization of 'htoI'.+--+-- @since 0.3.1.0+--+toI_POP ::+ forall f xss yss .+ AllZip2 (LiftedCoercible f I) xss yss+ => POP f xss -> POP I yss+toI_POP = htoI++instance HTrans NP NP where+ htrans = trans_NP+ hcoerce = coerce_NP+instance HTrans POP POP where+ htrans = trans_POP+ hcoerce = coerce_POP
+ src/Data/SOP/NS.hs view
@@ -0,0 +1,980 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-deprecations #-}+-- | n-ary sums (and sums of products)+module Data.SOP.NS+ ( -- * Datatypes+ NS(..)+ , SOP(..)+ , unSOP+ -- * Constructing sums+ , Injection+ , injections+ , shift+ , shiftInjection+ , apInjs_NP+ , apInjs'_NP+ , apInjs_POP+ , apInjs'_POP+ -- * Destructing sums+ , unZ+ , index_NS+ , index_SOP+ -- * Application+ , ap_NS+ , ap_SOP+ -- * Lifting / mapping+ , liftA_NS+ , liftA_SOP+ , liftA2_NS+ , liftA2_SOP+ , cliftA_NS+ , cliftA_SOP+ , cliftA2_NS+ , cliftA2_SOP+ , map_NS+ , map_SOP+ , cmap_NS+ , cmap_SOP+ -- * Dealing with @'All' c@+ , cliftA2'_NS+ -- * Comparison+ , compare_NS+ , ccompare_NS+ , compare_SOP+ , ccompare_SOP+ -- * Collapsing+ , collapse_NS+ , collapse_SOP+ -- * Folding and sequencing+ , ctraverse__NS+ , ctraverse__SOP+ , traverse__NS+ , traverse__SOP+ , cfoldMap_NS+ , cfoldMap_SOP+ , sequence'_NS+ , sequence'_SOP+ , sequence_NS+ , sequence_SOP+ , ctraverse'_NS+ , ctraverse'_SOP+ , traverse'_NS+ , traverse'_SOP+ , ctraverse_NS+ , ctraverse_SOP+ -- * Catamorphism and anamorphism+ , cata_NS+ , ccata_NS+ , ana_NS+ , cana_NS+ -- * Expanding sums to products+ , expand_NS+ , cexpand_NS+ , expand_SOP+ , cexpand_SOP+ -- * Transformation of index lists and coercions+ , trans_NS+ , trans_SOP+ , coerce_NS+ , coerce_SOP+ , fromI_NS+ , fromI_SOP+ , toI_NS+ , toI_SOP+ ) where++import Data.Coerce+import Data.Kind (Type)+import Data.Proxy (Proxy (..))+import Unsafe.Coerce++import Control.DeepSeq (NFData(..))++import Data.SOP.BasicFunctors+import Data.SOP.Classes+import Data.SOP.Constraint+import Data.SOP.NP+import Data.SOP.Sing++-- * Datatypes++-- | An n-ary sum.+--+-- The sum is parameterized by a type constructor @f@ and+-- indexed by a type-level list @xs@. The length of the list+-- determines the number of choices in the sum and if the+-- @i@-th element of the list is of type @x@, then the @i@-th+-- choice of the sum is of type @f x@.+--+-- The constructor names are chosen to resemble Peano-style+-- natural numbers, i.e., 'Z' is for "zero", and 'S' is for+-- "successor". Chaining 'S' and 'Z' chooses the corresponding+-- component of the sum.+--+-- /Examples:/+--+-- > Z :: f x -> NS f (x ': xs)+-- > S . Z :: f y -> NS f (x ': y ': xs)+-- > S . S . Z :: f z -> NS f (x ': y ': z ': xs)+-- > ...+--+-- Note that empty sums (indexed by an empty list) have no+-- non-bottom elements.+--+-- Two common instantiations of @f@ are the identity functor 'I'+-- and the constant functor 'K'. For 'I', the sum becomes a+-- direct generalization of the 'Either' type to arbitrarily many+-- choices. For @'K' a@, the result is a homogeneous choice type,+-- where the contents of the type-level list are ignored, but its+-- length specifies the number of options.+--+-- In the context of the SOP approach to generic programming, an+-- n-ary sum describes the top-level structure of a datatype,+-- which is a choice between all of its constructors.+--+-- /Examples:/+--+-- > Z (I 'x') :: NS I '[ Char, Bool ]+-- > S (Z (I True)) :: NS I '[ Char, Bool ]+-- > S (Z (K 1)) :: NS (K Int) '[ Char, Bool ]+--+data NS :: (k -> Type) -> [k] -> Type where+ Z :: f x -> NS f (x ': xs)+ S :: NS f xs -> NS f (x ': xs)++deriving instance All (Show `Compose` f) xs => Show (NS f xs)+deriving instance All (Eq `Compose` f) xs => Eq (NS f xs)+deriving instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NS f xs)++-- | @since 0.2.5.0+instance All (NFData `Compose` f) xs => NFData (NS f xs) where+ rnf (Z x) = rnf x+ rnf (S xs) = rnf xs++-- | Extract the payload from a unary sum.+--+-- For larger sums, this function would be partial, so it is only+-- provided with a rather restrictive type.+--+-- /Example:/+--+-- >>> unZ (Z (I 'x'))+-- I 'x'+--+-- @since 0.2.2.0+--+unZ :: NS f '[x] -> f x+unZ (Z x) = x+unZ (S x) = case x of {}++-- | Obtain the index from an n-ary sum.+--+-- An n-nary sum represents a choice between n different options.+-- This function returns an integer between 0 and n - 1 indicating+-- the option chosen by the given value.+--+-- /Examples:/+--+-- >>> index_NS (S (S (Z (I False))))+-- 2+-- >>> index_NS (Z (K ()))+-- 0+--+-- @since 0.2.4.0+--+index_NS :: forall f xs . NS f xs -> Int+index_NS = go 0+ where+ go :: forall ys . Int -> NS f ys -> Int+ go !acc (Z _) = acc+ go !acc (S x) = go (acc + 1) x++instance HIndex NS where+ hindex = index_NS++-- | A sum of products.+--+-- This is a 'newtype' for an 'NS' of an 'NP'. The elements of the+-- (inner) products are applications of the parameter @f@. The type+-- 'SOP' is indexed by the list of lists that determines the sizes+-- of both the (outer) sum and all the (inner) products, as well as+-- the types of all the elements of the inner products.+--+-- An @'SOP' 'I'@ reflects the structure of a normal Haskell datatype.+-- The sum structure represents the choice between the different+-- constructors, the product structure represents the arguments of+-- each constructor.+--+newtype SOP (f :: (k -> Type)) (xss :: [[k]]) = SOP (NS (NP f) xss)++deriving instance (Show (NS (NP f) xss)) => Show (SOP f xss)+deriving instance (Eq (NS (NP f) xss)) => Eq (SOP f xss)+deriving instance (Ord (NS (NP f) xss)) => Ord (SOP f xss)++-- | @since 0.2.5.0+instance (NFData (NS (NP f) xss)) => NFData (SOP f xss) where+ rnf (SOP xss) = rnf xss++-- | Unwrap a sum of products.+unSOP :: SOP f xss -> NS (NP f) xss+unSOP (SOP xss) = xss++type instance AllN NS c = All c+type instance AllN SOP c = All2 c++-- | Obtain the index from an n-ary sum of products.+--+-- An n-nary sum represents a choice between n different options.+-- This function returns an integer between 0 and n - 1 indicating+-- the option chosen by the given value.+--+-- /Specification:/+--+-- @+-- 'index_SOP' = 'index_NS' '.' 'unSOP'+-- @+--+-- /Example:/+--+-- >>> index_SOP (SOP (S (Z (I True :* I 'x' :* Nil))))+-- 1+--+-- @since 0.2.4.0+--+index_SOP :: SOP f xs -> Int+index_SOP = index_NS . unSOP++instance HIndex SOP where+ hindex = index_SOP++-- * Constructing sums++-- | The type of injections into an n-ary sum.+--+-- If you expand the type synonyms and newtypes involved, you get+--+-- > Injection f xs a = (f -.-> K (NS f xs)) a ~= f a -> K (NS f xs) a ~= f a -> NS f xs+--+-- If we pick @a@ to be an element of @xs@, this indeed corresponds to an+-- injection into the sum.+--+type Injection (f :: k -> Type) (xs :: [k]) = f -.-> K (NS f xs)++-- | Compute all injections into an n-ary sum.+--+-- Each element of the resulting product contains one of the injections.+--+injections :: forall xs f. SListI xs => NP (Injection f xs) xs+injections = case sList :: SList xs of+ SNil -> Nil+ SCons -> fn (K . Z) :* liftA_NP shiftInjection injections++-- | Shift an injection.+--+-- Given an injection, return an injection into a sum that is one component larger.+--+shiftInjection :: Injection f xs a -> Injection f (x ': xs) a+shiftInjection (Fn f) = Fn $ K . S . unK . f++{-# DEPRECATED shift "Use 'shiftInjection' instead." #-}+-- | Shift an injection.+--+-- Given an injection, return an injection into a sum that is one component larger.+--+shift :: Injection f xs a -> Injection f (x ': xs) a+shift = shiftInjection++-- | Apply injections to a product.+--+-- Given a product containing all possible choices, produce a+-- list of sums by applying each injection to the appropriate+-- element.+--+-- /Example:/+--+-- >>> apInjs_NP (I 'x' :* I True :* I 2 :* Nil)+-- [Z (I 'x'),S (Z (I True)),S (S (Z (I 2)))]+--+apInjs_NP :: SListI xs => NP f xs -> [NS f xs]+apInjs_NP = hcollapse . apInjs'_NP++-- | `apInjs_NP` without `hcollapse`.+--+-- >>> apInjs'_NP (I 'x' :* I True :* I 2 :* Nil)+-- K (Z (I 'x')) :* K (S (Z (I True))) :* K (S (S (Z (I 2)))) :* Nil+--+-- @since 0.2.5.0+--+apInjs'_NP :: SListI xs => NP f xs -> NP (K (NS f xs)) xs+apInjs'_NP = hap injections++-- | Apply injections to a product of product.+--+-- This operates on the outer product only. Given a product+-- containing all possible choices (that are products),+-- produce a list of sums (of products) by applying each+-- injection to the appropriate element.+--+-- /Example:/+--+-- >>> apInjs_POP (POP ((I 'x' :* Nil) :* (I True :* I 2 :* Nil) :* Nil))+-- [SOP (Z (I 'x' :* Nil)),SOP (S (Z (I True :* I 2 :* Nil)))]+--+apInjs_POP :: SListI xss => POP f xss -> [SOP f xss]+apInjs_POP = map SOP . apInjs_NP . unPOP++-- | `apInjs_POP` without `hcollapse`.+--+-- /Example:/+--+-- >>> apInjs'_POP (POP ((I 'x' :* Nil) :* (I True :* I 2 :* Nil) :* Nil))+-- K (SOP (Z (I 'x' :* Nil))) :* K (SOP (S (Z (I True :* I 2 :* Nil)))) :* Nil+--+-- @since 0.2.5.0+--+apInjs'_POP :: SListI xss => POP f xss -> NP (K (SOP f xss)) xss+apInjs'_POP = hmap (K . SOP . unK) . hap injections . unPOP++type instance UnProd NP = NS+type instance UnProd POP = SOP++instance HApInjs NS where+ hapInjs = apInjs_NP++instance HApInjs SOP where+ hapInjs = apInjs_POP++-- * Application++-- | Specialization of 'hap'.+ap_NS :: NP (f -.-> g) xs -> NS f xs -> NS g xs+ap_NS (Fn f :* _) (Z x) = Z (f x)+ap_NS (_ :* fs) (S xs) = S (ap_NS fs xs)+ap_NS Nil x = case x of {}++-- | Specialization of 'hap'.+ap_SOP :: POP (f -.-> g) xss -> SOP f xss -> SOP g xss+ap_SOP (POP fss') (SOP xss') = SOP (go fss' xss')+ where+ go :: NP (NP (f -.-> g)) xss -> NS (NP f) xss -> NS (NP g) xss+ go (fs :* _ ) (Z xs ) = Z (ap_NP fs xs )+ go (_ :* fss) (S xss) = S (go fss xss)+ go Nil x = case x of {}++-- The definition of 'ap_SOP' is a more direct variant of+-- '_ap_SOP_spec'. The direct definition has the advantage+-- that it avoids the 'SListI' constraint.+_ap_SOP_spec :: SListI xss => POP (t -.-> f) xss -> SOP t xss -> SOP f xss+_ap_SOP_spec (POP fs) (SOP xs) = SOP (liftA2_NS ap_NP fs xs)++type instance Same NS = NS+type instance Same SOP = SOP++type instance Prod NS = NP+type instance Prod SOP = POP++type instance SListIN NS = SListI+type instance SListIN SOP = SListI2++instance HAp NS where hap = ap_NS+instance HAp SOP where hap = ap_SOP++-- * Lifting / mapping++-- | Specialization of 'hliftA'.+liftA_NS :: SListI xs => (forall a. f a -> g a) -> NS f xs -> NS g xs+-- | Specialization of 'hliftA'.+liftA_SOP :: All SListI xss => (forall a. f a -> g a) -> SOP f xss -> SOP g xss++liftA_NS = hliftA+liftA_SOP = hliftA++-- | Specialization of 'hliftA2'.+liftA2_NS :: SListI xs => (forall a. f a -> g a -> h a) -> NP f xs -> NS g xs -> NS h xs+-- | Specialization of 'hliftA2'.+liftA2_SOP :: All SListI xss => (forall a. f a -> g a -> h a) -> POP f xss -> SOP g xss -> SOP h xss++liftA2_NS = hliftA2+liftA2_SOP = hliftA2++-- | Specialization of 'hmap', which is equivalent to 'hliftA'.+map_NS :: SListI xs => (forall a. f a -> g a) -> NS f xs -> NS g xs+-- | Specialization of 'hmap', which is equivalent to 'hliftA'.+map_SOP :: All SListI xss => (forall a. f a -> g a) -> SOP f xss -> SOP g xss++map_NS = hmap+map_SOP = hmap++-- | Specialization of 'hcliftA'.+cliftA_NS :: All c xs => proxy c -> (forall a. c a => f a -> g a) -> NS f xs -> NS g xs+-- | Specialization of 'hcliftA'.+cliftA_SOP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> SOP f xss -> SOP g xss++cliftA_NS = hcliftA+cliftA_SOP = hcliftA++-- | Specialization of 'hcliftA2'.+cliftA2_NS :: All c xs => proxy c -> (forall a. c a => f a -> g a -> h a) -> NP f xs -> NS g xs -> NS h xs+-- | Specialization of 'hcliftA2'.+cliftA2_SOP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a) -> POP f xss -> SOP g xss -> SOP h xss++cliftA2_NS = hcliftA2+cliftA2_SOP = hcliftA2++-- | Specialization of 'hcmap', which is equivalent to 'hcliftA'.+cmap_NS :: All c xs => proxy c -> (forall a. c a => f a -> g a) -> NS f xs -> NS g xs+-- | Specialization of 'hcmap', which is equivalent to 'hcliftA'.+cmap_SOP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> SOP f xss -> SOP g xss++cmap_NS = hcmap+cmap_SOP = hcmap++-- * Dealing with @'All' c@++-- | Specialization of 'hcliftA2''.+{-# DEPRECATED cliftA2'_NS "Use 'cliftA2_NS' instead." #-}+cliftA2'_NS :: All2 c xss => proxy c -> (forall xs. All c xs => f xs -> g xs -> h xs) -> NP f xss -> NS g xss -> NS h xss++cliftA2'_NS = hcliftA2'++-- * Comparison++-- | Compare two sums with respect to the choice they+-- are making.+--+-- A value that chooses the first option+-- is considered smaller than one that chooses the second+-- option.+--+-- If the choices are different, then either the first+-- (if the first is smaller than the second)+-- or the third (if the first is larger than the second)+-- argument are called. If both choices are equal, then the+-- second argument is called, which has access to the+-- elements contained in the sums.+--+-- @since 0.3.2.0+--+compare_NS ::+ forall r f g xs .+ r -- ^ what to do if first is smaller+ -> (forall x . f x -> g x -> r) -- ^ what to do if both are equal+ -> r -- ^ what to do if first is larger+ -> NS f xs -> NS g xs+ -> r+compare_NS lt eq gt = go+ where+ go :: forall ys . NS f ys -> NS g ys -> r+ go (Z x) (Z y) = eq x y+ go (Z _) (S _) = lt+ go (S _) (Z _) = gt+ go (S xs) (S ys) = go xs ys+--+-- NOTE: The above could be written in terms of+-- ccompare_NS, but the direct definition avoids the+-- SListI constraint. We may change this in the future.++-- | Constrained version of 'compare_NS'.+--+-- @since 0.3.2.0+--+ccompare_NS ::+ forall c proxy r f g xs .+ (All c xs)+ => proxy c+ -> r -- ^ what to do if first is smaller+ -> (forall x . c x => f x -> g x -> r) -- ^ what to do if both are equal+ -> r -- ^ what to do if first is larger+ -> NS f xs -> NS g xs+ -> r+ccompare_NS _ lt eq gt = go+ where+ go :: forall ys . (All c ys) => NS f ys -> NS g ys -> r+ go (Z x) (Z y) = eq x y+ go (Z _) (S _) = lt+ go (S _) (Z _) = gt+ go (S xs) (S ys) = go xs ys++-- | Compare two sums of products with respect to the+-- choice in the sum they are making.+--+-- Only the sum structure is used for comparison.+-- This is a small wrapper around 'ccompare_NS' for+-- a common special case.+--+-- @since 0.3.2.0+--+compare_SOP ::+ forall r f g xss .+ r -- ^ what to do if first is smaller+ -> (forall xs . NP f xs -> NP g xs -> r) -- ^ what to do if both are equal+ -> r -- ^ what to do if first is larger+ -> SOP f xss -> SOP g xss+ -> r+compare_SOP lt eq gt (SOP xs) (SOP ys) =+ compare_NS lt eq gt xs ys++-- | Constrained version of 'compare_SOP'.+--+-- @since 0.3.2.0+--+ccompare_SOP ::+ forall c proxy r f g xss .+ (All2 c xss)+ => proxy c+ -> r -- ^ what to do if first is smaller+ -> (forall xs . All c xs => NP f xs -> NP g xs -> r) -- ^ what to do if both are equal+ -> r -- ^ what to do if first is larger+ -> SOP f xss -> SOP g xss+ -> r+ccompare_SOP p lt eq gt (SOP xs) (SOP ys) =+ ccompare_NS (allP p) lt eq gt xs ys++-- * Collapsing++-- | Specialization of 'hcollapse'.+collapse_NS :: NS (K a) xs -> a+-- | Specialization of 'hcollapse'.+collapse_SOP :: SListI xss => SOP (K a) xss -> [a]++collapse_NS (Z (K x)) = x+collapse_NS (S xs) = collapse_NS xs++collapse_SOP = collapse_NS . hliftA (K . collapse_NP) . unSOP++type instance CollapseTo NS a = a+type instance CollapseTo SOP a = [a]++instance HCollapse NS where hcollapse = collapse_NS+instance HCollapse SOP where hcollapse = collapse_SOP++-- * Folding++-- | Specialization of 'hctraverse_'.+--+-- /Note:/ we don't need 'Applicative' constraint.+--+-- @since 0.3.2.0+--+ctraverse__NS ::+ forall c proxy xs f g. (All c xs)+ => proxy c -> (forall a. c a => f a -> g ()) -> NS f xs -> g ()+ctraverse__NS _ f = go+ where+ go :: All c ys => NS f ys -> g ()+ go (Z x) = f x+ go (S xs) = go xs++-- | Specialization of 'htraverse_'.+--+-- /Note:/ we don't need 'Applicative' constraint.+--+-- @since 0.3.2.0+--+traverse__NS ::+ forall xs f g. (SListI xs)+ => (forall a. f a -> g ()) -> NS f xs -> g ()+traverse__NS f = go+ where+ go :: NS f ys -> g ()+ go (Z x) = f x+ go (S xs) = go xs++-- | Specialization of 'hctraverse_'.+--+-- @since 0.3.2.0+--+ctraverse__SOP ::+ forall c proxy xss f g. (All2 c xss, Applicative g)+ => proxy c -> (forall a. c a => f a -> g ()) -> SOP f xss -> g ()+ctraverse__SOP p f = ctraverse__NS (allP p) (ctraverse__NP p f) . unSOP++-- | Specialization of 'htraverse_'.+--+-- @since 0.3.2.0+--+traverse__SOP ::+ forall xss f g. (SListI2 xss, Applicative g)+ => (forall a. f a -> g ()) -> SOP f xss -> g ()+traverse__SOP f =+ ctraverse__SOP topP f+{-# INLINE traverse__SOP #-}++topP :: Proxy Top+topP = Proxy++instance HTraverse_ NS where+ hctraverse_ = ctraverse__NS+ htraverse_ = traverse__NS++instance HTraverse_ SOP where+ hctraverse_ = ctraverse__SOP+ htraverse_ = traverse__SOP++-- | Specialization of 'hcfoldMap'.+--+-- /Note:/ We don't need 'Monoid' instance.+--+-- @since 0.3.2.0+--+cfoldMap_NS ::+ forall c proxy f xs m. (All c xs)+ => proxy c -> (forall a. c a => f a -> m) -> NS f xs -> m+cfoldMap_NS _ f = go+ where+ go :: All c ys => NS f ys -> m+ go (Z x) = f x+ go (S xs) = go xs++-- | Specialization of 'hcfoldMap'.+--+-- @since 0.3.2.0+--+cfoldMap_SOP :: (All2 c xs, Monoid m) => proxy c -> (forall a. c a => f a -> m) -> SOP f xs -> m+cfoldMap_SOP = hcfoldMap++-- * Sequencing++-- | Specialization of 'hsequence''.+sequence'_NS :: Applicative f => NS (f :.: g) xs -> f (NS g xs)+sequence'_NS (Z mx) = Z <$> unComp mx+sequence'_NS (S mxs) = S <$> sequence'_NS mxs++-- | Specialization of 'hsequence''.+sequence'_SOP :: (SListI xss, Applicative f) => SOP (f :.: g) xss -> f (SOP g xss)+sequence'_SOP = fmap SOP . sequence'_NS . hliftA (Comp . sequence'_NP) . unSOP++-- | Specialization of 'hctraverse''.+--+-- /Note:/ as 'NS' has exactly one element, the 'Functor' constraint is enough.+--+-- @since 0.3.2.0+--+ctraverse'_NS ::+ forall c proxy xs f f' g. (All c xs, Functor g)+ => proxy c -> (forall a. c a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs)+ctraverse'_NS _ f = go where+ go :: All c ys => NS f ys -> g (NS f' ys)+ go (Z x) = Z <$> f x+ go (S xs) = S <$> go xs++-- | Specialization of 'htraverse''.+--+-- /Note:/ as 'NS' has exactly one element, the 'Functor' constraint is enough.+--+-- @since 0.3.2.0+--+traverse'_NS ::+ forall xs f f' g. (SListI xs, Functor g)+ => (forall a. f a -> g (f' a)) -> NS f xs -> g (NS f' xs)+traverse'_NS f =+ ctraverse'_NS topP f+{-# INLINE traverse'_NS #-}++-- | Specialization of 'hctraverse''.+--+-- @since 0.3.2.0+--+ctraverse'_SOP :: (All2 c xss, Applicative g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> SOP f xss -> g (SOP f' xss)+ctraverse'_SOP p f = fmap SOP . ctraverse'_NS (allP p) (ctraverse'_NP p f) . unSOP++-- | Specialization of 'htraverse''.+--+-- @since 0.3.2.0+--+traverse'_SOP :: (SListI2 xss, Applicative g) => (forall a. f a -> g (f' a)) -> SOP f xss -> g (SOP f' xss)+traverse'_SOP f =+ ctraverse'_SOP topP f+{-# INLINE traverse'_SOP #-}++instance HSequence NS where+ hsequence' = sequence'_NS+ hctraverse' = ctraverse'_NS+ htraverse' = traverse'_NS++instance HSequence SOP where+ hsequence' = sequence'_SOP+ hctraverse' = ctraverse'_SOP+ htraverse' = traverse'_SOP++-- | Specialization of 'hsequence'.+sequence_NS :: (SListI xs, Applicative f) => NS f xs -> f (NS I xs)++-- | Specialization of 'hsequence'.+sequence_SOP :: (All SListI xss, Applicative f) => SOP f xss -> f (SOP I xss)++sequence_NS = hsequence+sequence_SOP = hsequence++-- | Specialization of 'hctraverse'.+--+-- @since 0.3.2.0+--+ctraverse_NS :: (All c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> NP f xs -> g (NP I xs)++-- | Specialization of 'hctraverse'.+--+-- @since 0.3.2.0+--+ctraverse_SOP :: (All2 c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> POP f xs -> g (POP I xs)++ctraverse_NS = hctraverse+ctraverse_SOP = hctraverse++-- * Catamorphism and anamorphism++-- | Catamorphism for 'NS'.+--+-- Takes arguments determining what to do for 'Z'+-- and what to do for 'S'. The result type is still+-- indexed over the type-level lit.+--+-- @since 0.2.3.0+--+cata_NS ::+ forall r f xs .+ (forall y ys . f y -> r (y ': ys))+ -> (forall y ys . r ys -> r (y ': ys))+ -> NS f xs+ -> r xs+cata_NS z s = go+ where+ go :: forall ys . NS f ys -> r ys+ go (Z x) = z x+ go (S i) = s (go i)++-- | Constrained catamorphism for 'NS'.+--+-- @since 0.2.3.0+--+ccata_NS ::+ forall c proxy r f xs . (All c xs)+ => proxy c+ -> (forall y ys . c y => f y -> r (y ': ys))+ -> (forall y ys . c y => r ys -> r (y ': ys))+ -> NS f xs+ -> r xs+ccata_NS _ z s = go+ where+ go :: forall ys . (All c ys) => NS f ys -> r ys+ go (Z x) = z x+ go (S i) = s (go i)++-- | Anamorphism for 'NS'.+--+-- @since 0.2.3.0+--+ana_NS ::+ forall s f xs . (SListI xs)+ => (forall r . s '[] -> r)+ -> (forall y ys . s (y ': ys) -> Either (f y) (s ys))+ -> s xs+ -> NS f xs+ana_NS refute decide =+ cana_NS topP refute decide+{-# INLINE ana_NS #-}++-- | Constrained anamorphism for 'NS'.+--+-- @since 0.2.3.0+--+cana_NS :: forall c proxy s f xs .+ (All c xs)+ => proxy c+ -> (forall r . s '[] -> r)+ -> (forall y ys . c y => s (y ': ys) -> Either (f y) (s ys))+ -> s xs+ -> NS f xs+cana_NS _ refute decide = go sList+ where+ go :: forall ys . (All c ys) => SList ys -> s ys -> NS f ys+ go SNil s = refute s+ go SCons s = case decide s of+ Left x -> Z x+ Right s' -> S (go sList s')++-- * Expanding sums to products++-- | Specialization of 'hexpand'.+--+-- @since 0.2.5.0+--+expand_NS :: forall f xs .+ (SListI xs)+ => (forall x . f x)+ -> NS f xs -> NP f xs+expand_NS d =+ cexpand_NS topP d+{-# INLINE expand_NS #-}++-- | Specialization of 'hcexpand'.+--+-- @since 0.2.5.0+--+cexpand_NS :: forall c proxy f xs .+ (All c xs)+ => proxy c -> (forall x . c x => f x)+ -> NS f xs -> NP f xs+cexpand_NS p d = go+ where+ go :: forall ys . All c ys => NS f ys -> NP f ys+ go (Z x) = x :* hcpure p d+ go (S i) = d :* go i++-- | Specialization of 'hexpand'.+--+-- @since 0.2.5.0+--+expand_SOP :: forall f xss .+ (All SListI xss)+ => (forall x . f x)+ -> SOP f xss -> POP f xss+expand_SOP d =+ cexpand_SOP topP d+{-# INLINE cexpand_SOP #-}++-- | Specialization of 'hcexpand'.+--+-- @since 0.2.5.0+--+cexpand_SOP :: forall c proxy f xss .+ (All2 c xss)+ => proxy c -> (forall x . c x => f x)+ -> SOP f xss -> POP f xss+cexpand_SOP p d =+ POP . cexpand_NS (allP p) (hcpure p d) . unSOP++allP :: proxy c -> Proxy (All c)+allP _ = Proxy++instance HExpand NS where+ hexpand = expand_NS+ hcexpand = cexpand_NS++instance HExpand SOP where+ hexpand = expand_SOP+ hcexpand = cexpand_SOP++-- | Specialization of 'htrans'.+--+-- @since 0.3.1.0+--+trans_NS ::+ AllZip c xs ys+ => proxy c+ -> (forall x y . c x y => f x -> g y)+ -> NS f xs -> NS g ys+trans_NS _ t (Z x) = Z (t x)+trans_NS p t (S x) = S (trans_NS p t x)++-- | Specialization of 'htrans'.+--+-- @since 0.3.1.0+--+trans_SOP ::+ AllZip2 c xss yss+ => proxy c+ -> (forall x y . c x y => f x -> g y)+ -> SOP f xss -> SOP g yss+trans_SOP p t =+ SOP . trans_NS (allZipP p) (trans_NP p t) . unSOP++allZipP :: proxy c -> Proxy (AllZip c)+allZipP _ = Proxy++-- | Specialization of 'hcoerce'.+--+-- @since 0.3.1.0+--+coerce_NS ::+ forall f g xs ys .+ AllZip (LiftedCoercible f g) xs ys+ => NS f xs -> NS g ys+coerce_NS =+ unsafeCoerce++-- | Safe version of 'coerce_NS'.+--+-- For documentation purposes only; not exported.+--+_safe_coerce_NS ::+ forall f g xs ys .+ AllZip (LiftedCoercible f g) xs ys+ => NS f xs -> NS g ys+_safe_coerce_NS =+ trans_NS (Proxy :: Proxy (LiftedCoercible f g)) coerce++-- | Specialization of 'hcoerce'.+--+-- @since 0.3.1.0+--+coerce_SOP ::+ forall f g xss yss .+ AllZip2 (LiftedCoercible f g) xss yss+ => SOP f xss -> SOP g yss+coerce_SOP =+ unsafeCoerce++-- | Safe version of 'coerce_SOP'.+--+-- For documentation purposes only; not exported.+--+_safe_coerce_SOP ::+ forall f g xss yss .+ AllZip2 (LiftedCoercible f g) xss yss+ => SOP f xss -> SOP g yss+_safe_coerce_SOP =+ trans_SOP (Proxy :: Proxy (LiftedCoercible f g)) coerce++-- | Specialization of 'hfromI'.+--+-- @since 0.3.1.0+--+fromI_NS ::+ forall f xs ys .+ AllZip (LiftedCoercible I f) xs ys+ => NS I xs -> NS f ys+fromI_NS = hfromI++-- | Specialization of 'htoI'.+--+-- @since 0.3.1.0+--+toI_NS ::+ forall f xs ys .+ AllZip (LiftedCoercible f I) xs ys+ => NS f xs -> NS I ys+toI_NS = htoI++-- | Specialization of 'hfromI'.+--+-- @since 0.3.1.0+--+fromI_SOP ::+ forall f xss yss .+ AllZip2 (LiftedCoercible I f) xss yss+ => SOP I xss -> SOP f yss+fromI_SOP = hfromI++-- | Specialization of 'htoI'.+--+-- @since 0.3.1.0+--+toI_SOP ::+ forall f xss yss .+ AllZip2 (LiftedCoercible f I) xss yss+ => SOP f xss -> SOP I yss+toI_SOP = htoI++instance HTrans NS NS where+ htrans = trans_NS+ hcoerce = coerce_NS++instance HTrans SOP SOP where+ htrans = trans_SOP+ hcoerce = coerce_SOP
+ src/Data/SOP/Sing.hs view
@@ -0,0 +1,111 @@+{-# LANGUAGE PolyKinds, StandaloneDeriving #-}+-- | Singleton types corresponding to type-level data structures.+--+-- The implementation is similar, but subtly different to that of the+-- @<https://hackage.haskell.org/package/singletons singletons>@ package.+-- See the <http://www.andres-loeh.de/TrueSumsOfProducts "True Sums of Products">+-- paper for details.+--+module Data.SOP.Sing+ ( -- * Singletons+ SList(..)+ , SListI+ , sList+ , para_SList+ , case_SList+ -- ** Shape of type-level lists+ , Shape(..)+ , shape+ , lengthSList+ ) where++import Data.Kind (Type)+import Data.Proxy (Proxy(..))++import Data.SOP.Constraint++-- * Singletons++-- | Explicit singleton list.+--+-- A singleton list can be used to reveal the structure of+-- a type-level list argument that the function is quantified+-- over. For every type-level list @xs@, there is one non-bottom+-- value of type @'SList' xs@.+--+-- Note that these singleton lists are polymorphic in the+-- list elements; we do not require a singleton representation+-- for them.+--+-- @since 0.2+--+data SList :: [k] -> Type where+ SNil :: SList '[]+ SCons :: SListI xs => SList (x ': xs)++deriving instance Show (SList (xs :: [k]))+deriving instance Eq (SList (xs :: [k]))+deriving instance Ord (SList (xs :: [k]))++-- | Paramorphism for a type-level list.+--+-- @since 0.4.0.0+--+para_SList ::+ SListI xs+ => r '[]+ -> (forall y ys . (SListI ys) => r ys -> r (y ': ys))+ -> r xs+para_SList nil cons =+ cpara_SList (Proxy :: Proxy Top) nil cons+{-# INLINE para_SList #-}++-- | Case distinction on a type-level list.+--+-- @since 0.4.0.0+--+case_SList ::+ SListI xs+ => r '[]+ -> (forall y ys . (SListI ys) => r (y ': ys))+ -> r xs+case_SList nil cons =+ ccase_SList (Proxy :: Proxy Top) nil cons+{-# INLINE case_SList #-}++-- | Get hold of an explicit singleton (that one can then+-- pattern match on) for a type-level list+--+sList :: SListI xs => SList xs+sList = ccase_SList (Proxy :: Proxy Top) SNil SCons++-- * Shape of type-level lists++-- | Occassionally it is useful to have an explicit, term-level, representation+-- of type-level lists (esp because of https://ghc.haskell.org/trac/ghc/ticket/9108 )+--+data Shape :: [k] -> Type where+ ShapeNil :: Shape '[]+ ShapeCons :: SListI xs => Shape xs -> Shape (x ': xs)++deriving instance Show (Shape xs)+deriving instance Eq (Shape xs)+deriving instance Ord (Shape xs)++-- | The shape of a type-level list.+shape :: forall (xs :: [k]). SListI xs => Shape xs+shape = case sList :: SList xs of+ SNil -> ShapeNil+ SCons -> ShapeCons shape++-- | The length of a type-level list.+--+-- @since 0.2+--+lengthSList :: forall (xs :: [k]) proxy. SListI xs => proxy xs -> Int+lengthSList _ = lengthShape (shape :: Shape xs)+ where+ lengthShape :: forall xs'. Shape xs' -> Int+ lengthShape ShapeNil = 0+ lengthShape (ShapeCons s) = 1 + lengthShape s+