Type.Set.Variant

Core types

data Variant (v :: TypeSet *) where

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.

Constructors

Variant :: SSide ss -> Follow ss v -> Variant v

class Has t bst where

A proof that the set bst contains type t.

Methods

toVariant :: t -> Variant bst

Inject a t into a Variant.

fromVariant :: Variant bst -> Maybe t

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.

Instances

(Follow (Locate t bst) bst ~ t, FromSides (Locate t bst)) => Has t bst

Defined in Type.Set.Variant

Methods

toVariant :: t -> Variant bst

fromVariant :: Variant bst -> Maybe t

Decomposition proofs

decompRoot :: Variant (Branch t lbst rbst) -> Split t lbst rbst

Like fromVariant, but decomposes the Variant into its left and right branches, depending on where t is.

data Split t lbst rbst

Constructors

Root t

LSplit (Variant lbst)

RSplit (Variant rbst)

Weakening

weaken :: forall t bst. Variant bst -> Variant (Insert t bst)

Weaken a Variant so that it can contain something else.

Internal stuff

proveFollowInsert :: Follow ss (Insert t bst) :~: Follow ss bst

A proof that inserting into a bst doesn't affect the position of anything already in the tree.

data SSide (ss :: [Side]) where

Singletons for Sides.

Constructors

SNil :: SSide '[]

SL :: SSide ss -> SSide (L ': ss)

SR :: SSide ss -> SSide (R ': ss)

Instances

TestEquality SSide

Defined in Type.Set.Variant

Methods

testEquality :: SSide a -> SSide b -> Maybe (a :~: b)

class FromSides (ss :: [Side]) where

Get a singleton for a list of Sides.

Methods

fromSides :: SSide ss

Instances

FromSides ([] :: [Side])

Defined in Type.Set.Variant

Methods

fromSides :: SSide []

FromSides ss => FromSides (L ': ss)

Defined in Type.Set.Variant

Methods

fromSides :: SSide (L ': ss)

FromSides ss => FromSides (R ': ss)

Defined in Type.Set.Variant

Methods

fromSides :: SSide (R ': ss)