Copyright | (c) Justin Le 2018 |
---|---|

License | BSD3 |

Maintainer | justin@jle.im |

Stability | experimental |

Portability | non-portable |

Safe Haskell | None |

Language | Haskell2010 |

Witnesses regarding single-item edits of lists.

## Synopsis

- data Insert :: [k] -> [k] -> k -> Type where
- autoInsert :: forall as bs x. Auto (IsInsert as bs) x => Insert as bs x
- data Delete :: [k] -> [k] -> k -> Type where
- autoDelete :: forall as bs x. Auto (IsDelete as bs) x => Delete as bs x
- insToDel :: Insert as bs x -> Delete bs as x
- delToIns :: Delete as bs x -> Insert bs as x
- data Substitute :: [k] -> [k] -> k -> k -> Type where
- SubZ :: Substitute (x ': as) (y ': as) x y
- SubS :: Substitute as bs x y -> Substitute (c ': as) (c ': bs) x y

- autoSubstitute :: forall as bs x y. Auto (IsSubstitute as bs x) y => Substitute as bs x y
- flipSub :: Substitute as bs x y -> Substitute bs as y x
- subToDelIns :: Substitute as bs x y -> (forall cs. Delete as cs x -> Insert cs bs y -> r) -> r
- type IsInsert as bs = TyPred (Insert as bs)
- type InsertedInto (as :: [k]) = (TyPP (Insert as) :: ParamPred [k] k)
- type IsDelete as bs = TyPred (Delete as bs)
- type DeletedFrom (as :: [k]) = (TyPP (Delete as) :: ParamPred [k] k)
- type IsSubstitute as bs x = TyPred (Substitute as bs x)
- data SInsert as bs x :: Insert as bs x -> Type where
- data SDelete as bs x :: Delete as bs x -> Type where
- data SSubstitute as bs x y :: Substitute as bs x y -> Type where
- 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)

- data Edit :: [k] -> [k] -> Type where
- compEdit :: Edit as bs -> Edit bs cs -> Edit as cs
- flipEdit :: Edit as bs -> Edit bs as
- insertRec :: Insert as bs x -> f x -> Rec f as -> Rec f bs
- deleteRec :: Delete as bs x -> Rec f as -> Rec f bs
- deleteGetRec :: Delete as bs x -> Rec f as -> (f x, Rec f bs)
- recLens :: forall as bs x y f. Substitute as bs x y -> Lens (Rec f as) (Rec f bs) (f x) (f y)
- substituteRec :: Substitute as bs x y -> (f x -> f y) -> Rec f as -> Rec f bs
- insertIndex :: Insert as bs x -> Index as y -> Index bs y
- data DeletedIx :: [k] -> k -> k -> Type where
- GotDeleted :: DeletedIx bs x x
- NotDeleted :: Index bs y -> DeletedIx bs x y

- deleteIndex :: Delete as bs x -> Index as y -> DeletedIx bs x y
- deleteIndex_ :: Delete as bs x -> Index as y -> Maybe (Index bs y)
- data SubstitutedIx :: [k] -> k -> k -> k -> Type where
- GotSubbed :: Index bs y -> SubstitutedIx bs z y z
- NotSubbed :: Index bs z -> SubstitutedIx bs x y z

- substituteIndex :: Substitute as bs x y -> Index as z -> SubstitutedIx bs x y z
- substituteIndex_ :: Substitute as bs x y -> Index as z -> Either (Index bs y) (Index bs z)
- withDelete :: Index as x -> (forall bs. Delete as bs x -> r) -> r
- withInsert :: Index as x -> (forall bs. Insert as bs y -> r) -> r
- withInsertAfter :: Index as x -> (forall bs. Insert as bs y -> r) -> r
- type family InsertIndex as bs x y (ins :: Insert as bs x) (i :: Index as y) :: Index bs y where ...
- sInsertIndex :: SInsert as bs x ins -> SIndex as y i -> SIndex bs y (InsertIndex as bs x y ins i)
- data SDeletedIx bs x y :: DeletedIx bs x y -> Type where
- 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 ...
- sDeleteIndex :: SDelete as bs x del -> SIndex as y i -> SDeletedIx bs x y (DeleteIndex as bs x y del i)
- data SSubstitutedIx bs x y z :: SubstitutedIx bs x y z -> Type where
- 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 ...
- sSubstituteIndex :: SSubstitute as bs x y s -> SIndex as z i -> SSubstitutedIx bs x y z (SubstituteIndex as bs x y z s i)
- data InsertIndexSym0 as bs x y :: Insert as bs x ~> (Index as y ~> Index bs y)
- data InsertIndexSym as bs x y :: Insert as bs x -> Index as y ~> Index bs y
- data DeleteIndexSym0 as bs x y :: Delete as bs x ~> (Index as y ~> DeletedIx bs x y)
- data DeleteIndexSym as bs x y :: Delete as bs x -> Index as y ~> DeletedIx bs x y
- data SubstituteIndexSym0 as bs x y z :: Substitute as bs x y ~> (Index as z ~> SubstitutedIx bs x y z)
- data SubstituteIndexSym as bs x y z :: Substitute as bs x y -> Index as z ~> SubstitutedIx bs x y z

