resin-0.2.0.3: High performance variable binders

Safe HaskellNone
LanguageHaskell2010

Resin.Binders.Tree.Internal

Synopsis

Documentation

the safe subset of the api... I think

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

Constructors

PolyRefl :: IxEq f i i 
MonoRefl :: forall f i. f i -> IxEq f i i 
Instances
TestEquality f => TestEquality (IxEq f i :: k -> Type) Source # 
Instance details

Defined in Resin.Binders.Tree.Internal

Methods

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

data Inject :: (k -> *) -> k -> k -> * 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 (Inject f :: k -> k -> Type) Source # 
Instance details

Defined in Resin.Binders.Tree.Internal

Methods

o :: Inject f j k1 -> Inject f i j -> Inject f i k1 #

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

Constructors

Dual :: Inject f b a -> Extract f a b 
Instances
Semigroupoid (Extract f :: k -> k -> Type) Source # 
Instance details

Defined in Resin.Binders.Tree.Internal

Methods

o :: Extract f j k1 -> Extract f i j -> Extract f i k1 #

data TreeEq :: (k -> *) -> k -> k -> * 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 #