Data.Prodder

Description: Extensible products

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

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

(<>) :: Semigroup a => a -> a -> a infixr 6

An associative operation.

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'

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