DeBruijn.Wk

Documentation

data Wk ctx ctx' where

Weakenings, order preserving embeddings.

Wk n m could be represented as m bit field with popCount of n.

Constructor names make sense when you look at the implementation of weakenEnv.

Note: usually 'ViewWk is defined as

data Wk ctx ctx' where
    WkNil  :: Wk EmptyCtx EmptyCtx
    KeepWk :: Wk ctx ctx' -> Wk (S ctx)  (S ctx')
    SkipWk :: Wk ctx ctx' -> Wk    ctx   (S ctx')

However that representation doesn't allow to make wkId :: 'ViewWk ctx ctx without knowing the size of context. Therefore we morally use a representation closer to

data Wk ctx ctx' where
    IdWk   :: Wk ctx ctx
    KeepWk :: Wk ctx ctx' -> Wk (S ctx)  (S ctx')
    SkipWk :: Wk ctx ctx' -> Wk    ctx   (S ctx')

But we keep an invariant that identity weakenings are always represented by IdWk.

>>> KeepWk IdWk
IdWk

And KeepWk pattern doesn't match on identity weakenings.

>>> case IdWk :: Wk Ctx2 Ctx2 of { KeepWk _ -> "keep"; SkipWk _ -> "skip"; IdWk -> "id" } :: String
"id"

Constructors

IdWk :: Wk ctx ctx

Bundled Patterns

pattern SkipWk :: () => b ~ S b' => Wk a b' -> Wk a b

pattern KeepWk :: () => (a ~ S a', b ~ S b') => Wk a' b' -> Wk a b

Instances

IdxMapping Identity Wk

Defined in DeBruijn.Ren

Methods

mapIdx :: forall (ctx :: Ctx) (ctx' :: Ctx). Wk ctx ctx' -> Idx ctx -> Identity (Idx ctx')

keep :: forall (ctx :: Ctx) (ctx' :: Ctx). Wk ctx ctx' -> Wk (S ctx) (S ctx')

weakenIdxMapping :: forall (ctx :: Ctx) (ctx' :: Ctx) (ctx'' :: Ctx). Wk ctx ctx' -> Wk ctx' ctx'' -> Wk ctx ctx''

Show (Wk ctx ctx')

Defined in DeBruijn.Wk

Methods

showsPrec :: Int -> Wk ctx ctx' -> ShowS

show :: Wk ctx ctx' -> String

showList :: [Wk ctx ctx'] -> ShowS

Eq (Wk ctx ctx')

Defined in DeBruijn.Wk

Methods

(==) :: Wk ctx ctx' -> Wk ctx ctx' -> Bool

(/=) :: Wk ctx ctx' -> Wk ctx ctx' -> Bool

Combinators

wk1 :: Wk ctx (S ctx)

Weaken by one. wk1 = SkipWk IdWk.

compWk :: Wk a b -> Wk b c -> Wk a c

Weakening composition.

Index weakening

weakenIdx :: Wk ctx ctx' -> Idx ctx -> Idx ctx'

Weaken Idx, i.e. map index from smaller to larger context.

>>> IS IZ
1

>>> weakenIdx wk1 (IS IZ)
2

contractIdx :: Wk ctx ctx' -> Idx ctx' -> Maybe (Idx ctx)

Contract Idx, i.e. map index from larger to smaller context.

>>> contractIdx wk1 (IS IZ)
Just 0

>>> contractIdx wk1 IZ
Nothing

>>> contractIdx (SkipWk (KeepWk wk1)) <$> [IZ, IS IZ, IS (IS IZ), IS (IS IZ), IS (IS (IS IZ)), IS (IS (IS (IS IZ)))]
[Nothing,Just 0,Nothing,Nothing,Just 1,Just 2]

Size weakening

weakenSize :: Wk ctx ctx' -> Size ctx -> Size ctx'

Weaken Size.

contractSize :: Wk ctx ctx' -> Size ctx' -> Size ctx

Environment contraction

weakenEnv :: Wk ctx ctx' -> Env ctx' a -> Env ctx a

Contract Env i.e. drop elements from larger context.

This function explains the KeepWk and SkipWk constructor names:

>>> weakenEnv (IdWk & SkipWk & KeepWk) (EmptyEnv :> 'a' :> 'b' :> 'c' :> 'd' :> 'e')
EmptyEnv :> 'a' :> 'b' :> 'c' :> 'e'

setWeakenEnv :: Wk ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a

setWeakenEnv and weakenEnv together form a lens.

>>> setWeakenEnv (IdWk & SkipWk & KeepWk) (EmptyEnv :> 'a' :> 'b') (EmptyEnv :> 'x' :> 'y' :> 'z')
EmptyEnv :> 'a' :> 'y' :> 'b'

overWeakenEnv :: Wk ctx ctx' -> (Env ctx a -> Env ctx a) -> Env ctx' a -> Env ctx' a

Setter made from setWeakenEnv and weakenEnv.

>>> overWeakenEnv (IdWk & SkipWk & KeepWk) (fmap toUpper) (EmptyEnv :> 'a' :> 'x' :> 'y' :> 'z')
EmptyEnv :> 'A' :> 'X' :> 'y' :> 'Z'