list-witnesses-0.1.3.2: Witnesses for working with type-level lists

Copyright(c) Justin Le 2018
LicenseBSD3
Maintainerjustin@jle.im
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Type.List.Edit

Contents

Description

Witnesses regarding single-item edits of lists.

Synopsis

Simple edits

data Insert :: [k] -> [k] -> k -> Type where Source #

An Insert as bs x is a witness that you can insert x into some position in list as to produce list bs. It is essentially Delete flipped.

Some examples:

InsZ                   :: Insert '[1,2,3] '[4,1,2,3] 4
InsS InsZ              :: Insert '[1,2,3] '[1,4,2,3] 4
InsS (InsS InsZ)       :: Insert '[1,2,3] '[1,2,4,3] 4
InsS (InsS (InsS InsZ) :: Insert '[1,2,3] '[1,2,3,4] 4

bs will always be exactly one item longer than as.

Constructors

InsZ :: Insert as (x ': as) x 
InsS :: Insert as bs x -> Insert (a ': as) (a ': bs) x 
Instances
(SDecide k, SingI as, SingI bs) => Decidable (IsInsert as bs :: TyFun k Type -> Type) Source # 
Instance details

Defined in Data.Type.List.Edit

Methods

decide :: Decide (IsInsert as bs) #

Auto (IsInsert as bs) x => Auto (IsInsert (a ': as) (a ': bs) :: TyFun k Type -> Type) (x :: k) Source # 
Instance details

Defined in Data.Type.List.Edit

Methods

auto :: IsInsert (a ': as) (a ': bs) @@ x #

Auto (IsInsert as (x ': as) :: TyFun k Type -> Type) (x :: k) Source #

Prefers the "earlier" insert if there is ambiguity

Instance details

Defined in Data.Type.List.Edit

Methods

auto :: IsInsert as (x ': as) @@ x #

(SDecide k, SingI as) => Decidable (Found (InsertedInto as) :: TyFun [k] Type -> Type) Source # 
Instance details

Defined in Data.Type.List.Edit

Methods

decide :: Decide (Found (InsertedInto as)) #

Show (Insert as bs x) Source # 
Instance details

Defined in Data.Type.List.Edit

Methods

showsPrec :: Int -> Insert as bs x -> ShowS #

show :: Insert as bs x -> String #

showList :: [Insert as bs x] -> ShowS #

type Apply (InsertIndexSym0 as bs x y :: TyFun (Insert as bs x) (Index as y ~> Index bs y) -> Type) (ins :: Insert as bs x) Source # 
Instance details

Defined in Data.Type.List.Edit

type Apply (InsertIndexSym0 as bs x y :: TyFun (Insert as bs x) (Index as y ~> Index bs y) -> Type) (ins :: Insert as bs x) = InsertIndexSym as bs x y ins

autoInsert :: forall as bs x. Auto (IsInsert as bs) x => Insert as bs x Source #

Automatically generate an Insert if as, bs and x are known statically.

Prefers the earlier insertion if there is an ambiguity.

InsS InsZ        :: Insert '[1,2] '[1,2,2] 2
InsS (InsS InsZ) :: Insert '[1,2] '[1,2,2] 2
autoInsert '[1,2] '[1,2,2] @2 == InsS InsZ

Since: 0.1.2.0

data Delete :: [k] -> [k] -> k -> Type where Source #

A Delete as bs x is a witness that you can delete item x from as to produce the list bs. It is essentially Insert flipped.

Some examples:

DelZ             :: Delete '[1,2,3] '[2,3] 1
DelS DelZ        :: Delete '[1,2,3] '[2,3] 2
DelS (DelS DelZ) :: Delete '[1,2,3] '[1,2] 3

bs will always be exactly one item shorter than as.

Constructors

DelZ :: Delete (x ': as) as x 
DelS :: Delete as bs x -> Delete (a ': as) (a ': bs) x 
Instances
(SDecide k, SingI as, SingI bs) => Decidable (IsDelete as bs :: TyFun k Type -> Type) Source # 
Instance details

Defined in Data.Type.List.Edit

Methods

decide :: Decide (IsDelete as bs) #

Auto (IsDelete as bs) x => Auto (IsDelete (a ': as) (a ': bs) :: TyFun k Type -> Type) (x :: k) Source # 
Instance details

Defined in Data.Type.List.Edit

Methods

auto :: IsDelete (a ': as) (a ': bs) @@ x #

Auto (IsDelete (x ': as) as :: TyFun k Type -> Type) (x :: k) Source #

Prefers the "earlier" delete if there is ambiguity

Instance details

Defined in Data.Type.List.Edit

Methods

auto :: IsDelete (x ': as) as @@ x #

(SDecide k, SingI as) => Decidable (Found (DeletedFrom as) :: TyFun [k] Type -> Type) Source # 
Instance details

Defined in Data.Type.List.Edit

Methods

decide :: Decide (Found (DeletedFrom as)) #

Show (Delete as bs x) Source # 
Instance details

Defined in Data.Type.List.Edit

Methods

showsPrec :: Int -> Delete as bs x -> ShowS #

show :: Delete as bs x -> String #

showList :: [Delete as bs x] -> ShowS #

type Apply (DeleteIndexSym0 as bs x y :: TyFun (Delete as bs x) (Index as y ~> DeletedIx bs x y) -> Type) (del :: Delete as bs x) Source # 
Instance details

Defined in Data.Type.List.Edit

type Apply (DeleteIndexSym0 as bs x y :: TyFun (Delete as bs x) (Index as y ~> DeletedIx bs x y) -> Type) (del :: Delete as bs x) = DeleteIndexSym as bs x y del

autoDelete :: forall as bs x. Auto (IsDelete as bs) x => Delete as bs x Source #

Automatically generate an Delete if as, bs and x are known statically.

Prefers the earlier deletion if there is an ambiguity.

DelS DelZ        :: Delete '[1,2,2] '[1,2] 2
DelS (DelS DelZ) :: Delete '[1,2,2] '[1,2] 2
autoDelete '[1,2,2] '[1,2] @2 == DelS DelZ

Since: 0.1.2.0

insToDel :: Insert as bs x -> Delete bs as x Source #

Flip an insertion.

delToIns :: Delete as bs x -> Insert bs as x Source #

Flip a deletion.

data Substitute :: [k] -> [k] -> k -> k -> Type where Source #

A Substitute as bs x y is a witness that you can replace item x in as with item y to produce bs.

Some examples:

SubZ             :: Substitute '[1,2,3] '[4,2,3] 1 4
SubS SubZ        :: Substitute '[1,2,3] '[1,4,3] 2 4
SubS (SubS SubZ) :: Substitute '[1,2,3] '[1,2,4] 3 4

Constructors

SubZ :: Substitute (x ': as) (y ': as) x y 
SubS :: Substitute as bs x y -> Substitute (c ': as) (c ': bs) x y 
Instances
Auto (IsSubstitute (x ': as) (x ': as) x :: TyFun k Type -> Type) (x :: k) Source # 
Instance details

Defined in Data.Type.List.Edit

Methods

auto :: IsSubstitute (x ': as) (x ': as) x @@ x #

Auto (IsSubstitute as bs x) y => Auto (IsSubstitute (c ': as) (c ': bs) x :: TyFun k Type -> Type) (y :: k) Source #

Prefers the earlier subsitution if there is ambiguity.

Instance details

Defined in Data.Type.List.Edit

Methods

auto :: IsSubstitute (c ': as) (c ': bs) x @@ y #

Auto (IsSubstitute (x ': as) (y ': as) x :: TyFun k Type -> Type) (y :: k) Source # 
Instance details

Defined in Data.Type.List.Edit

Methods

auto :: IsSubstitute (x ': as) (y ': as) x @@ y #

Show (Substitute as bs x y) Source # 
Instance details

Defined in Data.Type.List.Edit

Methods

showsPrec :: Int -> Substitute as bs x y -> ShowS #

show :: Substitute as bs x y -> String #

showList :: [Substitute as bs x y] -> ShowS #

type Apply (SubstituteIndexSym0 as bs x y z :: TyFun (Substitute as bs x y) (Index as z ~> SubstitutedIx bs x y z) -> Type) (s :: Substitute as bs x y) Source # 
Instance details

Defined in Data.Type.List.Edit

type Apply (SubstituteIndexSym0 as bs x y z :: TyFun (Substitute as bs x y) (Index as z ~> SubstitutedIx bs x y z) -> Type) (s :: Substitute as bs x y) = SubstituteIndexSym as bs x y z s

autoSubstitute :: forall as bs x y. Auto (IsSubstitute as bs x) y => Substitute as bs x y Source #

Automatically generate an Substitute if as, bs, x, and y are known statically.

Prefers the "earlier" substitution if there is an ambiguity

SubZ      :: Substitute '[1,1] '[1,1] 1 1
SubS SubZ :: Substitute '[1,1] '[1,1] 1 1
autoSubstitute '[1,1] '[1,1] 1 1 == SubZ

Since: 0.1.2.0

flipSub :: Substitute as bs x y -> Substitute bs as y x Source #

Flip a substitution

subToDelIns :: Substitute as bs x y -> (forall cs. Delete as cs x -> Insert cs bs y -> r) -> r Source #

Decompose a Substitute into a Delete followed by an Insert.

Predicates

type IsInsert as bs = TyPred (Insert as bs) Source #

A type-level predicate that a given value can be used as an insertion to change as to bs.

Since: 0.1.2.0

type InsertedInto (as :: [k]) = (TyPP (Insert as) :: ParamPred [k] k) Source #

If bs satisfies InsertedInto as, it means that there exists some element x such that IsInsert as bs @@ x: you can get bs by inserting x into as somewhere.

In other words, InsertedInto as is satisfied by bs if you can turn as into bs by inserting one individual item.

You can find this element (if it exists) using search, or the Decidable instance of Found (InsertedInto as):

searchTC :: SingI as => Sing bs -> Decision (Σ k (IsInsert as bs))

This will find you the single element you need to insert into as to get bs, if it exists.

Since: 0.1.2.0

type IsDelete as bs = TyPred (Delete as bs) Source #

A type-level predicate that a given value can be used as a deletion to change as to bs.

Since: 0.1.2.0

type DeletedFrom (as :: [k]) = (TyPP (Delete as) :: ParamPred [k] k) Source #

If bs satisfies DeletedFrom as, it means that there exists some element x such that IsDelete as bs @@ x: you can get bs by deleting x from as somewhere.

In other words, DeletedFrom as is satisfied by bs if you can turn as into bs by deleting one individual item.

You can find this element (if it exists) using search, or the Decidable instance of Found (DeletedFrom as).

searchTC :: SingI as => Sing bs -> Decision (Σ k (IsDelete as bs))

This will find you the single element you need to delete from as to get bs, if it exists.

Since: 0.1.2.0

type IsSubstitute as bs x = TyPred (Substitute as bs x) Source #

A type-level predicate that a given value can be used as a substitution of x to change as to bs.

Since: 0.1.2.0

Singletons

data SInsert as bs x :: Insert as bs x -> Type where Source #

Kind-indexed singleton for Insert.

Constructors

SInsZ :: SInsert as (x ': as) x InsZ 
SInsS :: SInsert as bs x ins -> SInsert (a ': as) (a ': bs) x (InsS ins) 
Instances
Show (SInsert as bs x del) Source # 
Instance details

Defined in Data.Type.List.Edit

Methods

showsPrec :: Int -> SInsert as bs x del -> ShowS #

show :: SInsert as bs x del -> String #

showList :: [SInsert as bs x del] -> ShowS #

data SDelete as bs x :: Delete as bs x -> Type where Source #

Kind-indexed singleton for Delete.

Constructors

SDelZ :: SDelete (x ': as) as x DelZ 
SDelS :: SDelete as bs x del -> SDelete (a ': as) (a ': bs) x (DelS del) 
Instances
Show (SDelete as bs x del) Source # 
Instance details

Defined in Data.Type.List.Edit

Methods

showsPrec :: Int -> SDelete as bs x del -> ShowS #

show :: SDelete as bs x del -> String #

showList :: [SDelete as bs x del] -> ShowS #

data SSubstitute as bs x y :: Substitute as bs x y -> Type where Source #

Kind-indexed singleton for Substitute.

Constructors

SSubZ :: SSubstitute (x ': as) (y ': as) x y SubZ 
SSubS :: SSubstitute as bs x y sub -> SSubstitute (c ': as) (c ': bs) x y (SubS sub) 

Compound edits

data Edit :: [k] -> [k] -> Type where Source #

An Edit as bs is a reversible edit script transforming as into bs through successive insertions, deletions, and substitutions.

TODO: implement Wagner-Fischer or something similar to minimize find a minimal edit distance

Constructors

ENil :: Edit as as 
EIns :: Insert bs cs x -> Edit as bs -> Edit as cs 
EDel :: Delete bs cs x -> Edit as bs -> Edit as cs 
ESub :: Substitute bs cs x y -> Edit as bs -> Edit as cs 
Instances
Category (Edit :: [k] -> [k] -> Type) Source #

Edit composition

Instance details

Defined in Data.Type.List.Edit

Methods

id :: Edit a a #

(.) :: Edit b c -> Edit a b -> Edit a c #

Show (Edit as bs) Source # 
Instance details

Defined in Data.Type.List.Edit

Methods

showsPrec :: Int -> Edit as bs -> ShowS #

show :: Edit as bs -> String #

showList :: [Edit as bs] -> ShowS #

compEdit :: Edit as bs -> Edit bs cs -> Edit as cs Source #

Compose two Edits

flipEdit :: Edit as bs -> Edit bs as Source #

Reverse an Edit script. O(n^2). Please do not use ever in any circumstance.

TODO: Make O(n) using diff lists.

Rec

insertRec :: Insert as bs x -> f x -> Rec f as -> Rec f bs Source #

Insert a value into a Rec, at a position indicated by the Insert.

deleteRec :: Delete as bs x -> Rec f as -> Rec f bs Source #

Delete a value in a Rec, at a position indicated by the Delete.

deleteGetRec :: Delete as bs x -> Rec f as -> (f x, Rec f bs) Source #

Retrieve and delete a value in a Rec, at a position indicated by the Delete.

recLens :: forall as bs x y f. Substitute as bs x y -> Lens (Rec f as) (Rec f bs) (f x) (f y) Source #

A type-changing lens into a value in a Rec, given a Substitute indicating which value.

For example:

recLens (SubS SubZ)
     :: Lens (Rec f '[a,b,c,d]) (Rec f '[a,e,c,d])
             (f b)              (f e)

The number of SubS in the index essentially indicates the index to edit at.

This is similar to rlensC from vinyl, but is built explicitly and inductively, instead of using typeclass magic.

substituteRec :: Substitute as bs x y -> (f x -> f y) -> Rec f as -> Rec f bs Source #

Substitute a value in a Rec at a given position, indicated by the Substitute. This is essentially a specialized version of recLens.

Index

Manipulating indices

insertIndex :: Insert as bs x -> Index as y -> Index bs y Source #

If you add an item to as to create bs, you also need to shift an Index as y to Index bs y. This shifts the Index in as to become an Index in bs, but makes sure that the index points to the same original value.

data DeletedIx :: [k] -> k -> k -> Type where Source #

Used as the return type of deleteIndex. An DeletedIx bs x y is like a Maybe (Index bs y), except the Nothing case witnesses that x ~ y.

Constructors

GotDeleted :: DeletedIx bs x x 
NotDeleted :: Index bs y -> DeletedIx bs x y 
Instances
Show (DeletedIx bs x y) Source # 
Instance details

Defined in Data.Type.List.Edit

Methods

showsPrec :: Int -> DeletedIx bs x y -> ShowS #

show :: DeletedIx bs x y -> String #

showList :: [DeletedIx bs x y] -> ShowS #

type Apply (DeleteIndexSym0 as bs x y :: TyFun (Delete as bs x) (Index as y ~> DeletedIx bs x y) -> Type) (del :: Delete as bs x) Source # 
Instance details

Defined in Data.Type.List.Edit

type Apply (DeleteIndexSym0 as bs x y :: TyFun (Delete as bs x) (Index as y ~> DeletedIx bs x y) -> Type) (del :: Delete as bs x) = DeleteIndexSym as bs x y del
type Apply (DeleteIndexSym as bs x y del :: TyFun (Index as y) (DeletedIx bs x y) -> Type) (i :: Index as y) Source # 
Instance details

Defined in Data.Type.List.Edit

type Apply (DeleteIndexSym as bs x y del :: TyFun (Index as y) (DeletedIx bs x y) -> Type) (i :: Index as y) = DeleteIndex as bs x y del i

deleteIndex :: Delete as bs x -> Index as y -> DeletedIx bs x y Source #

If you delete an item in as to create bs, you also need to move Index as y into Index bs y. This transforms the Index in as to become an Index in bs, making sure the index points to the same original value.

However, there is a possibility that the deleted item is the item that the index was originally pointing to. If this is the case, this function returns GotDeleted, a witness that x ~ y. Otherwise, it returns NotDeleted with the unshifted index.

deleteIndex_ :: Delete as bs x -> Index as y -> Maybe (Index bs y) Source #

A version of deleteIndex returning a simple Maybe. This can be used if you don't care about witnessing that x ~ y in the case that the index is the item that is deleted.

data SubstitutedIx :: [k] -> k -> k -> k -> Type where Source #

Used as the return type of substituteIndex. An SubstitutedIx bs x y z is like an Either (Index bs y) (Index bs z), except the Left case witnesses that x ~ z.

Constructors

GotSubbed :: Index bs y -> SubstitutedIx bs z y z 
NotSubbed :: Index bs z -> SubstitutedIx bs x y z 
Instances
type Apply (SubstituteIndexSym0 as bs x y z :: TyFun (Substitute as bs x y) (Index as z ~> SubstitutedIx bs x y z) -> Type) (s :: Substitute as bs x y) Source # 
Instance details

Defined in Data.Type.List.Edit

type Apply (SubstituteIndexSym0 as bs x y z :: TyFun (Substitute as bs x y) (Index as z ~> SubstitutedIx bs x y z) -> Type) (s :: Substitute as bs x y) = SubstituteIndexSym as bs x y z s
type Apply (SubstituteIndexSym as bs x y z s :: TyFun (Index as z) (SubstitutedIx bs x y z) -> Type) (i :: Index as z) Source # 
Instance details

Defined in Data.Type.List.Edit

type Apply (SubstituteIndexSym as bs x y z s :: TyFun (Index as z) (SubstitutedIx bs x y z) -> Type) (i :: Index as z) = SubstituteIndex as bs x y z s i

substituteIndex :: Substitute as bs x y -> Index as z -> SubstitutedIx bs x y z Source #

If you substitute an item in as to create bs, you also need to reshift Index as z into Index bs z. This reshifts the Index in as to become an Index in bs, making sure the index points to the same original value.

However, there is a possibility that the substituted item is the item that the index was originally pointing to. If this is the case, this function returns GotSubbed, a witness that x ~ z. Otherwise, it returns NotSubbed. Both contain the updated index.

substituteIndex_ :: Substitute as bs x y -> Index as z -> Either (Index bs y) (Index bs z) Source #

A version of substituteIndex returning a simple Either. This can be the case if you don't care about witnessing x ~ z in the case that the index is the item that was substituted.

Converting from indices

withDelete :: Index as x -> (forall bs. Delete as bs x -> r) -> r Source #

Given an Index pointing to an element, create a Delete corresponding to the given item. The type of the resulting list is existentially quantified, is guaranteed to be just exactly the original list minus the specified element.

withInsert :: Index as x -> (forall bs. Insert as bs y -> r) -> r Source #

Given an Index pointing to an element, create an Insert placing an item directly before the given element. The type is existentailly quantified.

withInsertAfter :: Index as x -> (forall bs. Insert as bs y -> r) -> r Source #

Given an Index pointing to an element, create an Insert placing an item directly after the given element. The type is existentailly quantified.

Type-Level

type family InsertIndex as bs x y (ins :: Insert as bs x) (i :: Index as y) :: Index bs y where ... Source #

Type-level version of insertIndex. Because of how GADTs and type families interact, the type-level lists and kinds of the insertion and index must be provided.

Equations

InsertIndex as (x ': as) x y InsZ i = IS i 
InsertIndex (y ': as) (y ': bs) x y (InsS ins) IZ = IZ 
InsertIndex (a ': as) (a ': bs) x y (InsS ins) (IS i) = IS (InsertIndex as bs x y ins i) 

sInsertIndex :: SInsert as bs x ins -> SIndex as y i -> SIndex bs y (InsertIndex as bs x y ins i) Source #

Singleton witness for InsertIndex.

data SDeletedIx bs x y :: DeletedIx bs x y -> Type where Source #

Kind-indexed singleton for DeletedIx.

Constructors

SGotDeleted :: SDeletedIx bs x x GotDeleted 
SNotDeleted :: SIndex bs y i -> SDeletedIx bs x y (NotDeleted i) 

type family DeleteIndex as bs x y (del :: Delete as bs x) (i :: Index as y) :: DeletedIx bs x y where ... Source #

Type-level version of deleteIndex. Because of how GADTs and type families interact, the type-level lists and kinds of the insertion and index must be provided.

Equations

DeleteIndex (x ': bs) bs x x DelZ IZ = GotDeleted 
DeleteIndex (x ': bs) bs x y DelZ (IS i) = NotDeleted i 
DeleteIndex (y ': as) (y ': bs) x y (DelS del) IZ = NotDeleted IZ 
DeleteIndex (b ': as) (b ': bs) x y (DelS del) (IS i) = SuccDeletedIx b bs x y (DeleteIndex as bs x y del i) 

sDeleteIndex :: SDelete as bs x del -> SIndex as y i -> SDeletedIx bs x y (DeleteIndex as bs x y del i) Source #

Singleton witness for DeleteIndex.

data SSubstitutedIx bs x y z :: SubstitutedIx bs x y z -> Type where Source #

Kind-indexed singleton for SubstitutedIx.

Constructors

SGotSubbed :: SIndex bs y i -> SSubstitutedIx bs z y z (GotSubbed i) 
SNotSubbed :: SIndex bs z i -> SSubstitutedIx bs x y z (NotSubbed i) 

type family SubstituteIndex as bs x y z (s :: Substitute as bs x y) (i :: Index as z) :: SubstitutedIx bs x y z where ... Source #

Type-level version of substituteIndex. Because of how GADTs and type families interact, the type-level lists and kinds of the insertion and index must be provided.

Equations

SubstituteIndex (z ': as) (y ': as) z y z SubZ IZ = GotSubbed IZ 
SubstituteIndex (x ': as) (y ': as) x y z SubZ (IS i) = NotSubbed (IS i) 
SubstituteIndex (z ': as) (z ': bs) x y z (SubS s) IZ = NotSubbed IZ 
SubstituteIndex (b ': as) (b ': bs) x y z (SubS s) (IS i) = SuccSubstitutedIx b bs x y z (SubstituteIndex as bs x y z s i) 

sSubstituteIndex :: SSubstitute as bs x y s -> SIndex as z i -> SSubstitutedIx bs x y z (SubstituteIndex as bs x y z s i) Source #

Singleton witness for SubstituteIndex.

Defunctionalization Symbols

data InsertIndexSym0 as bs x y :: Insert as bs x ~> (Index as y ~> Index bs y) Source #

Defunctionalization symbol for InsertIndex, expecting only the kind variables.

Instances
type Apply (InsertIndexSym0 as bs x y :: TyFun (Insert as bs x) (Index as y ~> Index bs y) -> Type) (ins :: Insert as bs x) Source # 
Instance details

Defined in Data.Type.List.Edit

type Apply (InsertIndexSym0 as bs x y :: TyFun (Insert as bs x) (Index as y ~> Index bs y) -> Type) (ins :: Insert as bs x) = InsertIndexSym as bs x y ins

data InsertIndexSym as bs x y :: Insert as bs x -> Index as y ~> Index bs y Source #

Defunctionalization symbol for InsertIndex, expecting the Insert along with the kind variables.

Instances
type Apply (InsertIndexSym as bs x y ins :: TyFun (Index as y) (Index bs y) -> Type) (i :: Index as y) Source # 
Instance details

Defined in Data.Type.List.Edit

type Apply (InsertIndexSym as bs x y ins :: TyFun (Index as y) (Index bs y) -> Type) (i :: Index as y) = InsertIndex as bs x y ins i

data DeleteIndexSym0 as bs x y :: Delete as bs x ~> (Index as y ~> DeletedIx bs x y) Source #

Defunctionalization symbol for DeleteIndex, expecting only the kind variables.

Instances
type Apply (DeleteIndexSym0 as bs x y :: TyFun (Delete as bs x) (Index as y ~> DeletedIx bs x y) -> Type) (del :: Delete as bs x) Source # 
Instance details

Defined in Data.Type.List.Edit

type Apply (DeleteIndexSym0 as bs x y :: TyFun (Delete as bs x) (Index as y ~> DeletedIx bs x y) -> Type) (del :: Delete as bs x) = DeleteIndexSym as bs x y del

data DeleteIndexSym as bs x y :: Delete as bs x -> Index as y ~> DeletedIx bs x y Source #

Defunctionalization symbol for DeleteIndex, expecting the Delete along with the kind variables.

Instances
type Apply (DeleteIndexSym as bs x y del :: TyFun (Index as y) (DeletedIx bs x y) -> Type) (i :: Index as y) Source # 
Instance details

Defined in Data.Type.List.Edit

type Apply (DeleteIndexSym as bs x y del :: TyFun (Index as y) (DeletedIx bs x y) -> Type) (i :: Index as y) = DeleteIndex as bs x y del i

data SubstituteIndexSym0 as bs x y z :: Substitute as bs x y ~> (Index as z ~> SubstitutedIx bs x y z) Source #

Defunctionalization symbol for SubstituteIndex, expecting only the kind variables.

Instances
type Apply (SubstituteIndexSym0 as bs x y z :: TyFun (Substitute as bs x y) (Index as z ~> SubstitutedIx bs x y z) -> Type) (s :: Substitute as bs x y) Source # 
Instance details

Defined in Data.Type.List.Edit

type Apply (SubstituteIndexSym0 as bs x y z :: TyFun (Substitute as bs x y) (Index as z ~> SubstitutedIx bs x y z) -> Type) (s :: Substitute as bs x y) = SubstituteIndexSym as bs x y z s

data SubstituteIndexSym as bs x y z :: Substitute as bs x y -> Index as z ~> SubstitutedIx bs x y z Source #

Defunctionalization symbol for SubstituteIndex, expecting the Substitute along with the kind variables.

Instances
type Apply (SubstituteIndexSym as bs x y z s :: TyFun (Index as z) (SubstitutedIx bs x y z) -> Type) (i :: Index as z) Source # 
Instance details

Defined in Data.Type.List.Edit

type Apply (SubstituteIndexSym as bs x y z s :: TyFun (Index as z) (SubstitutedIx bs x y z) -> Type) (i :: Index as z) = SubstituteIndex as bs x y z s i