Safe Haskell	None
Language	Haskell98

Data.Row.Internal

Contents

Rows
Row Operations
Row Classes
Helper functions

Description

This module implements the internals of open records and variants.

Synopsis

Rows

newtype Row a Source #

The kind of rows. This type is only used as a datakind. A row is a typelevel entity telling us which symbols are associated with which types.

Constructors

R [LT a]

A row is a list of symbol-to-type pairs that should always be sorted lexically by the symbol. The constructor is exported here (because this is an internal module) but should not be exported elsewhere.

data Label (s :: Symbol) Source #

A label

Constructors

Label

Instances

(≈) Symbol x y => IsLabel x (Label y) Source #
Methods fromLabel :: Label y #
KnownSymbol s => Show (Label s) Source #
Methods showsPrec :: Int -> Label s -> ShowS # show :: Label s -> String # showList :: [Label s] -> ShowS #

class KnownSymbol (n :: Symbol) #

This class gives the string associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.

Since: 4.7.0.0

Minimal complete definition

symbolSing

data LT a Source #

The kind of elements of rows. Each element is a label and its associated type.

Constructors

Symbol :-> a

Instances

(KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ, Forall (R * ρ) c) => Forall (R * ((:) (LT ) ((:->) ℓ τ) ρ)) c Source #
Methods metamorph :: Proxy (* -> ) h -> (f (Empty ) -> g (Empty )) -> (forall (a :: Symbol) b (d :: [LT ]). (KnownSymbol a, c b) => Label a -> f (R * ((LT * ': (* :-> a) b) d)) -> (h b, f (R * d))) -> (forall (a :: Symbol) b (d :: [LT ]). (KnownSymbol a, c b, FoldStep a b d) => Label a -> h b -> g (R d) -> g (R * ((LT * ': (* :-> a) b) d))) -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ)) Source # metamorph' :: Proxy (* -> ) h -> (f (Empty ) -> g (Empty )) -> (forall (a :: Symbol) b (d :: [LT ]). (KnownSymbol a, c b) => Label a -> f (R * ((LT * ': (* :-> a) b) d)) -> Either (h b) (f (R * d))) -> (forall (a :: Symbol) b (d :: [LT ]). (KnownSymbol a, c b, FoldStep a b d) => Label a -> Either (h b) (g (R d)) -> g (R * ((LT * ': (* :-> a) b) d))) -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ)) Source #
Forall (R * ([] (LT *))) c Source #
Methods metamorph :: Proxy (* -> ) h -> (f (Empty ) -> g (Empty )) -> (forall (ℓ :: Symbol) τ (ρ :: [LT ]). (KnownSymbol ℓ, c τ) => Label ℓ -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> (h τ, f (R * ρ))) -> (forall (ℓ :: Symbol) τ (ρ :: [LT ]). (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> h τ -> g (R ρ) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ))) -> f (R * [LT ]) -> g (R [LT ]) Source # metamorph' :: Proxy ( -> ) h -> (f (Empty ) -> g (Empty )) -> (forall (ℓ :: Symbol) τ (ρ :: [LT ]). (KnownSymbol ℓ, c τ) => Label ℓ -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> Either (h τ) (f (R * ρ))) -> (forall (ℓ :: Symbol) τ (ρ :: [LT ]). (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> Either (h τ) (g (R ρ)) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ))) -> f (R * [LT ]) -> g (R [LT *]) Source #
(KnownSymbol ℓ, c τ1, c τ2, Forall2 (R * ρ1) (R * ρ2) c) => Forall2 (R * ((:) (LT ) ((:->) ℓ τ1) ρ1)) (R * ((:) (LT ) ((:->) ℓ τ2) ρ2)) c Source #
Methods metamorph2 :: Proxy (* -> ) f' -> Proxy ( -> ) g' -> (f (Empty ) -> g (Empty ) -> h (Empty ) (Empty )) -> (forall (a :: Symbol) τ10 τ20 (ρ10 :: [LT ]) (ρ20 :: [LT ]). (KnownSymbol a, c τ10, c τ20) => Label a -> f (R ((LT * ': (* :-> a) τ10) ρ10)) -> g (R * ((LT * ': (* :-> a) τ20) ρ20)) -> ((f' τ10, f (R * ρ10)), (g' τ20, g (R * ρ20)))) -> (forall (a :: Symbol) τ10 τ20 (ρ10 :: [LT ]) (ρ20 :: [LT ]). (KnownSymbol a, c τ10, c τ20) => Label a -> f' τ10 -> g' τ20 -> h (R * ρ10) (R * ρ20) -> h (R * ((LT * ': (* :-> a) τ10) ρ10)) (R * ((LT * ': (* :-> a) τ20) ρ20))) -> f (R * ((LT * ': (* :-> ℓ) τ1) ρ1)) -> g (R * ((LT * ': (* :-> ℓ) τ2) ρ2)) -> h (R * ((LT * ': (* :-> ℓ) τ1) ρ1)) (R * ((LT * ': (* :-> ℓ) τ2) ρ2)) Source #
Forall2 (R * ([] (LT ))) (R ([] (LT *))) c Source #
Methods metamorph2 :: Proxy (* -> ) f' -> Proxy ( -> ) g' -> (f (Empty ) -> g (Empty ) -> h (Empty ) (Empty )) -> (forall (ℓ :: Symbol) τ1 τ2 (ρ1 :: [LT ]) (ρ2 :: [LT ]). (KnownSymbol ℓ, c τ1, c τ2) => Label ℓ -> f (R ((LT * ': (* :-> ℓ) τ1) ρ1)) -> g (R * ((LT * ': (* :-> ℓ) τ2) ρ2)) -> ((f' τ1, f (R * ρ1)), (g' τ2, g (R * ρ2)))) -> (forall (ℓ :: Symbol) τ1 τ2 (ρ1 :: [LT ]) (ρ2 :: [LT ]). (KnownSymbol ℓ, c τ1, c τ2) => Label ℓ -> f' τ1 -> g' τ2 -> h (R * ρ1) (R * ρ2) -> h (R * ((LT * ': (* :-> ℓ) τ1) ρ1)) (R * ((LT * ': (* :-> ℓ) τ2) ρ2))) -> f (R * [LT ]) -> g (R [LT ]) -> h (R [LT ]) (R [LT *]) Source #
(KnownSymbol l, Switch (R * v) (R * r) b) => Switch (R * ((:) (LT ) ((:->) l a) v)) (R * ((:) (LT ) ((:->) l (a -> b)) r)) b Source #
Methods switch :: Var (R * ((LT * ': (* :-> l) a) v)) -> Rec (R * ((LT * ': (* :-> l) (a -> b)) r)) -> b Source # caseon :: Rec (R * ((LT * ': (* :-> l) (a -> b)) r)) -> Var (R * ((LT * ': (* :-> l) a) v)) -> b Source #
Switch (R * ([] (LT ))) (R ([] (LT *))) x Source #
Methods switch :: Var (R * [LT ]) -> Rec (R [LT ]) -> x Source # caseon :: Rec (R [LT ]) -> Var (R [LT *]) -> x Source #