# Simple edits

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

An

is a witness that you can insert `Insert`

as bs x`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`

.

## Instances

(SDecide k, SingI as, SingI bs) => Decidable (IsInsert as bs :: TyFun k Type -> Type) Source # | |

Defined in Data.Type.List.Edit | |

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

Defined in Data.Type.List.Edit | |

Auto (IsInsert as (x ': as) :: TyFun k Type -> Type) (x :: k) Source # | Prefers the "earlier" insert if there is ambiguity |

Defined in Data.Type.List.Edit | |

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

Defined in Data.Type.List.Edit decide :: Decide (Found (InsertedInto as)) # | |

Show (Insert as bs x) Source # | |

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

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

is a witness that you can delete item `Delete`

as bs x`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`

.

## Instances

(SDecide k, SingI as, SingI bs) => Decidable (IsDelete as bs :: TyFun k Type -> Type) Source # | |

Defined in Data.Type.List.Edit | |

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

Defined in Data.Type.List.Edit | |

Auto (IsDelete (x ': as) as :: TyFun k Type -> Type) (x :: k) Source # | Prefers the "earlier" delete if there is ambiguity |

Defined in Data.Type.List.Edit | |

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

Defined in Data.Type.List.Edit decide :: Decide (Found (DeletedFrom as)) # | |

Show (Delete as bs x) Source # | |

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

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*

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

A

is a witness that you can replace item `Substitute`

as bs x y`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

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

Defined in Data.Type.List.Edit 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. |

Defined in Data.Type.List.Edit auto :: IsSubstitute (c ': as) (c ': bs) x @@ y # | |

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

Defined in Data.Type.List.Edit auto :: IsSubstitute (x ': as) (y ': as) x @@ y # | |

Show (Substitute as bs x y) Source # | |

Defined in Data.Type.List.Edit 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 # | |

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

, it means that there exists some
element `InsertedInto`

as`x`

such that

: you can get `IsInsert`

as bs @@ x`bs`

by
inserting `x`

into `as`

somewhere.

In other words,

is satisfied by `InsertedInto`

as`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

, it means that there exists some
element `DeletedFrom`

as`x`

such that

: you can get `IsDelete`

as bs @@ x`bs`

by
deleting `x`

from `as`

somewhere.

In other words,

is satisfied by `DeletedFrom`

as`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`

.

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

Kind-indexed singleton for `Delete`

.

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

Kind-indexed singleton for `Substitute`

.

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

is a reversible edit script transforming `Edit`

as bs`as`

into
`bs`

through successive insertions, deletions, and substitutions.

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

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 |

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

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

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

Used as the return type of `deleteIndex`

. An

is
like a `DeletedIx`

bs x y

, except the `Maybe`

(`Index`

bs y)`Nothing`

case witnesses
that `x ~ y`

.

GotDeleted :: DeletedIx bs x x | |

NotDeleted :: Index bs y -> DeletedIx bs x y |

## Instances

Show (DeletedIx bs x y) Source # | |

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

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

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

into `Index`

as y`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

is
like an `SubstitutedIx`

bs x y z

, except the `Either`

(`Index`

bs y) (`Index`

bs z)`Left`

case
witnesses that `x ~ z`

.

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

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

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

into `Index`

as z

. This reshifts the `Index`

bs z`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 #

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

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

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

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`

.

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.

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`

.

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.

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

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

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

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

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

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

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 |