tuple-ops 0.0.0.0 → 0.0.0.1

raw patch · 3 files changed

+129/−125 lines, 3 filesdep +type-combinators

Dependencies added: type-combinators

Files

src/Data/Tuple/Ops/Internal.hs +89/−100
src/Data/Tuple/Ops/Uncons.hs +37/−22
tuple-ops.cabal +3/−3

src/Data/Tuple/Ops/Internal.hs view

@@ -13,139 +13,125 @@ -- representation of tuple.
 ------------------------------------------------------------
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module Data.Tuple.Ops.Internal where
 
-import qualified GHC.Generics as G
-import GHC.Generics (Generic(..), (:*:)(..), (:+:)(..), Rec0, C1, D1, S1, M1(..), U1, K1(..))
-import GHC.TypeLits
+import GHC.Generics ((:*:)(..), Rec0, D1, S1, Meta(..), SourceUnpackedness(..), SourceStrictness(..), DecidedStrictness(..))
 import Data.Proxy
-import qualified Prelude as P 
-import Prelude (Maybe(..), Int, Word, Char, Float, Double, Bool(..), ($))
+import Data.Type.Combinator
+import Data.Type.Product
+import Type.Family.List
+import Type.Class.Witness
+import qualified Type.Family.Nat as Nat
 
--- | a sentinial datatype that represents a empty product
-data End a = End
+-- '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)}
 
--- | Representation of tuple are shaped in a balanced tree. 
--- 'L' transforms the tree into a line, for further manipulation.
-class Linearize (t :: * -> *) (b :: * -> *) where
-  type L t b :: * -> *
-  linearize :: t x -> b x -> L t b 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
 
--- | base case 1. cons field with end
-instance Linearize (S1 MetaS (Rec0 t)) End where
-    type L (S1 MetaS (Rec0 t)) End = (S1 MetaS (Rec0 t))
-    linearize a End = a
+-- | utility function to call 'appDistrWit'
+appDistrWitPassArg :: (f :*: g) x -> (Proxy (L f), Proxy (L g), Proxy x)
+appDistrWitPassArg _ = (Proxy, Proxy, Proxy)
 
--- note that it is not possible to combine base case 2 and 3, which results in
--- a ambiguous instantiation with base case 1
---
--- | base case 2. cons field1 with field2 
-instance Linearize (S1 MetaS (Rec0 t)) (S1 MetaS (Rec0 b)) where
-    type L (S1 MetaS (Rec0 t)) (S1 MetaS (Rec0 b)) = S1 MetaS (Rec0 t) :*: S1 MetaS (Rec0 b)
-    linearize a b = a :*: b
+-- | 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 3. cons field1 with a product
-instance Linearize (S1 MetaS (Rec0 t)) (b :*: c) where
-    type L (S1 MetaS (Rec0 t)) (b :*: c) = S1 MetaS (Rec0 t) :*: b :*: c
-    linearize a b = a :*: b
+-- | 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 b, Linearize u (L v b)) => Linearize (u :*: v) b where
-    type L (u :*: v) b = L u (L v b)
-    linearize (a :*: b) c = linearize a (linearize b c)
+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)
 
--- | calculate the number of fields of a product
--- note: undefined on non-product rep
-type family Length a :: Nat where
-    Length (S1 MetaS (Rec0 t)) = 1
-    Length (a :*: b) = Length a + Length b
--- | calculate the number of fields of a product
-length :: a x -> Proxy (Length a)
-length _ = Proxy
+length' :: TupleR a x -> Proxy (Nat.Len a)
+length' _ = Proxy
 
 -- | calculate the half
-type family Half (a :: Nat) :: Nat where
-    Half 1 = 0
-    Half 2 = 1
-    Half n = Half (n - 2) + 1
+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 :: KnownNat n => Proxy n -> Proxy (Half n)
+half :: Proxy n -> Proxy (Half n)
 half _ = Proxy
 
--- | Positive natural number in type level
--- We rely on the SNat to define Take and Drop
-data SNat = One | Succ SNat
--- | transform the GHC's typelit into SNat
-type family ToSNat (a :: Nat) :: SNat where
-    ToSNat 1 = One
-    ToSNat n = Succ (ToSNat (n - 1))
--- | transform the GHC's typelit into SNat
-tosnat :: KnownNat n => Proxy n -> Proxy (ToSNat n)
-tosnat _ = Proxy
-
 -- | take the first n elements from a product
