resin-0.2.0.0: High performance variable binders

Safe HaskellNone
LanguageHaskell2010

Resin.Binders.Tree.Internal

Synopsis

Documentation

the safe subset of the api... I think

data IxEq :: (k -> Type) -> k -> k -> Type where Source #

Constructors

PolyRefl :: IxEq f i i 
MonoRefl :: forall f i. f i -> IxEq f i i 

Instances

TestEquality k f => TestEquality k (IxEq k f i) Source # 

Methods

testEquality :: f a -> f b -> Maybe ((IxEq k f i :~: a) b) #

data Inject :: (k -> Type) -> k -> k -> Type where Source #

Inject is about

Constructors

InjectRefl :: forall f a b. IxEq f a b -> Inject f a b 
CompactCompose :: forall f i j. IxEq f i i -> IxEq f j j -> Natural -> Inject f i j 

Instances

Semigroupoid k (Inject k f) Source # 

Methods

o :: c j k1 -> c i j -> c i k1 #

newtype Extract :: (k -> Type) -> k -> k -> Type where Source #

Constructors

Dual :: Inject f b a -> Extract f a b 

Instances

Semigroupoid k (Extract k f) Source # 

Methods

o :: c j k1 -> c i j -> c i k1 #

data TreeEq :: (k -> Type) -> k -> k -> Type where Source #

Constructors

TreeInject :: Inject f a b -> TreeEq f a b 
TreeExtract :: Extract f a b -> TreeEq f a b 
TreeRefl :: TreeEq f c c 

treeElimination :: TestEquality f => Inject f a b -> Extract f b c -> TreeEq f a c Source #

rightExtendInject :: Inject p a b -> p c -> Inject p a c Source #

leftExtendExtract :: p a -> Extract p b c -> Extract p a c Source #

jumpDepthInject :: Natural -> p c -> Inject p a b -> Inject p a c Source #

jumpDepthExtract :: Natural -> Extract p b c -> p a -> Extract p a c Source #