Safe Haskell	Safe
Language	Haskell2010

DeBruijn.Wk

Contents

Combinators
Index weakening
Size weakening
Environment contraction

Synopsis

data Wk ctx ctx' where
- IdWk :: Wk ctx ctx
- 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
wk1 :: Wk ctx (S ctx)
compWk :: Wk a b -> Wk b c -> Wk a c
weakenIdx :: Wk ctx ctx' -> Idx ctx -> Idx ctx'
weakenSize :: Wk ctx ctx' -> Size ctx -> Size ctx'
contractSize :: Wk ctx ctx' -> Size ctx' -> Size ctx
weakenEnv :: Wk ctx ctx' -> Env ctx' a -> Env ctx a
setWeakenEnv :: Wk ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a
overWeakenEnv :: Wk ctx ctx' -> (Env ctx a -> Env ctx a) -> Env ctx' a -> Env ctx' a

Documentation

data Wk ctx ctx' where Source #

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

Instances details

IdxMapping Identity Wk Source #
Instance details Defined in DeBruijn.Ren Methods mapIdx :: forall (ctx :: Ctx) (ctx' :: Ctx). Wk ctx ctx' -> Idx ctx -> Identity (Idx ctx') Source # keep :: forall (ctx :: Ctx) (ctx' :: Ctx). Wk ctx ctx' -> Wk (S ctx) (S ctx') Source # weakenIdxMapping :: forall (ctx :: Ctx) (ctx' :: Ctx) (ctx'' :: Ctx). Wk ctx ctx' -> Wk ctx' ctx'' -> Wk ctx ctx'' Source #
Show (Wk ctx ctx') Source #
Instance details 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') Source #
Instance details 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) Source #

Weaken by one. wk1 = SkipWk IdWk.

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

Weakening composition.

Index weakening

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

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

Size weakening

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

Weaken Size.

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

Environment contraction

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

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

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

Setter made from setWeakenEnv and weakenEnv.

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