diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -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.) + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/doctest.sh b/doctest.sh new file mode 100644 --- /dev/null +++ b/doctest.sh @@ -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') diff --git a/sop-core.cabal b/sop-core.cabal new file mode 100644 --- /dev/null +++ b/sop-core.cabal @@ -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 + @@. + . + A detailed description of the ideas behind this library is provided by + the paper: + . + * Edsko de Vries and Andres Löh. + . + Workshop on Generic Programming (WGP) 2014. + . +license: BSD3 +license-file: LICENSE +author: Edsko de Vries , Andres Löh +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 diff --git a/src/Data/SOP.hs b/src/Data/SOP.hs new file mode 100644 --- /dev/null +++ b/src/Data/SOP.hs @@ -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 + diff --git a/src/Data/SOP/BasicFunctors.hs b/src/Data/SOP/BasicFunctors.hs new file mode 100644 --- /dev/null +++ b/src/Data/SOP/BasicFunctors.hs @@ -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 . +-- +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 #-} diff --git a/src/Data/SOP/Classes.hs b/src/Data/SOP/Classes.hs new file mode 100644 --- /dev/null +++ b/src/Data/SOP/Classes.hs @@ -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 diff --git a/src/Data/SOP/Constraint.hs b/src/Data/SOP/Constraint.hs new file mode 100644 --- /dev/null +++ b/src/Data/SOP/Constraint.hs @@ -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 + diff --git a/src/Data/SOP/Dict.hs b/src/Data/SOP/Dict.hs new file mode 100644 --- /dev/null +++ b/src/Data/SOP/Dict.hs @@ -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 diff --git a/src/Data/SOP/NP.hs b/src/Data/SOP/NP.hs new file mode 100644 --- /dev/null +++ b/src/Data/SOP/NP.hs @@ -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 diff --git a/src/Data/SOP/NS.hs b/src/Data/SOP/NS.hs new file mode 100644 --- /dev/null +++ b/src/Data/SOP/NS.hs @@ -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 diff --git a/src/Data/SOP/Sing.hs b/src/Data/SOP/Sing.hs new file mode 100644 --- /dev/null +++ b/src/Data/SOP/Sing.hs @@ -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 +-- @@ package. +-- See the +-- 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 +