-class Take (n :: SNat) (a :: * -> *) where
-    type T n a :: * -> *
-    take :: Proxy n -> a x -> T n a x
-
--- | base case 1. take one out of singleton
-instance Take One (S1 MetaS (Rec0 t)) where
-    type T One (S1 MetaS (Rec0 t)) = S1 MetaS (Rec0 t)
-    take _ a = a
+class Take (n :: Nat.N) (a :: [* -> *]) where
+    type T n a :: [* -> *]
+    take' :: Proxy n -> TupleR a x -> TupleR (T n a) x
 
--- | base case 2. take one out of a product
-instance Take One (a :*: b) where
-    type T One (a :*: b) = a
-    take _ (a :*: _) = a
+-- | 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 b => Take (Succ n) (a :*: b) where
-    type T (Succ n) (a :*: b) = a :*: T n b
-    take (_ :: Proxy (Succ n)) (a :*: b) = a :*: take (Proxy :: Proxy n) b
+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 :: SNat) (a :: * -> *) where
-    type D n a :: * -> *
-    drop :: Proxy n -> a x -> D n a x
+class Drop (n :: Nat.N) (a :: [* -> *]) where
+    type D n a :: [* -> *]
+    drop' :: Proxy n -> TupleR a x -> TupleR (D n a) x
 
--- | base case 1. drop one from product
-instance Drop One (a :*: b) where
-    type D One (a :*: b) = b
-    drop _ (_ :*: b) = b
+-- | 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 b => Drop (Succ n) (a :*: b) where
-    type D (Succ n) (a :*: b) = D n b
-    drop (_ :: Proxy (Succ n)) (a :*: b) = drop (Proxy :: Proxy n) b
+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 :: a x -> N a x
+class Normalize (a :: [* -> *]) where
+    type N a :: * -> *
+    normalize :: TupleR a x -> N a x
 
--- | base case 1. singleton
-instance Normalize (S1 MetaS (Rec0 t)) where
-    type N (S1 MetaS (Rec0 t)) = S1 MetaS (Rec0 t)
-    normalize a = a
+-- | 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 (KnownNat (Length a + Length b),
-          KnownNat (Half (Length a + Length b)),
-          Take (ToSNat (Half (Length a + Length b))) (a :*: b),
-          Drop (ToSNat (Half (Length a + Length b))) (a :*: b),
-          Normalize ((T (ToSNat (Half (Length a + Length b))) (a :*: b))), 
-          Normalize ((D (ToSNat (Half (Length a + Length b))) (a :*: b)))) 
-    => Normalize (a :*: b) where
-    type N (a :*: b) = N (T (ToSNat (Half (Length a + Length b))) (a :*: b)) :*: 
-                       N (D (ToSNat (Half (Length a + Length b))) (a :*: b))
-    normalize v = let n1 = length v :: Proxy (Length a + Length b)
-                      n2 = tosnat $ half n1
-                  in normalize (take n2 v) :*: normalize (drop n2 v)
+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 = 'G.MetaSel 'Nothing 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy
+type MetaS = 'MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy
 -- | utility type function to trim the Rec0 
 type family UnRec0 t where
     UnRec0 (Rec0 t) = t
@@ -155,3 +141,6 @@ -- | 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

src/Data/Tuple/Ops/Uncons.hs view

