Data.Tuple.Ops.Internal

This module defins operations to manipulate the generic representation of tuple.

Documentation

newtype TupleR (f :: [* -> *]) x

Constructors

TupleR

Fields

• unTupleR :: Tuple (f <&> x)

class AppDistributive (a :: [* -> *]) where

prove that (a ++ b) & x == a & x ++ b & x

Minimal complete definition

appDistrWit

Methods

appDistrWit :: (Proxy a, Proxy b, Proxy x) -> Wit (((a ++ b) <&> x) ~ ((a <&> x) ++ (b <&> x)))

Instances

AppDistributive ([] (* -> *))

inductive proof on a case 1. a is []

Methods

appDistrWit :: (Proxy [* -> *] [* -> *], Proxy [* -> *] b, Proxy * x) -> Wit (([*] ~ (* <&> *) (((* -> *) ++ [* -> *]) b) x) ((* ++ (* <&> *) [* -> *] x) ((* <&> *) b x)))

AppDistributive as => AppDistributive ((:<) (* -> *) a as)

case 2. a is _ :< _

Methods

appDistrWit :: (Proxy [* -> *] (((* -> *) :< a) as), Proxy [* -> *] b, Proxy * x) -> Wit (([*] ~ (* <&> *) (((* -> *) ++ ((* -> *) :< a) as) b) x) ((* ++ (* <&> *) (((* -> *) :< a) as) x) ((* <&> *) b x)))

appDistrWitPassArg :: (f :*: g) x -> (Proxy (L f), Proxy (L g), Proxy x)

utility function to call appDistrWit

class Linearize (t :: * -> *) where

Representation of tuple are shaped in a balanced tree. L transforms the tree into a list, for further manipulation.

Minimal complete definition

linearize

Associated Types

type L t :: [* -> *]

Methods

linearize :: t x -> TupleR (L t) x

Instances

(Linearize v, Linearize u, AppDistributive (L u)) => Linearize ((:*:) * u v)

inductive case. preppend a product with what ever

Associated Types

type L ((* :*: u) v :: * -> *) :: [* -> *]

Methods

linearize :: (* :*: u) v x -> TupleR (L ((* :*: u) v)) x

Linearize (S1 * MetaS (Rec0 * t))

base case. sinleton

Associated Types

type L (S1 * MetaS (Rec0 * t) :: * -> *) :: [* -> *]

Methods

linearize :: S1 * MetaS (Rec0 * t) x -> TupleR (L (S1 * MetaS (Rec0 * t))) x

length' :: TupleR a x -> Proxy (Len a)

type family Half (a :: N) :: N where ...

calculate the half

Equations

Half (S Z) = Z

Half (S (S Z)) = S Z

Half (S (S n)) = S (Half n)

half :: Proxy n -> Proxy (Half n)

calculate the half

class Take (n :: N) (a :: [* -> *]) where

take the first n elements from a product

Minimal complete definition

take'

Associated Types

type T n a :: [* -> *]

Methods

take' :: Proxy n -> TupleR a x -> TupleR (T n a) x

Instances

Take Z xs

base case. take one out of singleton

Associated Types

type T (Z :: N) (xs :: [* -> *]) :: [* -> *]

Methods

take' :: Proxy N Z -> TupleR xs x -> TupleR (T Z xs) x

Take n as => Take (S n) ((:) (* -> *) a as)

inductive case. take (n+1) elements

Associated Types

type T (S n :: N) (((* -> *) ': a) as :: [* -> *]) :: [* -> *]

Methods

take' :: Proxy N (S n) -> TupleR (((* -> *) ': a) as) x -> TupleR (T (S n) (((* -> *) ': a) as)) x

class Drop (n :: N) (a :: [* -> *]) where

drop the first n elements from a product

Minimal complete definition

drop'

Associated Types

type D n a :: [* -> *]

Methods

drop' :: Proxy n -> TupleR a x -> TupleR (D n a) x

Instances

Drop Z as

base case. drop one from product

Associated Types

type D (Z :: N) (as :: [* -> *]) :: [* -> *]

Methods

drop' :: Proxy N Z -> TupleR as x -> TupleR (D Z as) x

Drop n as => Drop (S n) ((:) (* -> *) a as)

inductive case. drop (n+1) elements

Associated Types

type D (S n :: N) (((* -> *) ': a) as :: [* -> *]) :: [* -> *]

Methods

drop' :: Proxy N (S n) -> TupleR (((* -> *) ': a) as) x -> TupleR (D (S n) (((* -> *) ': a) as)) x

class Normalize (a :: [* -> *]) where

Normalize converts a linear product back into a balanced tree.

Minimal complete definition

normalize

Associated Types

type N a :: * -> *

Methods

normalize :: TupleR a x -> N a x

Instances

Normalize ((:) (* -> *) (S1 * MetaS (Rec0 * t)) ([] (* -> *)))

base case. singleton

Associated Types

type N (((* -> *) ': S1 * MetaS (Rec0 * t)) [* -> *] :: [* -> *]) :: * -> *

Methods

normalize :: TupleR (((* -> *) ': S1 * MetaS (Rec0 * t)) [* -> *]) x -> N (((* -> *) ': S1 * MetaS (Rec0 * t)) [* -> *]) x

(Take (Half ((+) N2 (Len (* -> *) c))) ((:<) (* -> *) a ((:<) (* -> *) b c)), Drop (Half ((+) N2 (Len (* -> *) c))) ((:<) (* -> *) a ((:<) (* -> *) b c)), Normalize (T (Half ((+) N2 (Len (* -> *) c))) ((:<) (* -> *) a ((:<) (* -> *) b c))), Normalize (D (Half ((+) N2 (Len (* -> *) c))) ((:<) (* -> *) a ((:<) (* -> *) b c)))) => Normalize ((:<) (* -> *) a ((:<) (* -> *) b c))

inductive case. product

Associated Types

type N (((* -> *) :< a) (((* -> *) :< b) c) :: [* -> *]) :: * -> *

Methods

normalize :: TupleR (((* -> *) :< a) (((* -> *) :< b) c)) x -> N (((* -> *) :< a) (((* -> *) :< b) c)) x

type MetaS = MetaSel Nothing NoSourceUnpackedness NoSourceStrictness DecidedLazy

type family UnRec0 t where ...

utility type function to trim the Rec0

Equations

UnRec0 (Rec0 t) = t

type family UnS1 t where ...

utility type function to trim the S1

Equations

UnS1 (S1 _ t) = t

type family UnD1 t where ...

utility type function to trim the D1

Equations

UnD1 (D1 _ t) = t

type family MetaOfD1 t where ...

utility type function to extract the meta information

Equations

MetaOfD1 (D1 m _) = m