Resin.Binders.Tree.Internal

Documentation

the safe subset of the api... I think

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

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)

Methods

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

data Inject :: (k -> *) -> k -> k -> * where

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)

Methods

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

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

Constructors

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

Instances

Semigroupoid k (Extract k f)

Methods

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

data TreeEq :: (k -> *) -> k -> k -> * where

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

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

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

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

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