type Empty = R '[] Source #

Type level version of empty

data HideType where Source #

Elements stored in a Row type are usually hidden.

Constructors

HideType :: a -> HideType

Row Operations

type family Extend (l :: Symbol) (a :: *) (r :: Row *) :: Row * where ... Source #

Type level Row extension

Equations

Extend l a (R x) = R (Inject (l :-> a) x)

type family Modify (l :: Symbol) (a :: *) (r :: Row *) :: Row * where ... Source #

Type level Row modification

Equations

Modify l a (R ρ) = R (ModifyR l a ρ)

type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row *) :: Row * where ... Source #

Type level row renaming

Equations

Rename l l' r = Extend l' (r .! l) (r .- l)

type family (r :: Row *) .\ (l :: Symbol) :: Constraint where ... infixl 4 Source #

Does the row lack (i.e. it does not have) the specified label?

Equations

(R r) .\ l = LacksR l r r

type family (r :: Row *) .! (t :: Symbol) :: * where ... infixl 5 Source #

Type level label fetching

Equations

(R r) .! l = Get l r

type family (r :: Row *) .- (s :: Symbol) :: Row * where ... infixl 6 Source #

Type level Row element removal

Equations

(R r) .- l = R (Remove l r)

type family (l :: Row *) .+ (r :: Row *) :: Row * where ... infixl 6 Source #

