Data.Type.List.Edit

Witnesses regarding single-item edits of lists.

Simple edits

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

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

Show (Insert as bs x)

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)

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 Delete :: [k] -> [k] -> k -> Type where

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

Show (Delete as bs x)

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)

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

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

Flip an insertion.

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

Flip a deletion.

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

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

Show (Substitute as bs x y)

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)

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

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

Flip a substitution

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

Decompose a Substitute into a Delete followed by an Insert.

Singletons

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

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)

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

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)

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

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

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

TODO: implement Wagner-Fischer 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)

Edit composition

Defined in Data.Type.List.Edit

Methods

id :: Edit a a

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

Show (Edit as bs)

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

Compose two Edits

flipEdit :: Edit as bs -> Edit bs as

Reverse an Edit script. O(n^2). Please do not use.

TODO: Make O(n) using diff lists.

Rec

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

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

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

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)

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

recLens :: forall as bs x y g f. Functor f => Substitute as bs x y -> (g x -> f (g y)) -> Rec g as -> f (Rec g bs)

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

Read this type signature as:

recLens
    :: Substitute as bs x y
    -> Lens (Rec f as) (Rec f bs) (f x) (f y)

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

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

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

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)

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)

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)

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

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)

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

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)

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)

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

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)

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

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

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

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

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)

Singleton witness for InsertIndex.

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

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

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)

Singleton witness for DeleteIndex.

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

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

Type-level version of subsituteIndex. 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)

Singleton witness for SubstituteIndex.

Defunctionalization Symbols

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

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)

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

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)

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)

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)

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

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)

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)

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)

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

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)

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