Data.Prodder

The extensible product type

data Prod (xs :: [*])

An extensible product type

Instances

(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

produce :: (forall r. Consumer xs r -> r) -> Prod xs

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

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

Instances

Consume ('[] :: [Type])

Defined in Data.Prodder

Methods

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

produce :: (forall r. Consumer '[] r -> r) -> Prod '[]

extend1 :: x -> Consumer '[] (Prod (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

produce :: (forall r. Consumer (x ': xs) r -> r) -> Prod (x ': xs)

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

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

Type families

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

Rearranging and removing elements

class Strengthen xs ys where

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

Methods

strengthen :: Prod xs -> Prod ys

Instances

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

Defined in Data.Prodder

Methods

strengthen :: Prod xs -> Prod '[]

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

Defined in Data.Prodder

Methods

strengthen :: Prod xs -> Prod (y ': 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