Type level Row append

Equations

(R l) .+ (R r) = R (Merge l r)

type family (l :: Row *) .\\ (r :: Row *) :: Row * where ... infixl 6 Source #

Type level Row difference. That is, l .\\ r is the row remaining after removing any matching elements of r from l.

Equations

(R l) .\\ (R r) = R (Diff l r)

type (.==) (l :: Symbol) (a :: *) = Extend l a Empty infix 7 Source #

A type level way to create a singleton Row.

type family (l :: Row *) .\/ (r :: Row *) where ... Source #

The minimum join of the two rows.

Equations

(R l) .\/ (R r) = R (MinJoinR l r)

class Lacks (l :: Symbol) (r :: Row *) Source #

Alias for .\. It is a class rather than an alias, so that it can be partially applied.

Instances

(.\) r l => Lacks l r Source #

class (r .! l) ≈ a => HasType l a r Source #

Alias for (r .! l) ≈ a. It is a class rather than an alias, so that it can be partially applied.

Instances

(≈) * ((.!) r l) a => HasType l a r Source #

Row Classes

type family Labels (r :: Row a) where ... Source #

The labels in a Row.

Equations

Labels (R '[]) = '[]
Labels (R ((l :-> a) ': xs)) = l ': Labels (R xs)

labels :: forall ρ c s. (IsString s, Forall ρ c) => [s] Source #

Return a list of the labels in a row type.

labels' :: forall ρ s. (IsString s, Forall ρ Unconstrained1) => [s] Source #

Return a list of the labels in a row type and is specialized to the Unconstrained1 constraint.

class Forall (r :: Row *) (c :: * -> Constraint) where Source #

Any structure over a row in which every element is similarly constrained can be metamorphized into another structure over the same row.

Minimal complete definition

metamorph, metamorph'

Methods

metamorph Source #

Arguments

:: forall (f :: Row * -> ) (g :: Row -> ) (h :: -> *). Proxy h
-> (f Empty -> g Empty)	The way to transform the empty element
-> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> f (R ((ℓ :-> τ) ': ρ)) -> (h τ, f (R ρ)))	The unfold
-> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> h τ -> g (R ρ) -> g (R ((ℓ :-> τ) ': ρ)))	The fold
-> f r	The input structure
-> g r

A metamorphism is an unfold followed by a fold. This one is for product-like row-types (e.g. Rec).

metamorph' Source #

Arguments

:: forall (f :: Row * -> ) (g :: Row -> ) (h :: -> *). Proxy h
-> (f Empty -> g Empty)	The way to transform the empty element
-> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> f (R ((ℓ :-> τ) ': ρ)) -> Either (h τ) (f (R ρ)))	The unfold
-> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> Either (h τ) (g (R ρ)) -> g (R ((ℓ :-> τ) ': ρ)))	The fold
-> f r	The input structure
-> g r

A metamorphism is an unfold followed by a fold. This one is for sum-like row-types (e.g. Var).

Instances

(KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ, Forall (R * ρ) c) => Forall (R * ((:) (LT ) ((:->) ℓ τ) ρ)) c Source #
Methods metamorph :: Proxy (* -> ) h -> (f (Empty ) -> g (Empty )) -> (forall (a :: Symbol) b (d :: [LT ]). (KnownSymbol a, c b) => Label a -> f (R * ((LT * ': (* :-> a) b) d)) -> (h b, f (R * d))) -> (forall (a :: Symbol) b (d :: [LT ]). (KnownSymbol a, c b, FoldStep a b d) => Label a -> h b -> g (R d) -> g (R * ((LT * ': (* :-> a) b) d))) -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ)) Source # metamorph' :: Proxy (* -> ) h -> (f (Empty ) -> g (Empty )) -> (forall (a :: Symbol) b (d :: [LT ]). (KnownSymbol a, c b) => Label a -> f (R * ((LT * ': (* :-> a) b) d)) -> Either (h b) (f (R * d))) -> (forall (a :: Symbol) b (d :: [LT ]). (KnownSymbol a, c b, FoldStep a b d) => Label a -> Either (h b) (g (R d)) -> g (R * ((LT * ': (* :-> a) b) d))) -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ)) Source #
Forall (R * ([] (LT *))) c Source #
Methods metamorph :: Proxy (* -> ) h -> (f (Empty ) -> g (Empty )) -> (forall (ℓ :: Symbol) τ (ρ :: [LT ]). (KnownSymbol ℓ, c τ) => Label ℓ -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> (h τ, f (R * ρ))) -> (forall (ℓ :: Symbol) τ (ρ :: [LT ]). (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> h τ -> g (R ρ) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ))) -> f (R * [LT ]) -> g (R [LT ]) Source # metamorph' :: Proxy ( -> ) h -> (f (Empty ) -> g (Empty )) -> (forall (ℓ :: Symbol) τ (ρ :: [LT ]). (KnownSymbol ℓ, c τ) => Label ℓ -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> Either (h τ) (f (R * ρ))) -> (forall (ℓ :: Symbol) τ (ρ :: [LT ]). (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> Either (h τ) (g (R ρ)) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ))) -> f (R * [LT ]) -> g (R [LT *]) Source #

class Forall2 (r1 :: Row *) (r2 :: Row *) (c :: * -> Constraint) where Source #

Any structure over two rows in which every element of both rows satisfies the given constraint can be metamorphized into another structure over both of the rows. TODO: Perhaps it should be over two constraints? But this hasn't seemed necessary in practice.

Minimal complete definition

metamorph2

Methods

metamorph2 :: forall (f :: Row * -> *) (g :: Row * -> *) (h :: Row * -> Row * -> *) (f' :: * -> *) (g' :: * -> *). Proxy f' -> Proxy g' -> (f Empty -> g Empty -> h Empty Empty) -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1, c τ2) => Label ℓ -> f (R ((ℓ :-> τ1) ': ρ1)) -> g (R ((ℓ :-> τ2) ': ρ2)) -> ((f' τ1, f (R ρ1)), (g' τ2, g (R ρ2)))) -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1, c τ2) => Label ℓ -> f' τ1 -> g' τ2 -> h (R ρ1) (R ρ2) -> h (R ((ℓ :-> τ1) ': ρ1)) (R ((ℓ :-> τ2) ': ρ2))) -> f r1 -> g r2 -> h r1 r2 Source #

A metamorphism is a fold followed by an unfold. Here, we fold both of the inputs.

Instances

(KnownSymbol ℓ, c τ1, c τ2, Forall2 (R * ρ1) (R * ρ2) c) => Forall2 (R * ((:) (LT ) ((:->) ℓ τ1) ρ1)) (R * ((:) (LT ) ((:->) ℓ τ2) ρ2)) c Source #
Methods metamorph2 :: Proxy (* -> ) f' -> Proxy ( -> ) g' -> (f (Empty ) -> g (Empty ) -> h (Empty ) (Empty )) -> (forall (a :: Symbol) τ10 τ20 (ρ10 :: [LT ]) (ρ20 :: [LT ]). (KnownSymbol a, c τ10, c τ20) => Label a -> f (R ((LT * ': (* :-> a) τ10) ρ10)) -> g (R * ((LT * ': (* :-> a) τ20) ρ20)) -> ((f' τ10, f (R * ρ10)), (g' τ20, g (R * ρ20)))) -> (forall (a :: Symbol) τ10 τ20 (ρ10 :: [LT ]) (ρ20 :: [LT ]). (KnownSymbol a, c τ10, c τ20) => Label a -> f' τ10 -> g' τ20 -> h (R * ρ10) (R * ρ20) -> h (R * ((LT * ': (* :-> a) τ10) ρ10)) (R * ((LT * ': (* :-> a) τ20) ρ20))) -> f (R * ((LT * ': (* :-> ℓ) τ1) ρ1)) -> g (R * ((LT * ': (* :-> ℓ) τ2) ρ2)) -> h (R * ((LT * ': (* :-> ℓ) τ1) ρ1)) (R * ((LT * ': (* :-> ℓ) τ2) ρ2)) Source #
Forall2 (R * ([] (LT ))) (R ([] (LT *))) c Source #
Methods metamorph2 :: Proxy (* -> ) f' -> Proxy ( -> ) g' -> (f (Empty ) -> g (Empty ) -> h (Empty ) (Empty )) -> (forall (ℓ :: Symbol) τ1 τ2 (ρ1 :: [LT ]) (ρ2 :: [LT ]). (KnownSymbol ℓ, c τ1, c τ2) => Label ℓ -> f (R ((LT * ': (* :-> ℓ) τ1) ρ1)) -> g (R * ((LT * ': (* :-> ℓ) τ2) ρ2)) -> ((f' τ1, f (R * ρ1)), (g' τ2, g (R * ρ2)))) -> (forall (ℓ :: Symbol) τ1 τ2 (ρ1 :: [LT ]) (ρ2 :: [LT ]). (KnownSymbol ℓ, c τ1, c τ2) => Label ℓ -> f' τ1 -> g' τ2 -> h (R * ρ1) (R * ρ2) -> h (R * ((LT * ': (* :-> ℓ) τ1) ρ1)) (R * ((LT * ': (* :-> ℓ) τ2) ρ2))) -> f (R * [LT ]) -> g (R [LT ]) -> h (R [LT ]) (R [LT *]) Source #

class Unconstrained1 a Source #

A null constraint of one argument

Instances

Unconstrained1 k a Source #

Helper functions

show' :: (IsString s, Show a) => a -> s Source #

A helper function for showing labels

toKey :: forall s. KnownSymbol s => Label s -> Text Source #

A helper function to turn a Label directly into Text.

type (≈) a b = a ~ b infix 4 Source #

A lower fixity operator for type equality

type WellBehaved ρ = (Forall ρ Unconstrained1, AllUniqueLabels ρ) Source #

A convenient way to provide common, easy constraints

type family AllUniqueLabels (r :: Row *) :: Constraint where ... Source #

Are all of the labels in this Row unique?

Equations

AllUniqueLabels (R r) = AllUniqueLabelsR r

type family Zip (r1 :: Row *) (r2 :: Row *) where ... Source #

Zips two rows together to create a Row of the pairs. The two rows must have the same set of labels.

Equations

Zip (R r1) (R r2) = R (ZipR r1 r2)

type family Map (f :: a -> b) (r :: Row a) :: Row b where ... Source #

Map a type level function over a Row.

Equations

Map f (R r) = R (MapR f r)

type family Subset (r1 :: Row *) (r2 :: Row *) :: Constraint where ... Source #

Is the first row a subset of the second?

Equations

Subset (R r1) (R r2) = SubsetR r1 r2

type Disjoint l r = (WellBehaved l, WellBehaved r, Subset l (l .+ r), Subset r (l .+ r), ((l .+ r) .\\ l) ≈ r, ((l .+ r) .\\ r) ≈ l) Source #

A type synonym for disjointness.

mapForall :: forall f c ρ. Forall ρ c :- Forall (Map f ρ) (IsA c f) Source #

This allows us to derive a `Forall (Map f r) ..` from a `Forall r ..`.

freeForall :: forall r c. Forall r c :- Forall r Unconstrained1 Source #

Allow any Forall over a row-type, be usable for Unconstrained1.

uniqueMap :: forall f ρ. AllUniqueLabels ρ :- AllUniqueLabels (Map f ρ) Source #

Map preserves uniqueness of labels.

class IsA c f a where Source #

A class to capture the idea of As so that it can be partially applied in a context.

Minimal complete definition

as

Methods

as :: As c f a Source #

Instances

c a => IsA k2 k1 c f (f a) Source #
Methods as :: As c f (f a) f a Source #

data As c f a where Source #

This data type is used to for its ability to existentially bind a type variable. Particularly, it says that for the type a, there exists a t such that 'a ~ f t' and 'c t' holds.

Constructors

As :: forall c f a t. (a ~ f t, c t) => As c f a

type FoldStep ℓ τ ρ = Inject (ℓ :-> τ) ρ ≈ ((ℓ :-> τ) ': ρ) Source #

Proof that the given label is a valid candidate for the next step in a metamorph fold, i.e. it's not in the list yet and, when sorted, will be placed at the head.

(KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ, Forall (R * ρ) c) => Forall (R * ((:) (LT ) ((:->) ℓ τ) ρ)) c Source #
Methods metamorph :: Proxy (* -> ) h -> (f (Empty ) -> g (Empty )) -> (forall (a :: Symbol) b (d :: [LT ]). (KnownSymbol a, c b) => Label a -> f (R * ((LT * ': (* :-> a) b) d)) -> (h b, f (R * d))) -> (forall (a :: Symbol) b (d :: [LT ]). (KnownSymbol a, c b, FoldStep a b d) => Label a -> h b -> g (R d) -> g (R * ((LT * ': (* :-> a) b) d))) -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ)) Source # metamorph' :: Proxy (* -> ) h -> (f (Empty ) -> g (Empty )) -> (forall (a :: Symbol) b (d :: [LT ]). (KnownSymbol a, c b) => Label a -> f (R * ((LT * ': (* :-> a) b) d)) -> Either (h b) (f (R * d))) -> (forall (a :: Symbol) b (d :: [LT ]). (KnownSymbol a, c b, FoldStep a b d) => Label a -> Either (h b) (g (R d)) -> g (R * ((LT * ': (* :-> a) b) d))) -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ)) Source #
Forall (R * ([] (LT *))) c Source #
Methods metamorph :: Proxy (* -> ) h -> (f (Empty ) -> g (Empty )) -> (forall (ℓ :: Symbol) τ (ρ :: [LT ]). (KnownSymbol ℓ, c τ) => Label ℓ -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> (h τ, f (R * ρ))) -> (forall (ℓ :: Symbol) τ (ρ :: [LT ]). (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> h τ -> g (R ρ) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ))) -> f (R * [LT ]) -> g (R [LT ]) Source # metamorph' :: Proxy ( -> ) h -> (f (Empty ) -> g (Empty )) -> (forall (ℓ :: Symbol) τ (ρ :: [LT ]). (KnownSymbol ℓ, c τ) => Label ℓ -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> Either (h τ) (f (R * ρ))) -> (forall (ℓ :: Symbol) τ (ρ :: [LT ]). (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> Either (h τ) (g (R ρ)) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ))) -> f (R * [LT ]) -> g (R [LT *]) Source #
(KnownSymbol ℓ, c τ1, c τ2, Forall2 (R * ρ1) (R * ρ2) c) => Forall2 (R * ((:) (LT ) ((:->) ℓ τ1) ρ1)) (R * ((:) (LT ) ((:->) ℓ τ2) ρ2)) c Source #
Methods metamorph2 :: Proxy (* -> ) f' -> Proxy ( -> ) g' -> (f (Empty ) -> g (Empty ) -> h (Empty ) (Empty )) -> (forall (a :: Symbol) τ10 τ20 (ρ10 :: [LT ]) (ρ20 :: [LT ]). (KnownSymbol a, c τ10, c τ20) => Label a -> f (R ((LT * ': (* :-> a) τ10) ρ10)) -> g (R * ((LT * ': (* :-> a) τ20) ρ20)) -> ((f' τ10, f (R * ρ10)), (g' τ20, g (R * ρ20)))) -> (forall (a :: Symbol) τ10 τ20 (ρ10 :: [LT ]) (ρ20 :: [LT ]). (KnownSymbol a, c τ10, c τ20) => Label a -> f' τ10 -> g' τ20 -> h (R * ρ10) (R * ρ20) -> h (R * ((LT * ': (* :-> a) τ10) ρ10)) (R * ((LT * ': (* :-> a) τ20) ρ20))) -> f (R * ((LT * ': (* :-> ℓ) τ1) ρ1)) -> g (R * ((LT * ': (* :-> ℓ) τ2) ρ2)) -> h (R * ((LT * ': (* :-> ℓ) τ1) ρ1)) (R * ((LT * ': (* :-> ℓ) τ2) ρ2)) Source #
Forall2 (R * ([] (LT ))) (R ([] (LT *))) c Source #
Methods metamorph2 :: Proxy (* -> ) f' -> Proxy ( -> ) g' -> (f (Empty ) -> g (Empty ) -> h (Empty ) (Empty )) -> (forall (ℓ :: Symbol) τ1 τ2 (ρ1 :: [LT ]) (ρ2 :: [LT ]). (KnownSymbol ℓ, c τ1, c τ2) => Label ℓ -> f (R ((LT * ': (* :-> ℓ) τ1) ρ1)) -> g (R * ((LT * ': (* :-> ℓ) τ2) ρ2)) -> ((f' τ1, f (R * ρ1)), (g' τ2, g (R * ρ2)))) -> (forall (ℓ :: Symbol) τ1 τ2 (ρ1 :: [LT ]) (ρ2 :: [LT ]). (KnownSymbol ℓ, c τ1, c τ2) => Label ℓ -> f' τ1 -> g' τ2 -> h (R * ρ1) (R * ρ2) -> h (R * ((LT * ': (* :-> ℓ) τ1) ρ1)) (R * ((LT * ': (* :-> ℓ) τ2) ρ2))) -> f (R * [LT ]) -> g (R [LT ]) -> h (R [LT ]) (R [LT *]) Source #
(KnownSymbol l, Switch (R * v) (R * r) b) => Switch (R * ((:) (LT ) ((:->) l a) v)) (R * ((:) (LT ) ((:->) l (a -> b)) r)) b Source #
Methods switch :: Var (R * ((LT * ': (* :-> l) a) v)) -> Rec (R * ((LT * ': (* :-> l) (a -> b)) r)) -> b Source # caseon :: Rec (R * ((LT * ': (* :-> l) (a -> b)) r)) -> Var (R * ((LT * ': (* :-> l) a) v)) -> b Source #
Switch (R * ([] (LT ))) (R ([] (LT *))) x Source #
Methods switch :: Var (R * [LT ]) -> Rec (R [LT ]) -> x Source # caseon :: Rec (R [LT ]) -> Var (R [LT *]) -> x Source #

(KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ, Forall (R * ρ) c) => Forall (R * ((:) (LT ) ((:->) ℓ τ) ρ)) c Source #
Methods metamorph :: Proxy (* -> ) h -> (f (Empty ) -> g (Empty )) -> (forall (a :: Symbol) b (d :: [LT ]). (KnownSymbol a, c b) => Label a -> f (R * ((LT * ': (* :-> a) b) d)) -> (h b, f (R * d))) -> (forall (a :: Symbol) b (d :: [LT ]). (KnownSymbol a, c b, FoldStep a b d) => Label a -> h b -> g (R d) -> g (R * ((LT * ': (* :-> a) b) d))) -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ)) Source # metamorph' :: Proxy (* -> ) h -> (f (Empty ) -> g (Empty )) -> (forall (a :: Symbol) b (d :: [LT ]). (KnownSymbol a, c b) => Label a -> f (R * ((LT * ': (* :-> a) b) d)) -> Either (h b) (f (R * d))) -> (forall (a :: Symbol) b (d :: [LT ]). (KnownSymbol a, c b, FoldStep a b d) => Label a -> Either (h b) (g (R d)) -> g (R * ((LT * ': (* :-> a) b) d))) -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ)) Source #
Forall (R * ([] (LT *))) c Source #
Methods metamorph :: Proxy (* -> ) h -> (f (Empty ) -> g (Empty )) -> (forall (ℓ :: Symbol) τ (ρ :: [LT ]). (KnownSymbol ℓ, c τ) => Label ℓ -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> (h τ, f (R * ρ))) -> (forall (ℓ :: Symbol) τ (ρ :: [LT ]). (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> h τ -> g (R ρ) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ))) -> f (R * [LT ]) -> g (R [LT ]) Source # metamorph' :: Proxy ( -> ) h -> (f (Empty ) -> g (Empty )) -> (forall (ℓ :: Symbol) τ (ρ :: [LT ]). (KnownSymbol ℓ, c τ) => Label ℓ -> f (R * ((LT * ': (* :-> ℓ) τ) ρ)) -> Either (h τ) (f (R * ρ))) -> (forall (ℓ :: Symbol) τ (ρ :: [LT ]). (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> Either (h τ) (g (R ρ)) -> g (R * ((LT * ': (* :-> ℓ) τ) ρ))) -> f (R * [LT ]) -> g (R [LT *]) Source #

