| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Type.Set.Variant
Synopsis
- data Variant (v :: TypeSet *) where
- class Has t bst where
- toVariant :: t -> Variant bst
- fromVariant :: Variant bst -> Maybe t
- decompRoot :: Variant (Branch t lbst rbst) -> Split t lbst rbst
- data Split t lbst rbst
- weaken :: forall t bst. Variant bst -> Variant (Insert t bst)
- proveFollowInsert :: Follow ss (Insert t bst) :~: Follow ss bst
- data SSide (ss :: [Side]) where
- class FromSides (ss :: [Side]) where
Core types
data Variant (v :: TypeSet *) where Source #
A Variant is like an Either, except that it can store any of the types
contained in the TypeSet. You can use toVariant to construct one, and
fromVariant to pattern match it out.
class Has t bst where Source #
A proof that the set bst contains type t.
Methods
toVariant :: t -> Variant bst Source #
Inject a t into a Variant.
fromVariant :: Variant bst -> Maybe t Source #
Attempt to project a Variant into t. This might fail, because there
is no guarantee that the Variant actually contains t.
You can use decompRoot instead of this function if you'd like a proof
that the Variant doesn't contain t in the case of failure.
Decomposition proofs
decompRoot :: Variant (Branch t lbst rbst) -> Split t lbst rbst Source #
Like fromVariant, but decomposes the Variant into its left and right
branches, depending on where t is.
Weakening
weaken :: forall t bst. Variant bst -> Variant (Insert t bst) Source #
Weaken a Variant so that it can contain something else.
Internal stuff
proveFollowInsert :: Follow ss (Insert t bst) :~: Follow ss bst Source #
A proof that inserting into a bst doesn't affect the position of
anything already in the tree.
data SSide (ss :: [Side]) where Source #
Singletons for Sides.
Instances
| TestEquality SSide Source # | |
Defined in Type.Set.Variant | |