diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,29 +1,29 @@ -BSD 3-Clause License - -Copyright (c) 2018, Jiasen Wu -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - -* Redistributions of source code must retain the above copyright notice, this - list of conditions and the following disclaimer. - -* 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. - -* 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. +BSD 3-Clause License + +Copyright (c) 2018, Jiasen Wu +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +* Redistributions of source code must retain the above copyright notice, this + list of conditions and the following disclaimer. + +* 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. + +* 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/src/Data/Tuple/Ops.hs b/src/Data/Tuple/Ops.hs --- a/src/Data/Tuple/Ops.hs +++ b/src/Data/Tuple/Ops.hs @@ -1,38 +1,38 @@ ------------------------------------------------------------- --- | --- Module : Data.Tuple.Ops --- Description : various operations on n-ary tuples via GHC.Generics --- Copyright : (c) 2018 Jiasen Wu --- License : BSD-style (see the file LICENSE) --- Maintainer : Jiasen Wu --- Stability : experimental --- Portability : portable --- --- --- This module exports various operations on n-ary tuples ------------------------------------------------------------- -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE StandaloneDeriving #-} -module Data.Tuple.Ops( - module Data.Tuple.Ops.Uncons, - module Data.Tuple.Ops.Cons -) where - -import GHC.Generics -import Data.Tuple.Ops.Uncons -import Data.Tuple.Ops.Cons - -deriving instance Generic Int -deriving instance Generic Word -deriving instance Generic Char -deriving instance Generic Float -deriving instance Generic Double -deriving instance Generic (a,b,c,d,e,f,g,h) -deriving instance Generic (a,b,c,d,e,f,g,h,i) -deriving instance Generic (a,b,c,d,e,f,g,h,i,j) -deriving instance Generic (a,b,c,d,e,f,g,h,i,j,k) -deriving instance Generic (a,b,c,d,e,f,g,h,i,j,k,l) -deriving instance Generic (a,b,c,d,e,f,g,h,i,j,k,l,m) -deriving instance Generic (a,b,c,d,e,f,g,h,i,j,k,l,m,n) -deriving instance Generic (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) +------------------------------------------------------------ +-- | +-- Module : Data.Tuple.Ops +-- Description : various operations on n-ary tuples via GHC.Generics +-- Copyright : (c) 2018 Jiasen Wu +-- License : BSD-style (see the file LICENSE) +-- Maintainer : Jiasen Wu +-- Stability : experimental +-- Portability : portable +-- +-- +-- This module exports various operations on n-ary tuples +------------------------------------------------------------ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE StandaloneDeriving #-} +module Data.Tuple.Ops( + module Data.Tuple.Ops.Uncons, + module Data.Tuple.Ops.Cons +) where + +import GHC.Generics +import Data.Tuple.Ops.Uncons +import Data.Tuple.Ops.Cons + +deriving instance Generic Int +deriving instance Generic Word +deriving instance Generic Char +deriving instance Generic Float +deriving instance Generic Double +deriving instance Generic (a,b,c,d,e,f,g,h) +deriving instance Generic (a,b,c,d,e,f,g,h,i) +deriving instance Generic (a,b,c,d,e,f,g,h,i,j) +deriving instance Generic (a,b,c,d,e,f,g,h,i,j,k) +deriving instance Generic (a,b,c,d,e,f,g,h,i,j,k,l) +deriving instance Generic (a,b,c,d,e,f,g,h,i,j,k,l,m) +deriving instance Generic (a,b,c,d,e,f,g,h,i,j,k,l,m,n) +deriving instance Generic (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) deriving instance Generic (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p) diff --git a/src/Data/Tuple/Ops/Cons.hs b/src/Data/Tuple/Ops/Cons.hs --- a/src/Data/Tuple/Ops/Cons.hs +++ b/src/Data/Tuple/Ops/Cons.hs @@ -1,120 +1,124 @@ ------------------------------------------------------------- --- | --- Module : Data.Tuple.Ops.Cons --- Description : various operations on n-ary tuples via GHC.Generics --- Copyright : (c) 2018 Jiasen Wu --- License : BSD-style (see the file LICENSE) --- Maintainer : Jiasen Wu --- Stability : experimental --- Portability : portable --- --- --- This module define 'cons'. Examples are given below: --- --- >>> cons (1::Int) () --- 1 --- --- >>> cons (1::Int) 'a' --- (1,'a') --- --- >>> cons (True,'a') "S" --- ((True,'a'),"S") --- --- >>> cons "S" (True,'a') --- ("S",True,'a') --- ------------------------------------------------------------- -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE ScopedTypeVariables #-} - -module Data.Tuple.Ops.Cons (cons, Cons, Consable) where - -import GHC.Generics (Generic(..), (:*:)(..), (:+:)(..), URec, Rec0, C1, D1, S1, M1(..), U1, K1(..)) -import GHC.TypeLits (Symbol) -import Type.Family.List -import Data.Tuple.Ops.Internal - --- | Abstract type class for generic representation of a /cons/able datatype -class ConsableR va rb where - -- | @consR@ takes a value of type @va@ and a value of type @vb@ together @vb@'s representation, - -- returns the cons'ed value. Note that, 'ConsableR' is inductively scrutinize @vb@'s - -- representation, however this representation is only a dummy argument, since the result is - -- constructed from the value directly. - consR :: (Generic vb, Rep vb ~ D1 (MetaOfD1 (Rep vb)) rb) => va -> vb -> rb x -> ConsR va rb vb x - --- | Type function to calculate the type of cons'ed value -type family ConsR va rb vb where - ConsR va (C1 mc U1) vb = UnD1 (Rep va) - ConsR va (C1 mc (S1 ms (URec b))) vb = RepOfTuple "(,)" (S1 MetaS (Rec0 va) :*: S1 MetaS (Rec0 vb)) - ConsR va (b0 :+: b1) vb = RepOfTuple "(,)" (S1 MetaS (Rec0 va) :*: S1 MetaS (Rec0 vb)) - ConsR va (RepOfTuple tcon (b0 :*: b1)) vb = RepOfTuple (TupleConSucc tcon) (N (L (S1 MetaS (Rec0 va) :*: b0 :*: b1))) - -instance (Generic a, Rep a ~ D1 (MetaOfD1 (Rep a)) (UnD1 (Rep a))) => ConsableR a (C1 mc U1) where - consR a _ _ = unM1 $ from a - -instance ConsableR va (C1 mc (S1 ms (URec b))) where - consR a b _ = M1 (M1 (K1 a) :*: M1 (K1 b)) - -instance ConsableR va (b0 :+: b1) where - consR a b _ = M1 (M1 (K1 a) :*: M1 (K1 b)) - -instance (Linearize b0, Linearize b1, - Normalize ((S1 MetaS (Rec0 va) :< L b0 ++ L b1)), - AppDistributive (L b0)) => ConsableR va (RepOfTuple tcon (b0 :*: b1)) where - consR a b _ = M1 $ normalize $ linearize $ (M1 (K1 a) :: S1 MetaS (Rec0 va) x) :*: unM1 (unM1 (from b)) - --- | calculate the tuple constructor of the size 1 bigger --- upto the tupel of arity of 15 -type family TupleConSucc (a :: Symbol) where - TupleConSucc "(,)" = "(,,)" - TupleConSucc "(,,)" = "(,,,)" - TupleConSucc "(,,,)" = "(,,,,)" - TupleConSucc "(,,,,)" = "(,,,,,)" - TupleConSucc "(,,,,,)" = "(,,,,,,)" - TupleConSucc "(,,,,,,)" = "(,,,,,,,)" - TupleConSucc "(,,,,,,,)" = "(,,,,,,,,)" - TupleConSucc "(,,,,,,,,)" = "(,,,,,,,,,)" - TupleConSucc "(,,,,,,,,,)" = "(,,,,,,,,,,)" - TupleConSucc "(,,,,,,,,,,)" = "(,,,,,,,,,,,)" - TupleConSucc "(,,,,,,,,,,,)" = "(,,,,,,,,,,,,)" - TupleConSucc "(,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,)" - TupleConSucc "(,,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,,)" - TupleConSucc "(,,,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,,,)" - TupleConSucc "(,,,,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,,,,)" - --- | calculate the result type of 'cons' -type family Cons a b where - Cons z (a,b) = (z,a,b) - Cons z (a,b,c) = (z,a,b,c) - Cons z (a,b,c,d) = (z,a,b,c,d) - Cons z (a,b,c,d,e) = (z,a,b,c,d,e) - Cons z (a,b,c,d,e,f) = (z,a,b,c,d,e,f) - Cons z (a,b,c,d,e,f,g) = (z,a,b,c,d,e,f,g) - Cons z (a,b,c,d,e,f,g,h) = (z,a,b,c,d,e,f,g,h) - Cons z (a,b,c,d,e,f,g,h,i) = (z,a,b,c,d,e,f,g,h,i) - Cons z (a,b,c,d,e,f,g,h,i,j) = (z,a,b,c,d,e,f,g,h,i,j) - Cons z (a,b,c,d,e,f,g,h,i,j,k) = (z,a,b,c,d,e,f,g,h,i,j,k) - Cons z (a,b,c,d,e,f,g,h,i,j,k,l) = (z,a,b,c,d,e,f,g,h,i,j,k,l) - Cons z (a,b,c,d,e,f,g,h,i,j,k,l,m) = (z,a,b,c,d,e,f,g,h,i,j,k,l,m) - Cons z (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = (z,a,b,c,d,e,f,g,h,i,j,k,l,m,n) - Cons z (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = (z,a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) - Cons z () = z - Cons z a = (z,a) - --- | A constraint on any 'cons'able data type, where --- @a@ and @b@ are the input, and @c@ is the output. -type Consable a b c = (Generic a, Generic b, Generic c, Cons a b ~ c, - Rep b ~ D1 (MetaOfD1 (Rep b)) (UnD1 (Rep b)), - Rep c ~ D1 (MetaOfD1 (Rep c)) (UnD1 (Rep c)), - ConsableR a (UnD1 (Rep b)), - ConsR a (UnD1 (Rep b)) b ~ (UnD1 (Rep c))) - --- | 'cons' takes two datatype, and produces a tuple of them. --- if @b@ is unit, then @a@ is returned. --- if @b@ is not a tuple, then a pair of @(a,b)@ is returned. --- otherwise, @a@ is placed in front of @b@. -cons :: Consable a b c => a -> b -> c -cons a b = to $ M1 $ consR a b (unM1 $ from b) +------------------------------------------------------------ +-- | +-- Module : Data.Tuple.Ops.Cons +-- Description : various operations on n-ary tuples via GHC.Generics +-- Copyright : (c) 2018 Jiasen Wu +-- License : BSD-style (see the file LICENSE) +-- Maintainer : Jiasen Wu +-- Stability : experimental +-- Portability : portable +-- +-- +-- This module define 'cons'. Examples are given below: +-- +-- >>> cons (1::Int) () +-- 1 +-- +-- >>> cons (1::Int) 'a' +-- (1,'a') +-- +-- >>> cons (True,'a') "S" +-- ((True,'a'),"S") +-- +-- >>> cons "S" (True,'a') +-- ("S",True,'a') +-- +------------------------------------------------------------ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Data.Tuple.Ops.Cons (cons, Cons, Consable) where + +import GHC.Generics (Generic(..), (:*:)(..), (:+:)(..), URec, Rec0, C1, D1, S1, M1(..), U1, K1(..)) +import GHC.TypeLits (Symbol) +import Type.Family.List +import Data.Tuple.Ops.Internal + +-- | Abstract type class for generic representation of a /cons/able datatype +class ConsableR va rb where + -- | @consR@ takes a value of type @va@ and a value of type @vb@ together @vb@'s representation, + -- returns the cons'ed value. Note that, 'ConsableR' is inductively scrutinize @vb@'s + -- representation, however this representation is only a dummy argument, since the result is + -- constructed from the value directly. + consR :: (Generic vb, Rep vb ~ D1 (MetaOfD1 (Rep vb)) rb) => va -> vb -> rb x -> ConsR va rb vb x + +-- | Type function to calculate the type of cons'ed value +type family ConsR va rb vb where + ConsR va (C1 mc U1) vb = UnD1 (Rep va) + ConsR va (C1 mc (S1 ms (URec b))) vb = RepOfTuple "(,)" (S1 MetaS (Rec0 va) :*: S1 MetaS (Rec0 vb)) + ConsR va (C1 mc (S1 ms (Rec0 b))) vb = RepOfTuple "(,)" (S1 MetaS (Rec0 va) :*: S1 MetaS (Rec0 vb)) + ConsR va (b0 :+: b1) vb = RepOfTuple "(,)" (S1 MetaS (Rec0 va) :*: S1 MetaS (Rec0 vb)) + ConsR va (RepOfTuple tcon (b0 :*: b1)) vb = RepOfTuple (TupleConSucc tcon) (N (L (S1 MetaS (Rec0 va) :*: b0 :*: b1))) + +instance (Generic a, Rep a ~ D1 (MetaOfD1 (Rep a)) (UnD1 (Rep a))) => ConsableR a (C1 mc U1) where + consR a _ _ = unM1 $ from a + +instance ConsableR va (C1 mc (S1 ms (URec b))) where + consR a b _ = M1 (M1 (K1 a) :*: M1 (K1 b)) + +instance ConsableR va (C1 mc (S1 ms (Rec0 b))) where + consR a b _ = M1 (M1 (K1 a) :*: M1 (K1 b)) + +instance ConsableR va (b0 :+: b1) where + consR a b _ = M1 (M1 (K1 a) :*: M1 (K1 b)) + +instance (Linearize b0, Linearize b1, + Normalize ((S1 MetaS (Rec0 va) :< L b0 ++ L b1)), + AppDistributive (L b0)) => ConsableR va (RepOfTuple tcon (b0 :*: b1)) where + consR a b _ = M1 $ normalize $ linearize $ (M1 (K1 a) :: S1 MetaS (Rec0 va) x) :*: unM1 (unM1 (from b)) + +-- | calculate the tuple constructor of the size 1 bigger +-- upto the tupel of arity of 15 +type family TupleConSucc (a :: Symbol) where + TupleConSucc "(,)" = "(,,)" + TupleConSucc "(,,)" = "(,,,)" + TupleConSucc "(,,,)" = "(,,,,)" + TupleConSucc "(,,,,)" = "(,,,,,)" + TupleConSucc "(,,,,,)" = "(,,,,,,)" + TupleConSucc "(,,,,,,)" = "(,,,,,,,)" + TupleConSucc "(,,,,,,,)" = "(,,,,,,,,)" + TupleConSucc "(,,,,,,,,)" = "(,,,,,,,,,)" + TupleConSucc "(,,,,,,,,,)" = "(,,,,,,,,,,)" + TupleConSucc "(,,,,,,,,,,)" = "(,,,,,,,,,,,)" + TupleConSucc "(,,,,,,,,,,,)" = "(,,,,,,,,,,,,)" + TupleConSucc "(,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,)" + TupleConSucc "(,,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,,)" + TupleConSucc "(,,,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,,,)" + TupleConSucc "(,,,,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,,,,)" + +-- | calculate the result type of 'cons' +type family Cons a b where + Cons z (a,b) = (z,a,b) + Cons z (a,b,c) = (z,a,b,c) + Cons z (a,b,c,d) = (z,a,b,c,d) + Cons z (a,b,c,d,e) = (z,a,b,c,d,e) + Cons z (a,b,c,d,e,f) = (z,a,b,c,d,e,f) + Cons z (a,b,c,d,e,f,g) = (z,a,b,c,d,e,f,g) + Cons z (a,b,c,d,e,f,g,h) = (z,a,b,c,d,e,f,g,h) + Cons z (a,b,c,d,e,f,g,h,i) = (z,a,b,c,d,e,f,g,h,i) + Cons z (a,b,c,d,e,f,g,h,i,j) = (z,a,b,c,d,e,f,g,h,i,j) + Cons z (a,b,c,d,e,f,g,h,i,j,k) = (z,a,b,c,d,e,f,g,h,i,j,k) + Cons z (a,b,c,d,e,f,g,h,i,j,k,l) = (z,a,b,c,d,e,f,g,h,i,j,k,l) + Cons z (a,b,c,d,e,f,g,h,i,j,k,l,m) = (z,a,b,c,d,e,f,g,h,i,j,k,l,m) + Cons z (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = (z,a,b,c,d,e,f,g,h,i,j,k,l,m,n) + Cons z (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = (z,a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) + Cons z () = z + Cons z a = (z,a) + +-- | A constraint on any 'cons'able data type, where +-- @a@ and @b@ are the input, and @c@ is the output. +type Consable a b c = (Generic a, Generic b, Generic c, Cons a b ~ c, + Rep b ~ D1 (MetaOfD1 (Rep b)) (UnD1 (Rep b)), + Rep c ~ D1 (MetaOfD1 (Rep c)) (UnD1 (Rep c)), + ConsableR a (UnD1 (Rep b)), + ConsR a (UnD1 (Rep b)) b ~ (UnD1 (Rep c))) + +-- | 'cons' takes two datatype, and produces a tuple of them. +-- if @b@ is unit, then @a@ is returned. +-- if @b@ is not a tuple, then a pair of @(a,b)@ is returned. +-- otherwise, @a@ is placed in front of @b@. +cons :: Consable a b c => a -> b -> c +cons a b = to $ M1 $ consR a b (unM1 $ from b) diff --git a/src/Data/Tuple/Ops/Internal.hs b/src/Data/Tuple/Ops/Internal.hs --- a/src/Data/Tuple/Ops/Internal.hs +++ b/src/Data/Tuple/Ops/Internal.hs @@ -1,149 +1,149 @@ ------------------------------------------------------------- --- | --- Module : Data.Tuple.Ops.Internal --- Description : various operations on n-ary tuples via GHC.Generics --- Copyright : (c) 2018 Jiasen Wu --- License : BSD-style (see the file LICENSE) --- Maintainer : Jiasen Wu --- Stability : experimental --- Portability : portable --- --- --- This module defins operations to manipulate the generic --- representation of tuple. ------------------------------------------------------------- -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE UndecidableInstances #-} - -module Data.Tuple.Ops.Internal where - -import GHC.Generics ((:*:)(..), Rec0, C1, D1, S1, Meta(..), SourceUnpackedness(..), SourceStrictness(..), DecidedStrictness(..), FixityI(..)) -import Data.Proxy -import Data.Type.Combinator -import Data.Type.Product -import Type.Family.List -import Type.Class.Witness -import qualified Type.Family.Nat as Nat - --- 'TupleR' is an injective type that @TupleR f x == TupleR g y ---> f == g && x == y@ -newtype TupleR (f :: [* -> *]) x = TupleR { unTupleR :: Tuple (f <&> x)} - --- | prove that @(a ++ b) <&> x == a <&> x ++ b <&> x@ -class AppDistributive (a :: [* -> *]) where - appDistrWit :: (Proxy a, Proxy b, Proxy x) -> Wit (((a ++ b) <&> x) ~ ((a <&> x) ++ (b <&> x))) --- | inductive proof on @a@ --- case 1. @a@ is @[]@ -instance AppDistributive '[] where - appDistrWit _ = Wit --- | case 2. @a@ is @_ :< _@ -instance AppDistributive as => AppDistributive (a :< as) where - appDistrWit (_ :: Proxy (a :< as), pb, px) = - case appDistrWit (Proxy :: Proxy as, pb, px) of - Wit -> Wit - --- | utility function to call 'appDistrWit' -appDistrWitPassArg :: (f :*: g) x -> (Proxy (L f), Proxy (L g), Proxy x) -appDistrWitPassArg _ = (Proxy, Proxy, Proxy) - --- | Representation of tuple are shaped in a balanced tree. --- 'L' transforms the tree into a list, for further manipulation. -class Linearize (t :: * -> *) where - type L t :: [* -> *] - linearize :: t x -> TupleR (L t) x - --- | base case. sinleton -instance Linearize (S1 MetaS (Rec0 t)) where - type L (S1 MetaS (Rec0 t)) = '[S1 MetaS (Rec0 t)] - linearize = TupleR . only . I - --- | inductive case. preppend a product with what ever -instance (Linearize v, Linearize u, AppDistributive (L u)) => Linearize (u :*: v) where - type L (u :*: v) = L u ++ L v - linearize (a :*: b) = - case appDistrWit (appDistrWitPassArg (a :*: b)) of - Wit -> TupleR $ append' (unTupleR $ linearize a) (unTupleR $ linearize b) - -length' :: TupleR a x -> Proxy (Nat.Len a) -length' _ = Proxy - --- | calculate the half -type family Half (a :: Nat.N) :: Nat.N where - Half ('Nat.S 'Nat.Z) = 'Nat.Z - Half ('Nat.S ('Nat.S 'Nat.Z)) = 'Nat.S 'Nat.Z - Half ('Nat.S ('Nat.S n)) = 'Nat.S (Half n) --- | calculate the half -half :: Proxy n -> Proxy (Half n) -half _ = Proxy - --- | take the first n elements from a product -class Take (n :: Nat.N) (a :: [* -> *]) where - type T n a :: [* -> *] - take' :: Proxy n -> TupleR a x -> TupleR (T n a) x - --- | base case. take one out of singleton -instance Take 'Nat.Z xs where - type T 'Nat.Z xs = '[] - take' _ _ = TupleR Ø - --- | inductive case. take (n+1) elements -instance Take n as => Take ('Nat.S n) (a : as) where - type T ('Nat.S n) (a : as) = a : T n as - take' (_ :: Proxy ('Nat.S n)) (TupleR (a :< as) :: TupleR (a : as) x) = - let as' = unTupleR $ take' (Proxy :: Proxy n) (TupleR as :: TupleR as x) - in TupleR (a :< as') - --- | drop the first n elements from a product -class Drop (n :: Nat.N) (a :: [* -> *]) where - type D n a :: [* -> *] - drop' :: Proxy n -> TupleR a x -> TupleR (D n a) x - --- | base case. drop one from product -instance Drop 'Nat.Z as where - type D 'Nat.Z as = as - drop' _ a = a - --- | inductive case. drop (n+1) elements -instance Drop n as => Drop ('Nat.S n) (a : as) where - type D ('Nat.S n) (a : as) = D n as - drop' (_ :: Proxy ('Nat.S n)) (TupleR (a :< as) :: TupleR (a : as) x) = - drop' (Proxy :: Proxy n) (TupleR as :: TupleR as x) - --- | 'Normalize' converts a linear product back into a balanced tree. -class Normalize (a :: [* -> *]) where - type N a :: * -> * - normalize :: TupleR a x -> N a x - --- | base case. singleton -instance Normalize '[S1 MetaS (Rec0 t)] where - type N '[S1 MetaS (Rec0 t)] = S1 MetaS (Rec0 t) - normalize a = getI $ head' $ unTupleR a - --- | inductive case. product -instance (Take (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c), - Drop (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c), - Normalize (T (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c)), - Normalize (D (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c))) - => Normalize (a :< b :< c) where - type N (a :< b :< c) = N (T (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c)) :*: - N (D (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c)) - normalize v = let n = half (length' v) - in normalize (take' n v) :*: normalize (drop' n v) - -type MetaS = 'MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy --- | utility type function to trim the Rec0 -type family UnRec0 t where - UnRec0 (Rec0 t) = t --- | utility type function to trim the S1 -type family UnS1 t where - UnS1 (S1 _ t) = t --- | utility type function to trim the D1 -type family UnD1 t where - UnD1 (D1 _ t) = t --- | utility type function to extract the meta information -type family MetaOfD1 t where - MetaOfD1 (D1 m _) = m - --- | representation of a tuple of arity > 2, in which @/u/@ is of the form @_ :*: _@ +------------------------------------------------------------ +-- | +-- Module : Data.Tuple.Ops.Internal +-- Description : various operations on n-ary tuples via GHC.Generics +-- Copyright : (c) 2018 Jiasen Wu +-- License : BSD-style (see the file LICENSE) +-- Maintainer : Jiasen Wu +-- Stability : experimental +-- Portability : portable +-- +-- +-- This module defins operations to manipulate the generic +-- representation of tuple. +------------------------------------------------------------ +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE UndecidableInstances #-} + +module Data.Tuple.Ops.Internal where + +import GHC.Generics ((:*:)(..), Rec0, C1, D1, S1, Meta(..), SourceUnpackedness(..), SourceStrictness(..), DecidedStrictness(..), FixityI(..)) +import Data.Proxy +import Data.Type.Combinator +import Data.Type.Product +import Type.Family.List +import Type.Class.Witness +import qualified Type.Family.Nat as Nat + +-- 'TupleR' is an injective type that @TupleR f x == TupleR g y ---> f == g && x == y@ +newtype TupleR (f :: [* -> *]) x = TupleR { unTupleR :: Tuple (f <&> x)} + +-- | prove that @(a ++ b) <&> x == a <&> x ++ b <&> x@ +class AppDistributive (a :: [* -> *]) where + appDistrWit :: (Proxy a, Proxy b, Proxy x) -> Wit (((a ++ b) <&> x) ~ ((a <&> x) ++ (b <&> x))) +-- | inductive proof on @a@ +-- case 1. @a@ is @[]@ +instance AppDistributive '[] where + appDistrWit _ = Wit +-- | case 2. @a@ is @_ :< _@ +instance AppDistributive as => AppDistributive (a :< as) where + appDistrWit (_ :: Proxy (a :< as), pb, px) = + case appDistrWit (Proxy :: Proxy as, pb, px) of + Wit -> Wit + +-- | utility function to call 'appDistrWit' +appDistrWitPassArg :: (f :*: g) x -> (Proxy (L f), Proxy (L g), Proxy x) +appDistrWitPassArg _ = (Proxy, Proxy, Proxy) + +-- | Representation of tuple are shaped in a balanced tree. +-- 'L' transforms the tree into a list, for further manipulation. +class Linearize (t :: * -> *) where + type L t :: [* -> *] + linearize :: t x -> TupleR (L t) x + +-- | base case. sinleton +instance Linearize (S1 MetaS (Rec0 t)) where + type L (S1 MetaS (Rec0 t)) = '[S1 MetaS (Rec0 t)] + linearize = TupleR . only . I + +-- | inductive case. preppend a product with what ever +instance (Linearize v, Linearize u, AppDistributive (L u)) => Linearize (u :*: v) where + type L (u :*: v) = L u ++ L v + linearize (a :*: b) = + case appDistrWit (appDistrWitPassArg (a :*: b)) of + Wit -> TupleR $ append' (unTupleR $ linearize a) (unTupleR $ linearize b) + +length' :: TupleR a x -> Proxy (Nat.Len a) +length' _ = Proxy + +-- | calculate the half +type family Half (a :: Nat.N) :: Nat.N where + Half ('Nat.S 'Nat.Z) = 'Nat.Z + Half ('Nat.S ('Nat.S 'Nat.Z)) = 'Nat.S 'Nat.Z + Half ('Nat.S ('Nat.S n)) = 'Nat.S (Half n) +-- | calculate the half +half :: Proxy n -> Proxy (Half n) +half _ = Proxy + +-- | take the first n elements from a product +class Take (n :: Nat.N) (a :: [* -> *]) where + type T n a :: [* -> *] + take' :: Proxy n -> TupleR a x -> TupleR (T n a) x + +-- | base case. take one out of singleton +instance Take 'Nat.Z xs where + type T 'Nat.Z xs = '[] + take' _ _ = TupleR Ø + +-- | inductive case. take (n+1) elements +instance Take n as => Take ('Nat.S n) (a : as) where + type T ('Nat.S n) (a : as) = a : T n as + take' (_ :: Proxy ('Nat.S n)) (TupleR (a :< as) :: TupleR (a : as) x) = + let as' = unTupleR $ take' (Proxy :: Proxy n) (TupleR as :: TupleR as x) + in TupleR (a :< as') + +-- | drop the first n elements from a product +class Drop (n :: Nat.N) (a :: [* -> *]) where + type D n a :: [* -> *] + drop' :: Proxy n -> TupleR a x -> TupleR (D n a) x + +-- | base case. drop one from product +instance Drop 'Nat.Z as where + type D 'Nat.Z as = as + drop' _ a = a + +-- | inductive case. drop (n+1) elements +instance Drop n as => Drop ('Nat.S n) (a : as) where + type D ('Nat.S n) (a : as) = D n as + drop' (_ :: Proxy ('Nat.S n)) (TupleR (a :< as) :: TupleR (a : as) x) = + drop' (Proxy :: Proxy n) (TupleR as :: TupleR as x) + +-- | 'Normalize' converts a linear product back into a balanced tree. +class Normalize (a :: [* -> *]) where + type N a :: * -> * + normalize :: TupleR a x -> N a x + +-- | base case. singleton +instance Normalize '[S1 MetaS (Rec0 t)] where + type N '[S1 MetaS (Rec0 t)] = S1 MetaS (Rec0 t) + normalize a = getI $ head' $ unTupleR a + +-- | inductive case. product +instance (Take (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c), + Drop (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c), + Normalize (T (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c)), + Normalize (D (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c))) + => Normalize (a :< b :< c) where + type N (a :< b :< c) = N (T (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c)) :*: + N (D (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c)) + normalize v = let n = half (length' v) + in normalize (take' n v) :*: normalize (drop' n v) + +type MetaS = 'MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy +-- | utility type function to trim the Rec0 +type family UnRec0 t where + UnRec0 (Rec0 t) = t +-- | utility type function to trim the S1 +type family UnS1 t where + UnS1 (S1 _ t) = t +-- | utility type function to trim the D1 +type family UnD1 t where + UnD1 (D1 _ t) = t +-- | utility type function to extract the meta information +type family MetaOfD1 t where + MetaOfD1 (D1 m _) = m + +-- | representation of a tuple of arity > 2, in which @/u/@ is of the form @_ :*: _@ type RepOfTuple c u = C1 ('MetaCons c 'PrefixI 'False) u diff --git a/src/Data/Tuple/Ops/Uncons.hs b/src/Data/Tuple/Ops/Uncons.hs --- a/src/Data/Tuple/Ops/Uncons.hs +++ b/src/Data/Tuple/Ops/Uncons.hs @@ -1,137 +1,145 @@ ------------------------------------------------------------- --- | --- Module : Data.Tuple.Ops.Uncons --- Description : various operations on n-ary tuples via GHC.Generics --- Copyright : (c) 2018 Jiasen Wu --- License : BSD-style (see the file LICENSE) --- Maintainer : Jiasen Wu --- Stability : experimental --- Portability : portable --- --- --- This module define 'uncons'. Examples are given below: --- --- >>> uncons (1::Int) --- (1,()) --- --- >>> uncons (1::Int,'a') --- (1,'a') --- --- >>> uncons (True,'a', "S") --- (True,('a',"S")) --- ------------------------------------------------------------- -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE UndecidableInstances #-} - -module Data.Tuple.Ops.Uncons (uncons, Uncons, Unconsable) where - -import GHC.Generics (Generic(..), (:*:)(..), (:+:)(..), URec, Rec0, C1, D1, S1, M1(..), U1, K1(..), Meta(..), FixityI(..)) -import GHC.TypeLits (Symbol) -import Data.Proxy -import Type.Family.Nat (N1) -import Data.Tuple.Ops.Internal - --- | 'HeadR' is a type function that takes the first element of a tuple -type family HeadR (f :: * -> *) :: * -> * where - HeadR (C1 mc (S1 ms (URec a))) = C1 mc (S1 ms (URec a)) - HeadR (a :+: b) = a :+: b - HeadR (RepOfTuple "(,)" (S1 MetaS (Rec0 a) :*: S1 MetaS (Rec0 b))) = UnD1 (Rep a) - HeadR (RepOfTuple tcon (a :*: b :*: c)) = UnD1 (Rep (UnRec0 (UnS1 (N (T N1 (L (a :*: b :*: c))))))) --- | 'TailR' is a type function that drops the first element of a tuple -type family TailR (f :: * -> *) :: * -> * where - TailR (C1 mc (S1 ms (URec a))) = C1 ('MetaCons "()" 'PrefixI 'False) U1 - TailR (a :+: b) = C1 ('MetaCons "()" 'PrefixI 'False) U1 - TailR (RepOfTuple "(,)" (S1 MetaS (Rec0 a) :*: S1 MetaS (Rec0 b))) = UnD1 (Rep b) - TailR (RepOfTuple tcon (a :*: b :*: c)) = RepOfTuple (TupleConPred tcon) (N (D N1 (L (a :*: b :*: c)))) - --- | Abstract type class for generic representation of a /uncons/able datatype -class UnconsableR f where - unconsR :: f a -> (HeadR f a, TailR f a) - --- | primitive datatype --- 'HeadR' is the datatype itself --- 'TailR' is () -instance UnconsableR (C1 mc (S1 ms (URec a))) where - unconsR a = (a, unM1 (from ())) - --- | sum datatype --- 'HeadR' is the datatype itself --- 'TailR' is () -instance UnconsableR (a :+: b) where - unconsR a = (a, unM1 (from ())) - --- | pair --- 'HeadR' is the first element --- 'TailR' is the second element -instance (Generic t1, Rep t1 ~ D1 mt1 ct1, - Generic t2, Rep t2 ~ D1 mt2 ct2) - => UnconsableR (RepOfTuple "(,)" (S1 MetaS (Rec0 t1) :*: S1 MetaS (Rec0 t2))) where - unconsR (M1 (a :*: b)) = (unM1 $ from $ unK1 $ unM1 a, unM1 $ from $ unK1 $ unM1 b) - --- | tuple of arity > 2 --- 'HeadR' is the first element --- 'TailR' is the rest all elements -instance (Linearize (a :*: b :*: c), L (a :*: b :*: c) ~ (S1 MetaS (Rec0 t) : w), - Generic t, Rep t ~ D1 hm hc, Normalize w) - => UnconsableR (RepOfTuple tcon (a :*: b :*: c)) where - unconsR a = let tup = linearize (unM1 a) - one = Proxy :: Proxy N1 - h = unM1 $ from $ unK1 $ unM1 $ normalize $ take' one tup - t = M1 $ normalize $ drop' one tup - in (h, t) - --- | calculate the tuple constructor of the size 1 smaller --- upto the tupel of arity of 16 -type family TupleConPred (a :: Symbol) where - TupleConPred "(,,)" = "(,)" - TupleConPred "(,,,)" = "(,,)" - TupleConPred "(,,,,)" = "(,,,)" - TupleConPred "(,,,,,)" = "(,,,,)" - TupleConPred "(,,,,,,)" = "(,,,,,)" - TupleConPred "(,,,,,,,)" = "(,,,,,,)" - TupleConPred "(,,,,,,,,)" = "(,,,,,,,)" - TupleConPred "(,,,,,,,,,)" = "(,,,,,,,,)" - TupleConPred "(,,,,,,,,,,)" = "(,,,,,,,,,)" - TupleConPred "(,,,,,,,,,,,)" = "(,,,,,,,,,,)" - TupleConPred "(,,,,,,,,,,,,)" = "(,,,,,,,,,,,)" - TupleConPred "(,,,,,,,,,,,,,)" = "(,,,,,,,,,,,,)" - TupleConPred "(,,,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,)" - TupleConPred "(,,,,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,,)" - TupleConPred "(,,,,,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,,,)" - --- | calculate the result type of 'uncons' -type family Uncons a where - Uncons (a,b) = (a,b) - Uncons (a,b,c) = (a, (b,c)) - Uncons (a,b,c,d) = (a, (b,c,d)) - Uncons (a,b,c,d,e) = (a, (b,c,d,e)) - Uncons (a,b,c,d,e,f) = (a, (b,c,d,e,f)) - Uncons (a,b,c,d,e,f,g) = (a, (b,c,d,e,f,g)) - Uncons (a,b,c,d,e,f,g,h) = (a, (b,c,d,e,f,g,h)) - Uncons (a,b,c,d,e,f,g,h,i) = (a, (b,c,d,e,f,g,h,i)) - Uncons (a,b,c,d,e,f,g,h,i,j) = (a, (b,c,d,e,f,g,h,i,j)) - Uncons (a,b,c,d,e,f,g,h,i,j,k) = (a, (b,c,d,e,f,g,h,i,j,k)) - Uncons (a,b,c,d,e,f,g,h,i,j,k,l) = (a, (b,c,d,e,f,g,h,i,j,k,l)) - Uncons (a,b,c,d,e,f,g,h,i,j,k,l,m) = (a, (b,c,d,e,f,g,h,i,j,k,l,m)) - Uncons (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = (a, (b,c,d,e,f,g,h,i,j,k,l,m,n)) - Uncons (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = (a, (b,c,d,e,f,g,h,i,j,k,l,m,n,o)) - Uncons (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p) = (a, (b,c,d,e,f,g,h,i,j,k,l,m,n,o,p)) - Uncons a = (a, ()) - --- | A constraint on any 'uncons'able data type, where --- @a@ is the input type, and @(b,c)@ is the output type -type Unconsable a b c = (Generic a, Generic b, Generic c, Uncons a ~ (b, c), - Rep a ~ D1 (MetaOfD1 (Rep a)) (UnD1 (Rep a)), - Rep b ~ D1 (MetaOfD1 (Rep b)) (UnD1 (Rep b)), - Rep c ~ D1 (MetaOfD1 (Rep c)) (UnD1 (Rep c)), - UnconsableR (UnD1 (Rep a)), - HeadR (UnD1 (Rep a)) ~ (UnD1 (Rep b)), - TailR (UnD1 (Rep a)) ~ (UnD1 (Rep c))) - --- | 'uncons' takes primitive, pair, tuple, --- and produces a pair of its first data and the rest elements. -uncons :: Unconsable a b c => a -> (b, c) +------------------------------------------------------------ +-- | +-- Module : Data.Tuple.Ops.Uncons +-- Description : various operations on n-ary tuples via GHC.Generics +-- Copyright : (c) 2018 Jiasen Wu +-- License : BSD-style (see the file LICENSE) +-- Maintainer : Jiasen Wu +-- Stability : experimental +-- Portability : portable +-- +-- +-- This module define 'uncons'. Examples are given below: +-- +-- >>> uncons (1::Int) +-- (1,()) +-- +-- >>> uncons (1::Int,'a') +-- (1,'a') +-- +-- >>> uncons (True,'a', "S") +-- (True,('a',"S")) +-- +------------------------------------------------------------ +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE UndecidableInstances #-} + +module Data.Tuple.Ops.Uncons (uncons, Uncons, Unconsable) where + +import GHC.Generics (Generic(..), (:*:)(..), (:+:)(..), URec, Rec0, C1, D1, S1, M1(..), U1, K1(..), Meta(..), FixityI(..)) +import GHC.TypeLits (Symbol) +import Data.Proxy +import Type.Family.Nat (N1) +import Data.Tuple.Ops.Internal + +-- | 'HeadR' is a type function that takes the first element of a tuple +type family HeadR (f :: * -> *) :: * -> * where + HeadR (C1 mc (S1 ms (URec a))) = C1 mc (S1 ms (URec a)) -- unlifted type + HeadR (C1 mc (S1 ms (Rec0 a))) = C1 mc (S1 ms (Rec0 a)) -- lifted type + HeadR (a :+: b) = a :+: b + HeadR (RepOfTuple "(,)" (S1 MetaS (Rec0 a) :*: S1 MetaS (Rec0 b))) = UnD1 (Rep a) + HeadR (RepOfTuple tcon (a :*: b :*: c)) = UnD1 (Rep (UnRec0 (UnS1 (N (T N1 (L (a :*: b :*: c))))))) +-- | 'TailR' is a type function that drops the first element of a tuple +type family TailR (f :: * -> *) :: * -> * where + TailR (C1 mc (S1 ms (URec a))) = C1 ('MetaCons "()" 'PrefixI 'False) U1 -- unlifted type + TailR (C1 mc (S1 ms (Rec0 a))) = C1 ('MetaCons "()" 'PrefixI 'False) U1 -- lifted type + TailR (a :+: b) = C1 ('MetaCons "()" 'PrefixI 'False) U1 + TailR (RepOfTuple "(,)" (S1 MetaS (Rec0 a) :*: S1 MetaS (Rec0 b))) = UnD1 (Rep b) + TailR (RepOfTuple tcon (a :*: b :*: c)) = RepOfTuple (TupleConPred tcon) (N (D N1 (L (a :*: b :*: c)))) + +-- | Abstract type class for generic representation of a /uncons/able datatype +class UnconsableR f where + unconsR :: f a -> (HeadR f a, TailR f a) + +-- | primitive datatype +-- 'HeadR' is the datatype itself +-- 'TailR' is () +instance UnconsableR (C1 mc (S1 ms (URec a))) where + unconsR a = (a, unM1 (from ())) + +-- | lifted datatype +-- 'HeadR' is the datatype itself +-- 'TailR' is () +instance UnconsableR (C1 mc (S1 ms (Rec0 a))) where + unconsR a = (a, unM1 (from ())) + +-- | sum datatype +-- 'HeadR' is the datatype itself +-- 'TailR' is () +instance UnconsableR (a :+: b) where + unconsR a = (a, unM1 (from ())) + +-- | pair +-- 'HeadR' is the first element +-- 'TailR' is the second element +instance (Generic t1, Rep t1 ~ D1 mt1 ct1, + Generic t2, Rep t2 ~ D1 mt2 ct2) + => UnconsableR (RepOfTuple "(,)" (S1 MetaS (Rec0 t1) :*: S1 MetaS (Rec0 t2))) where + unconsR (M1 (a :*: b)) = (unM1 $ from $ unK1 $ unM1 a, unM1 $ from $ unK1 $ unM1 b) + +-- | tuple of arity > 2 +-- 'HeadR' is the first element +-- 'TailR' is the rest all elements +instance (Linearize (a :*: b :*: c), L (a :*: b :*: c) ~ (S1 MetaS (Rec0 t) : w), + Generic t, Rep t ~ D1 hm hc, Normalize w) + => UnconsableR (RepOfTuple tcon (a :*: b :*: c)) where + unconsR a = let tup = linearize (unM1 a) + one = Proxy :: Proxy N1 + h = unM1 $ from $ unK1 $ unM1 $ normalize $ take' one tup + t = M1 $ normalize $ drop' one tup + in (h, t) + +-- | calculate the tuple constructor of the size 1 smaller +-- upto the tupel of arity of 16 +type family TupleConPred (a :: Symbol) where + TupleConPred "(,,)" = "(,)" + TupleConPred "(,,,)" = "(,,)" + TupleConPred "(,,,,)" = "(,,,)" + TupleConPred "(,,,,,)" = "(,,,,)" + TupleConPred "(,,,,,,)" = "(,,,,,)" + TupleConPred "(,,,,,,,)" = "(,,,,,,)" + TupleConPred "(,,,,,,,,)" = "(,,,,,,,)" + TupleConPred "(,,,,,,,,,)" = "(,,,,,,,,)" + TupleConPred "(,,,,,,,,,,)" = "(,,,,,,,,,)" + TupleConPred "(,,,,,,,,,,,)" = "(,,,,,,,,,,)" + TupleConPred "(,,,,,,,,,,,,)" = "(,,,,,,,,,,,)" + TupleConPred "(,,,,,,,,,,,,,)" = "(,,,,,,,,,,,,)" + TupleConPred "(,,,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,)" + TupleConPred "(,,,,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,,)" + TupleConPred "(,,,,,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,,,)" + +-- | calculate the result type of 'uncons' +type family Uncons a where + Uncons (a,b) = (a,b) + Uncons (a,b,c) = (a, (b,c)) + Uncons (a,b,c,d) = (a, (b,c,d)) + Uncons (a,b,c,d,e) = (a, (b,c,d,e)) + Uncons (a,b,c,d,e,f) = (a, (b,c,d,e,f)) + Uncons (a,b,c,d,e,f,g) = (a, (b,c,d,e,f,g)) + Uncons (a,b,c,d,e,f,g,h) = (a, (b,c,d,e,f,g,h)) + Uncons (a,b,c,d,e,f,g,h,i) = (a, (b,c,d,e,f,g,h,i)) + Uncons (a,b,c,d,e,f,g,h,i,j) = (a, (b,c,d,e,f,g,h,i,j)) + Uncons (a,b,c,d,e,f,g,h,i,j,k) = (a, (b,c,d,e,f,g,h,i,j,k)) + Uncons (a,b,c,d,e,f,g,h,i,j,k,l) = (a, (b,c,d,e,f,g,h,i,j,k,l)) + Uncons (a,b,c,d,e,f,g,h,i,j,k,l,m) = (a, (b,c,d,e,f,g,h,i,j,k,l,m)) + Uncons (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = (a, (b,c,d,e,f,g,h,i,j,k,l,m,n)) + Uncons (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = (a, (b,c,d,e,f,g,h,i,j,k,l,m,n,o)) + Uncons (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p) = (a, (b,c,d,e,f,g,h,i,j,k,l,m,n,o,p)) + Uncons a = (a, ()) + +-- | A constraint on any 'uncons'able data type, where +-- @a@ is the input type, and @(b,c)@ is the output type +type Unconsable a b c = (Generic a, Generic b, Generic c, Uncons a ~ (b, c), + Rep a ~ D1 (MetaOfD1 (Rep a)) (UnD1 (Rep a)), + Rep b ~ D1 (MetaOfD1 (Rep b)) (UnD1 (Rep b)), + Rep c ~ D1 (MetaOfD1 (Rep c)) (UnD1 (Rep c)), + UnconsableR (UnD1 (Rep a)), + HeadR (UnD1 (Rep a)) ~ (UnD1 (Rep b)), + TailR (UnD1 (Rep a)) ~ (UnD1 (Rep c))) + +-- | 'uncons' takes primitive, pair, tuple, +-- and produces a pair of its first data and the rest elements. +uncons :: Unconsable a b c => a -> (b, c) uncons x = let (a, b) = unconsR $ unM1 $ from x in (to $ M1 a, to $ M1 b) diff --git a/tuple-ops.cabal b/tuple-ops.cabal --- a/tuple-ops.cabal +++ b/tuple-ops.cabal @@ -1,30 +1,30 @@ -name: tuple-ops -version: 0.0.0.2 -category: Data -author: Jiasen Wu -maintainer: Jiasen Wu -homepage: https://github.com/pierric/tuple-ops -synopsis: various operations on n-ary tuples via GHC.Generics -description: Some operations on n-ary tuples, including 'uncons', 'cons', etc. This package distinguish itself from other packages - on tuple mainly on the the implementation under the cover. It converts Generic datatype into the its representation - form, and carries out the operations on there. The other point is that this package tends to treat non-tuples directly as - 1-ary, without need of 'OneTuple' or similar intermediate wrapper. -license: BSD3 -license-file: LICENSE -build-type: Simple -cabal-version: >= 1.24 - -Library - hs-source-dirs: src - exposed-modules: Data.Tuple.Ops - , Data.Tuple.Ops.Uncons - , Data.Tuple.Ops.Cons - , Data.Tuple.Ops.Internal - default-language: Haskell2010 - default-extensions: DataKinds - , TypeOperators - , KindSignatures - , TypeFamilies - , FlexibleInstances - build-depends: base >= 4.7 && < 5.0 +name: tuple-ops +version: 0.0.0.3 +category: Data +author: Jiasen Wu +maintainer: Jiasen Wu +homepage: https://github.com/pierric/tuple-ops +synopsis: various operations on n-ary tuples via GHC.Generics +description: Some operations on n-ary tuples, including 'uncons', 'cons', etc. This package distinguish itself from other packages + on tuple mainly on the the implementation under the cover. It converts Generic datatype into the its representation + form, and carries out the operations on there. The other point is that this package tends to treat non-tuples directly as + 1-ary, without need of 'OneTuple' or similar intermediate wrapper. +license: BSD3 +license-file: LICENSE +build-type: Simple +cabal-version: 1.24 + +Library + hs-source-dirs: src + exposed-modules: Data.Tuple.Ops + , Data.Tuple.Ops.Uncons + , Data.Tuple.Ops.Cons + , Data.Tuple.Ops.Internal + default-language: Haskell2010 + default-extensions: DataKinds + , TypeOperators + , KindSignatures + , TypeFamilies + , FlexibleInstances + build-depends: base >= 4.7 && < 5.0 , type-combinators == 0.2.4.3