Generics.MRSOP.STDiff.Types

Functorial Changes

Represents changes on the first layer of two values of mutually recursive families. For a more in-depth explanation of the datatypes and their meaning we refer the interested reader to the relevant literature:

• Miraldo, Dagand and Swierstra, TyDe 2017 pdf
• van Putten, MSc thesis https://dspace.library.uu.nl/handle/1874/380853

data TrivialK (ki :: kon -> *) :: kon -> * where

Represents a change between two opaque values. When they are equal represents a copy.

Constructors

Trivial :: ki kon -> ki kon -> TrivialK ki kon

data At (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Atom kon -> * where

Represents a change between two atoms, where an atom is either a recursive or an opaque value.

Constructors

AtSet :: TrivialK ki kon -> At ki codes (K kon)

AtFix :: IsNat ix => Almu ki codes ix ix -> At ki codes (I ix)

data Al (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: [Atom kon] -> [Atom kon] -> * where

Represents an alignment between two product of atoms.

Constructors

A0 :: Al ki codes '[] '[]

AX :: At ki codes x -> Al ki codes xs ys -> Al ki codes (x ': xs) (x ': ys)

ADel :: NA ki (Fix ki codes) x -> Al ki codes xs ys -> Al ki codes (x ': xs) ys

AIns :: NA ki (Fix ki codes) x -> Al ki codes xs ys -> Al ki codes xs (x ': ys)

data Spine (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: [[Atom kon]] -> [[Atom kon]] -> * where

Represents a change at the coproduct structure.

Constructors

Scp :: Spine ki codes s1 s1

SCns :: Constr s1 c1 -> NP (At ki codes) (Lkup c1 s1) -> Spine ki codes s1 s1

SChg :: Constr s1 c1 -> Constr s2 c2 -> Al ki codes (Lkup c1 s1) (Lkup c2 s2) -> Spine ki codes s1 s2

Fixpoint Changes

The next datatypes represent a sequence of Spine, Al and At assembled coupled with operators to describe changes in the recursive structure such as inserting and deleting constructors.

data Ctx (ki :: kon -> *) (codes :: [[[Atom kon]]]) (p :: Nat -> Nat -> *) (ix :: Nat) :: [Atom kon] -> * where

Represents a one-hole context over a NP (NA ki (fix ki codes)) xs where the hole is in a distinguished element indexed by 'I ix and is filled with applying p to the relevant indexes.

Constructors

H :: IsNat iy => p ix iy -> PoA ki (Fix ki codes) xs -> Ctx ki codes p ix (I iy ': xs)

T :: NA ki (Fix ki codes) a -> Ctx ki codes p ix xs -> Ctx ki codes p ix (a ': xs)

type InsCtx ki codes ix xs = Ctx ki codes (Almu ki codes) ix xs

Simple synonym for contexts.

type DelCtx ki codes ix xs = Ctx ki codes (AlmuMin ki codes) ix xs

A deletion context needs to swap the indexes in the hole, hence we use a newtype for that.

newtype AlmuMin ki codes ix iy

The newtype used to swap the indexes to |Almu|.

Constructors

AlmuMin

Fields

• unAlmuMin :: Almu ki codes iy ix

data Almu (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Nat -> Nat -> * where

Represent recursive spines.

Constructors

Spn :: Spine ki codes (Lkup ix codes) (Lkup iy codes) -> Almu ki codes ix iy

Ins :: Constr (Lkup iy codes) c -> InsCtx ki codes ix (Lkup c (Lkup iy codes)) -> Almu ki codes ix iy

Del :: IsNat iy => Constr (Lkup ix codes) c -> DelCtx ki codes iy (Lkup c (Lkup ix codes)) -> Almu ki codes ix iy