Data.Tuple.Ops.Internal

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

Documentation

data End a

a sentinial datatype that represents a empty product

Constructors

End

Instances

Linearize (S1 * MetaS (Rec0 * t)) End

base case 1. cons field with end

Associated Types

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

Methods

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

type L (S1 * MetaS (Rec0 * t)) End

type L (S1 * MetaS (Rec0 * t)) End = S1 * MetaS (Rec0 * t)

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

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

Minimal complete definition

linearize

Associated Types

type L t b :: * -> *

Methods

linearize :: t x -> b x -> L t b x

Instances

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

inductive case. preppend a product with what ever

Associated Types

type L ((* :*: u) v :: * -> *) (b :: * -> *) :: * -> *

Methods

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

Linearize (S1 * MetaS (Rec0 * t)) End

base case 1. cons field with end

Associated Types

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

Methods

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

Linearize (S1 * MetaS (Rec0 * t)) ((:*:) * b c)

base case 3. cons field1 with a product

Associated Types

type L (S1 * MetaS (Rec0 * t) :: * -> *) ((* :*: b) c :: * -> *) :: * -> *

Methods

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

Linearize (S1 * MetaS (Rec0 * t)) (S1 * MetaS (Rec0 * b))

base case 2. cons field1 with field2

Associated Types

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

Methods

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

type family Length a :: Nat where ...

calculate the number of fields of a product note: undefined on non-product rep

Equations

Length (S1 MetaS (Rec0 t)) = 1

Length (a :*: b) = Length a + Length b

length :: a x -> Proxy (Length a)

calculate the number of fields of a product

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

calculate the half

Equations

Half 1 = 0

Half 2 = 1

Half n = Half (n - 2) + 1

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

calculate the half

data SNat

Positive natural number in type level We rely on the SNat to define Take and Drop

Constructors

One

Succ SNat

type family ToSNat (a :: Nat) :: SNat where ...

transform the GHC's typelit into SNat

Equations

ToSNat 1 = One

ToSNat n = Succ (ToSNat (n - 1))

tosnat :: KnownNat n => Proxy n -> Proxy (ToSNat n)

transform the GHC's typelit into SNat

class Take (n :: SNat) (a :: * -> *) where

take the first n elements from a product

Minimal complete definition

take

Associated Types

type T n a :: * -> *

Methods

take :: Proxy n -> a x -> T n a x

Instances

Take One ((:*:) * a b)

base case 2. take one out of a product

Associated Types

type T (One :: SNat) ((* :*: a) b :: * -> *) :: * -> *

Methods

take :: Proxy SNat One -> (* :*: a) b x -> T One ((* :*: a) b) x

Take One (S1 * MetaS (Rec0 * t))

base case 1. take one out of singleton

Associated Types

type T (One :: SNat) (S1 * MetaS (Rec0 * t) :: * -> *) :: * -> *

Methods

take :: Proxy SNat One -> S1 * MetaS (Rec0 * t) x -> T One (S1 * MetaS (Rec0 * t)) x

Take n b => Take (Succ n) ((:*:) * a b)

inductive case. take (n+1) elements

Associated Types

type T (Succ n :: SNat) ((* :*: a) b :: * -> *) :: * -> *

Methods

take :: Proxy SNat (Succ n) -> (* :*: a) b x -> T (Succ n) ((* :*: a) b) x

class Drop (n :: SNat) (a :: * -> *) where

drop the first n elements from a product

Minimal complete definition

drop

Associated Types

type D n a :: * -> *

Methods

drop :: Proxy n -> a x -> D n a x

Instances

Drop One ((:*:) * a b)

base case 1. drop one from product

Associated Types

type D (One :: SNat) ((* :*: a) b :: * -> *) :: * -> *

Methods

drop :: Proxy SNat One -> (* :*: a) b x -> D One ((* :*: a) b) x

Drop n b => Drop (Succ n) ((:*:) * a b)

inductive case. drop (n+1) elements

Associated Types

type D (Succ n :: SNat) ((* :*: a) b :: * -> *) :: * -> *

Methods

drop :: Proxy SNat (Succ n) -> (* :*: a) b x -> D (Succ n) ((* :*: a) b) 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 :: a x -> N a x

Instances

(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)

inductive case. product

Associated Types

type N ((* :*: a) b :: * -> *) :: * -> *

Methods

normalize :: (* :*: a) b x -> N ((* :*: a) b) x

Normalize (S1 * MetaS (Rec0 * t))

base case 1. singleton

Associated Types

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

Methods

normalize :: S1 * MetaS (Rec0 * t) x -> N (S1 * MetaS (Rec0 * t)) 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