(KnownSymbol ℓ, c τ1, c τ2, Forall2 (R * ρ1) (R * ρ2) c) => Forall2 (R * ((:) (LT ) ((:->) ℓ τ1) ρ1)) (R * ((:) (LT ) ((:->) ℓ τ2) ρ2)) c Source #
Methods metamorph2 :: Proxy (* -> ) f' -> Proxy ( -> ) g' -> (f (Empty ) -> g (Empty ) -> h (Empty ) (Empty )) -> (forall (a :: Symbol) τ10 τ20 (ρ10 :: [LT ]) (ρ20 :: [LT ]). (KnownSymbol a, c τ10, c τ20) => Label a -> f (R ((LT * ': (* :-> a) τ10) ρ10)) -> g (R * ((LT * ': (* :-> a) τ20) ρ20)) -> ((f' τ10, f (R * ρ10)), (g' τ20, g (R * ρ20)))) -> (forall (a :: Symbol) τ10 τ20 (ρ10 :: [LT ]) (ρ20 :: [LT ]). (KnownSymbol a, c τ10, c τ20) => Label a -> f' τ10 -> g' τ20 -> h (R * ρ10) (R * ρ20) -> h (R * ((LT * ': (* :-> a) τ10) ρ10)) (R * ((LT * ': (* :-> a) τ20) ρ20))) -> f (R * ((LT * ': (* :-> ℓ) τ1) ρ1)) -> g (R * ((LT * ': (* :-> ℓ) τ2) ρ2)) -> h (R * ((LT * ': (* :-> ℓ) τ1) ρ1)) (R * ((LT * ': (* :-> ℓ) τ2) ρ2)) Source #
Forall2 (R * ([] (LT ))) (R ([] (LT *))) c Source #
Methods metamorph2 :: Proxy (* -> ) f' -> Proxy ( -> ) g' -> (f (Empty ) -> g (Empty ) -> h (Empty ) (Empty )) -> (forall (ℓ :: Symbol) τ1 τ2 (ρ1 :: [LT ]) (ρ2 :: [LT ]). (KnownSymbol ℓ, c τ1, c τ2) => Label ℓ -> f (R ((LT * ': (* :-> ℓ) τ1) ρ1)) -> g (R * ((LT * ': (* :-> ℓ) τ2) ρ2)) -> ((f' τ1, f (R * ρ1)), (g' τ2, g (R * ρ2)))) -> (forall (ℓ :: Symbol) τ1 τ2 (ρ1 :: [LT ]) (ρ2 :: [LT ]). (KnownSymbol ℓ, c τ1, c τ2) => Label ℓ -> f' τ1 -> g' τ2 -> h (R * ρ1) (R * ρ2) -> h (R * ((LT * ': (* :-> ℓ) τ1) ρ1)) (R * ((LT * ': (* :-> ℓ) τ2) ρ2))) -> f (R * [LT ]) -> g (R [LT ]) -> h (R [LT ]) (R [LT *]) Source #