Data.Prodder

The extensible product type

data Prod (xs :: [*])

An extensible product type

Instances

FoldProd Show xs => Show (Prod xs)

Showing extensible products.

Defined in Data.Prodder

Methods

showsPrec :: Int -> Prod xs -> ShowS

show :: Prod xs -> String

showList :: [Prod xs] -> ShowS

(Eq x, Eq (Prod xs)) => Eq (Prod (x ': xs))

Defined in Data.Prodder

Methods

(==) :: Prod (x ': xs) -> Prod (x ': xs) -> Bool

(/=) :: Prod (x ': xs) -> Prod (x ': xs) -> Bool

Eq (Prod ('[] :: [Type]))

Defined in Data.Prodder

Methods

(==) :: Prod '[] -> Prod '[] -> Bool

(/=) :: Prod '[] -> Prod '[] -> Bool

Construction and deconstruction

extract :: forall x xs. x `HasIndexIn` xs => Prod xs -> x

Extract a value at a particular index

index :: forall x xs. x `HasIndexIn` xs => Word

Computes the index of the given type in the given type level list.

tailN :: forall n xs. (KnownNat n, n <= Length xs) => Prod xs -> Prod (Tail n xs)

Takes the tail of a product after the nth element.

initN :: forall n xs. (KnownNat n, n <= Length xs) => Prod xs -> Prod (Init n xs)

Takes the initial length n segment of a product.

dropFirst :: forall x xs. Prod (x ': xs) -> Prod xs

Drop the first element of a product. Sometimes needed for better type inference and less piping around of constraints.

class Consume xs where

A typeclass that is useful to define the scott encoding/decoding for extensible products.

Methods

consume :: forall r. Prod xs -> Consumer xs r -> r

produceB :: (forall r. Consumer xs r -> r) -> ProdBuilder xs

extend1 :: x -> Consumer xs (ProdBuilder (x ': xs))

cmap :: (r -> r') -> Consumer xs r -> Consumer xs r'

Instances

Consume ('[] :: [Type])

Defined in Data.Prodder

Methods

consume :: Prod '[] -> Consumer '[] r -> r

produceB :: (forall r. Consumer '[] r -> r) -> ProdBuilder '[]

extend1 :: x -> Consumer '[] (ProdBuilder (x ': '[]))

cmap :: (r -> r') -> Consumer '[] r -> Consumer '[] r'

Consume xs => Consume (x ': xs)

Defined in Data.Prodder

Methods

consume :: Prod (x ': xs) -> Consumer (x ': xs) r -> r

produceB :: (forall r. Consumer (x ': xs) r -> r) -> ProdBuilder (x ': xs)

extend1 :: x0 -> Consumer (x ': xs) (ProdBuilder (x0 ': (x ': xs)))

cmap :: (r -> r') -> Consumer (x ': xs) r -> Consumer (x ': xs) r'

produce :: (KnownNat (Length xs), Consume xs) => (forall r. Consumer xs r -> r) -> Prod xs

empty :: Prod '[]

class ForAll c xs => FoldProd c xs where

A class for folding over a Prod using a function which only requires that every element of the product satisfy a certain constraint.

Methods

foldProd :: Monoid m => (forall a. c a => a -> m) -> Prod xs -> m

Instances

FoldProd c ('[] :: [Type])

Defined in Data.Prodder

Methods

foldProd :: Monoid m => (forall a. c a => a -> m) -> Prod '[] -> m

(c x, FoldProd c xs) => FoldProd c (x ': xs)

Defined in Data.Prodder

Methods

foldProd :: Monoid m => (forall a. c a => a -> m) -> Prod (x ': xs) -> m

toList :: forall c xs a. FoldProd c xs => (forall x. c x => x -> a) -> Prod xs -> [a]

type family ForAll c xs :: Constraint where ...

Equations

ForAll c '[] = ()

ForAll c (x ': xs) = (c x, ForAll c xs)

atType :: forall a b xs f. (a `HasIndexIn` xs, Functor f) => (a -> f b) -> Prod xs -> f (Prod (Replace a b xs))

Lens to modify one element of a product.

Efficient Iterative Construction

buildProd :: forall xs. KnownNat (Length xs) => ProdBuilder xs -> Prod xs

Execute a ProdBuilder, pulling out a Prod.

data ProdBuilder (xs :: [*])

A type for constructing products with linear memory use.

consB :: x -> ProdBuilder xs -> ProdBuilder (x ': xs)

Cons an element onto the head of a ProdBuilder.

emptyB :: ProdBuilder '[]

Empty ProdBuilder.

appendB :: ProdBuilder xs -> ProdBuilder ys -> ProdBuilder (xs <> ys)

Appends two ProdBuilders.

Type families

type family Index (n :: Nat) (xs :: [k]) where ...

A type family for indexing into lists of types.

Equations

Index 0 (x ': xs) = x

Index n (_ ': xs) = Index (n - 1) xs

type family IndexIn (x :: k) (xs :: [k]) where ...

A type family for computing the index of a type in a list of types.

Equations

IndexIn x (x ': xs) = 0

IndexIn x (y ': xs) = 1 + IndexIn x xs

class KnownNat (x `IndexIn` xs) => HasIndexIn x xs

A class that is used for convenience in order to make certain type signatures read more clearly.

Instances

KnownNat (IndexIn x xs) => HasIndexIn (x :: k) (xs :: [k])

Defined in Data.Prodder

type family Consumer xs r where ...

This is a reified pattern match on an extensible product

Equations

Consumer '[] r = r

Consumer (x ': xs) r = x -> Consumer xs r

type family (xs :: [k]) <> (ys :: [k]) :: [k] where ...

Equations

'[] <> ys = ys

(x ': xs) <> ys = x ': (xs <> ys)

type family Length (xs :: [k]) where ...

A type family for computing the length of a type level list

Equations

Length '[] = 0

Length (x ': xs) = 1 + Length xs

type family Tail n xs where ...

A type family for computing the tail of a type level list

Equations

Tail 0 xs = xs

Tail n (x ': xs) = Tail (n - 1) xs

type family Init n xs where ...

A type family for computing the initial segment of a type level list

Equations

Init 0 xs = '[]

Init n (x ': xs) = x ': Init (n - 1) xs

type family Replace x y xs where ...

Type family for replacing one type in a type level list with another

Equations

Replace x y (x ': xs) = y ': xs

Replace x y (z ': xs) = z ': Replace x y xs

Replace x y '[] = '[]

Rearranging and removing elements

class Strengthen xs ys where

A typeclass to rearrange and possibly remove things from a product.

Methods

strengthenP :: Prod xs -> ProdBuilder ys

Instances

Strengthen xs ('[] :: [Type])

Defined in Data.Prodder

Methods

strengthenP :: Prod xs -> ProdBuilder '[]

(Strengthen xs ys, HasIndexIn y xs) => Strengthen xs (y ': ys)

Defined in Data.Prodder

Methods

strengthenP :: Prod xs -> ProdBuilder (y ': ys)

strengthen :: (KnownNat (Length ys), Strengthen xs ys) => Prod xs -> Prod ys

Transforming extensible products

remap :: forall x y xs. x `HasIndexIn` xs => (x -> y) -> Prod xs -> Prod (Replace x y xs)

Replaces one type with another via a function

Picking out individual components of a product

class Selection def selector a where

A class for constructing the select function inductively.

Methods

select :: Prod def -> selector -> a

Instances

Selection def a a

Defined in Data.Prodder

Methods

select :: Prod def -> a -> a

(HasIndexIn x def, Selection def xs a) => Selection def (x -> xs) a

Defined in Data.Prodder

Methods

select :: Prod def -> (x -> xs) -> a

type family FieldsFromSelector def selector where ...

Extracts the fields intended from the given selector type.

Equations

FieldsFromSelector def (a -> b) = IndexIn a def ': FieldsFromSelector def b

FieldsFromSelector def (Identity a) = '[]

type family Selector def fields a where ...

A typeclass for creating a selection function which is valid on the given definition.

Equations

Selector def (field ': fields) a = Index field def -> Selector def fields a

Selector def '[] a = a