@@ -22,31 +22,35 @@ --
 ------------------------------------------------------------
 {-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
 
-module Data.Tuple.Ops.Uncons (uncons, Uncons) where
+module Data.Tuple.Ops.Uncons (uncons, Uncons, Unconsable) where
 
-import qualified GHC.Generics as G
-import GHC.Generics (Generic(..), (:*:)(..), (:+:)(..), Rec0, C1, D1, S1, M1(..), U1, K1(..))
-import GHC.TypeLits
+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
 
 -- | representation of a pair
-type RepOfPair t1 t2 = C1 ('G.MetaCons "(,)" 'G.PrefixI 'False) (S1 MetaS (Rec0 t1) :*: S1 MetaS (Rec0 t2))
+type RepOfPair t1 t2 = C1 ('MetaCons "(,)" 'PrefixI 'False) (S1 MetaS (Rec0 t1) :*: S1 MetaS (Rec0 t2))
 -- | representation of a tuple of arity > 2, in which @/u/@ is of the form @_ :*: _@
-type RepOfTuple c u = C1 ('G.MetaCons c 'G.PrefixI 'False) u 
+type RepOfTuple c u = C1 ('MetaCons c 'PrefixI 'False) u 
 
 -- | 'HeadR' is a type function that takes the first element of a tuple
 type family HeadR (f :: * -> *) :: * -> * where
-    HeadR (C1 mc (S1 ms (G.URec a))) = C1 mc (S1 ms (G.URec a))
+    HeadR (C1 mc (S1 ms (URec a))) = C1 mc (S1 ms (URec a))
     HeadR (a :+: b) = a :+: b
     HeadR (RepOfPair t1 t2) = UnD1 (Rep t1)
-    HeadR (RepOfTuple tcon (a :*: b :*: c)) = UnD1 (Rep (UnRec0 (UnS1 (T One (L (a :*: b :*: c) End)))))
+    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 (G.URec a))) = C1 ('G.MetaCons "()" 'G.PrefixI 'False) U1
-    TailR (a :+: b) = C1 ('G.MetaCons "()" 'G.PrefixI 'False) U1
+    TailR (C1 mc (S1 ms (URec a))) = C1 ('MetaCons "()" 'PrefixI 'False) U1
+    TailR (a :+: b) = C1 ('MetaCons "()" 'PrefixI 'False) U1
     TailR (RepOfPair t1 t2) = UnD1 (Rep t2)
-    TailR (RepOfTuple tcon (a :*: b :*: c)) = RepOfTuple (TupleConPred tcon) (N (D One (L (a :*: b :*: c) End)))
+    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 UnconsR f where
@@ -55,7 +59,7 @@ -- | primitive datatype
 -- 'HeadR' is the datatype itself
 -- 'TailR' is ()
-instance UnconsR (C1 mc (S1 ms (G.URec a))) where
+instance UnconsR (C1 mc (S1 ms (URec a))) where
     unconsR a = (a, unM1 (from ()))
 
 -- | sum datatype
@@ -75,12 +79,17 @@ -- | tuple of arity > 2
 -- 'HeadR' is the first element
 -- 'TailR' is the rest all elements
-instance (Linearize c End, Linearize b (L c End), Linearize a (L b (L c End)),
-          L a (L b (L c End)) ~ (S1 MetaS (Rec0 t) :*: w), 
+instance (Linearize (a :*: b :*: c), L (a :*: b :*: c) ~ (S1 MetaS (Rec0 t) : w), 
           Generic t, Rep t ~ D1 hm hc, Normalize w) 
     => UnconsR (RepOfTuple tcon (a :*: b :*: c)) where
-    unconsR a = case linearize (unM1 a) End of
-                  u :*: v -> (unM1 $ from $ unK1 $ unM1 u, M1 $ normalize v)
+    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)
+    -- unconsR a = case linearize (unM1 a) of
+    --               (TupleR (u :< v) :: TupleR (S1 MetaS (Rec0 t) : w) x) -> 
+    --                 (unM1 $ from $ (unK1 (unM1 (getI u)) :: t), M1 $ normalize $ (TupleR v :: TupleR w x))
 
 -- | calculate the tuple constructor of the size 1 smaller
 -- upto the tupel of arity of 16
@@ -120,11 +129,17 @@     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, ())
 
--- | 'uncons' takes primitive, pair, tuple
+-- | 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)),
+                         UnconsR (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 :: (Generic a, Rep a ~ D1 ma ra, Uncons a ~ (b, c),
-           Generic b, Rep b ~ D1 mb rb,
-           Generic c, Rep c ~ D1 mc rc,
-           UnconsR ra, HeadR ra ~ rb, TailR ra ~ rc)
-       => a -> Uncons a 
+uncons :: Unconsable a b c => a -> (b, c)
 uncons x = let (a, b) = unconsR $ unM1 $ from x in (to $ M1 a, to $ M1 b)

tuple-ops.cabal view

@@ -1,5 +1,5 @@ name:                       tuple-ops
-version:                    0.0.0.0
+version:                    0.0.0.1
 category:                   Data
 author:                     Jiasen Wu
 maintainer:                 Jiasen Wu <jiasenwu@hotmail.com>
@@ -21,6 +21,6 @@                           , TypeOperators
                           , KindSignatures
                           , TypeFamilies
-                          , UndecidableInstances
                           , FlexibleInstances
-    build-depends:          base >= 4.7 && < 5.0+    build-depends:          base >= 4.7 && < 5.0
+                          , type-combinators == 0.2.4.3