summer-0.3.7.2: An implementation of extensible products and sums
Copyright(c) Samuel Schlesinger 2020
LicenseMIT
Maintainersgschlesinger@gmail.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Prodder

Description

 
Synopsis

The extensible product type

data Prod (xs :: [*]) Source #

An extensible product type

Instances

Instances details
FoldProd Show xs => Show (Prod xs) Source #

Showing extensible products.

Instance details

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)) Source # 
Instance details

Defined in Data.Prodder

Methods

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

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

Eq (Prod ('[] :: [Type])) Source # 
Instance details

Defined in Data.Prodder

Methods

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

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

Construction and deconstruction

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

Extract a value at a particular index

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

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) Source #

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) Source #

Takes the initial length n segment of a product.

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

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

class Consume xs where Source #

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

Methods

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

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

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

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

Instances

Instances details
Consume ('[] :: [Type]) Source # 
Instance details

Defined in Data.Prodder

Methods

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

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

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

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

Consume xs => Consume (x ': xs) Source # 
Instance details

Defined in Data.Prodder

Methods

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

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

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

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

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

class ForAll c xs => FoldProd c xs where Source #

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 Source #

Instances

Instances details
FoldProd c ('[] :: [Type]) Source # 
Instance details

Defined in Data.Prodder

Methods

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

(c x, FoldProd c xs) => FoldProd c (x ': xs) Source # 
Instance details

Defined in Data.Prodder

Methods

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

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

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

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)) Source #

Lens to modify one element of a product.

Efficient Iterative Construction

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

Execute a ProdBuilder, pulling out a Prod.

data ProdBuilder (xs :: [*]) Source #

A type for constructing products with linear memory use.

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

Cons an element onto the head of a ProdBuilder.

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

Appends two ProdBuilders.

Type families

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

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 ... Source #

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 Source #

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

Instances

Instances details
KnownNat (IndexIn x xs) => HasIndexIn (x :: k) (xs :: [k]) Source # 
Instance details

Defined in Data.Prodder

type family Consumer xs r where ... Source #

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 ... Source #

Equations

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

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

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 ... Source #

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 ... Source #

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 ... Source #

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 Source #

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

Methods

strengthenP :: Prod xs -> ProdBuilder ys Source #

Instances

Instances details
Strengthen xs ('[] :: [Type]) Source # 
Instance details

Defined in Data.Prodder

Methods

strengthenP :: Prod xs -> ProdBuilder '[] Source #

(Strengthen xs ys, HasIndexIn y xs) => Strengthen xs (y ': ys) Source # 
Instance details

Defined in Data.Prodder

Methods

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

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

Transforming extensible products

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

Replaces one type with another via a function

Picking out individual components of a product

class Selection def selector a where Source #

A class for constructing the select function inductively.

Methods

select :: Prod def -> selector -> a Source #

Instances

Instances details
Selection def a a Source # 
Instance details

Defined in Data.Prodder

Methods

select :: Prod def -> a -> a Source #

(HasIndexIn x def, Selection def xs a) => Selection def (x -> xs) a Source # 
Instance details

Defined in Data.Prodder

Methods

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

type family FieldsFromSelector def selector where ... Source #

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 ... Source #

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