Copyright	(c) Yusuke Matsushita 2014
License	BSD3
Maintainer	Yusuke Matsushita
Stability	provisional
Portability	portable
Safe Haskell	Safe
Language	Haskell2010

Type.BST

Contents

BST, Record and Union
Item
List
Sum
Comparison
Showtype

Description

An efficient implementation of type-level binary search trees and of dependently-typed extensible records and unions.

Comments on some type families and functions contain the time complexity in the Big-O notation on an assumption that t (or t') is balanced.

This library does not export a proxy type. Since proxy is polymorphic, you can use your own proxy type, and you can also use the one in Data.Proxy.

Synopsis

BST, Record and Union

Data Types

data BST a Source

Type-level binary search tree used as an "ordered map".

a is supposed to be a proper type Item key val of the kind *, where key is a key type of an arbitrary kind val is a value type of the kind *. All Items in a BST should have different keys.

Type inference works very well with BSTs, and value types can naturally be polymorphic.

If you want to build a new BST, use Fromlist, whose result is guaranteed to be balanced.

Constructors

Leaf
Node (BST a) a (BST a)

data family Record s Source

Dependently-typed record, or an extensible record. If you want to build a new Record, use fromlist.

Instances

MetamorphosableR t t' => Metamorphosable Record t t'
Accessible k t key => AccessibleF k Record t key
Searchable k t key a => SearchableF k Record t key a
(Foldable s, Show (List (Tolist s))) => Show (Record s)
data Record (Leaf *) = None
data Record (Node * l a r) = Triple (Record l) a (Record r)

data family Union s Source

Dependently-typed union, or an extensible union. If you want to build a new Union, use inj or fromsum.

Instances

MetamorphosableU t t' => Metamorphosable Union t t'
Accessible k t key => AccessibleF k Union t key
Searchable k t key a => SearchableF k Union t key a
(Show a, Show (Union l), Show (Union r)) => Show (Union (Node * l a r))
Show (Union (Leaf *))
data Union (Leaf *)
data Union (Node * l a r) = Top a \| GoL (Union l) \| GoR (Union r)

Conversion

class Fromlistable as where Source

Associated Types

type Fromlist as :: BST * Source

O(n log n). Convert from a type-level list to a BST. If as has two or more Items that have the same key, only the first one will be added to the result.

If as and bs have the same items (just in different orders), Fromlist as == Fromlist bs.

Example:

>>> type T = Fromlist [0 |> Bool, 4 |> String, 2 |> Int, 3 |> Double, 1 |> Char]
>>> :kind! T
T :: BST *
= 'Node
    ('Node 'Leaf (Item 0 Bool) ('Node 'Leaf (Item 1 Char) 'Leaf))
    (Item 2 Int)
    ('Node ('Node 'Leaf (Item 3 Double) 'Leaf) (Item 4 [Char]) 'Leaf)
>>> :kind! Tolist T
Tolist T :: [*]
= '[Item 0 Bool, Item 1 Char, Item 2 Int, Item 3 Double,
    Item 4 [Char]]

Methods

fromlist :: List as -> Record (Fromlist as) Source

O(n log n). Convert from a List to a Record.

If rc and rc' have the same items (just in different orders), fromlist rc == fromlist rc'.

Example (where T is a type defined in the previous example):

>>> let rct = fromlist $ p3 |> 3 .:. p0 |> True .:. p2 |> 10 .:. p4 |> "wow" .:. p1 |> 'a' .:. Nil
>>> rct
<Record> [<0> True,<1> 'a',<2> 10,<3> 3,<4> "wow"]
>>> :type rct
rct
  :: (Num a1, Num a) =>
     Record
       ('Node
          ('Node 'Leaf (Item 0 Bool) ('Node 'Leaf (Item 1 Char) 'Leaf))
          (Item 2 a1)
          ('Node ('Node 'Leaf (Item 3 a) 'Leaf) (Item 4 [Char]) 'Leaf))
>>> :type rct :: Record T
rct :: Record T :: Record T

Instances

(Sortable as, Fromslistable (Sort as)) => Fromlistable as

class Fromsumable as where Source

Methods

fromsum :: Sum as -> Union (Fromlist as) Source

O(n). Convert from a Sum to a Union.

Instances

Fromsumable' as (Fromlist as) => Fromsumable as

class Foldable t where Source

Minimal complete definition

tolist', tosum', virtual

Methods

virtual :: Record t Source

Build a Record with empty Items.

Instances

Foldable (Leaf *)
(Foldable l, Foldable r) => Foldable (Node * l a r)

tolist :: Foldable t => Record t -> List (Tolist t) Source

O(n). Convert from a Record to a List.

tosum :: Foldable t => Union t -> Sum (Tolist t) Source

O(n). Convert from a Union to a Sum.

type family Tolist t :: [*] Source

O(n). Convert from a BST to a type-level sorted list.

Instances

type Tolist t

Accessible

class Searchable t key (At t key) => Accessible t key Source

t has an Item with key.

Associated Types

type At t key :: * Source

O(log n). Find the type at key.

Instances

Accessible' k (Compare k k1 key key') (Node * l ((|>) k1 key' a) r) key => Accessible k (Node * l ((|>) k key' a) r) key

at :: Accessible t key => Record t -> proxy key -> At t key Source

O(log n). Get the value at key in a Record.

A special version of atX with a tighter context and without Maybe.

proj :: Accessible t key => Union t -> proxy key -> Maybe (At t key) Source

O(log n). Get the value at key in a Union.

A special version of projX with a tighter context.

inj :: Accessible t key => proxy key -> At t key -> Union t Source

O(log n). Injection to a dependently-typed union. One way to build a Union.

A special version of injX with a tighter context and without Maybe.

Just (inj p x) == injX p x

(!) :: Accessible t key => Record t -> proxy key -> At t key infixl 9 Source

Infix synonym for at.

class (Accessible t key, SearchableF f t key (At t key)) => AccessibleF f t key Source

When f is either Record or Union,

AccessibleF f t key == Accessible t key

Instances

Accessible k t key => AccessibleF k Union t key
Accessible k t key => AccessibleF k Record t key

smap :: AccessibleF f t key => proxy key -> (At t key -> b) -> f t -> f (Smap t key (At t key) b) Source

O(log n). smap stands for "super-map". Change the value of the Item at key in f t by applying the function At t key -> b. A special version of smapX with a tighter context.

supdate :: AccessibleF f t key => proxy key -> b -> f t -> f (Smap t key (At t key) b) Source

O(log n). supdate stands for "super-update". A special version of supdateX with a tighter context.

supdate p x == smap p (const x)

adjust :: AccessibleF f t key => proxy key -> (At t key -> At t key) -> f t -> f t Source

O(log n). A special version of smap that does not change the value type. A special version of adjustX with a tighter context.

update :: AccessibleF f t key => proxy key -> At t key -> f t -> f t Source

O(log n). A special version of supdate that does not change the value type. A special version of updateX with a tighter context.

update p x == adjust p (const x)

(<$*>) :: AccessibleF f t key => (key |> (At t key -> b)) -> f t -> f (Smap t key (At t key) b) infixl 4 Source

Infix operator that works almost like smap.

(p |> f) <$*> c = smap p f c

class (Accessible t key, a ~ At t key) => Contains t key a | t key -> a Source

Instances

(Accessible k t key, (~) * a (At k t key)) => Contains k t key a

class Contains t key a => ContainedBy key a t | t key -> a Source

Instances

Contains k t key a => ContainedBy k key a t

Searchable

class (Smap t key a a ~ t) => Searchable t key a where Source

t may have an Item with a key type key and a value type a.

When Accessible t key, a should be At t key, but when not, a can be any type.

Minimal complete definition

atX, projX, injX, smapXR, smapXU

Associated Types

type Smap t key a b :: BST * Source

O(log n). Change the value type of an Item at key from a to b.

Methods

atX :: Record t -> proxy key -> Maybe a Source

O(log n). at with a looser context and Maybe.

projX :: Union t -> proxy key -> Maybe a Source

O(log n). proj with a looser context.

injX :: proxy key -> a -> Maybe (Union t) Source

O(log n). inj with a looser context and Maybe.

Instances

Searchable k (Leaf *) _' _''
Searchable' k (Compare k k1 key key') (Node * l ((\|>) k1 key' c) r) key a => Searchable k (Node * l ((\|>) k key' c) r) key a

(!?) :: Searchable t key a => Record t -> proxy key -> Maybe a Source

Infix synonym for atX.

class Searchable t key a => SearchableF f t key a where Source

When f is either Record or Union,

SearchableF f t key == Searchable t key

Methods

smapX :: proxy key -> (a -> b) -> f t -> f (Smap t key a b) Source

O(log n). smap with a looser context.

Instances

Searchable k t key a => SearchableF k Union t key a
Searchable k t key a => SearchableF k Record t key a

supdateX :: SearchableF f t key (At t key) => proxy key -> b -> f t -> f (Smap t key (At t key) b) Source

O(log n). supdate with a looser context.

adjustX :: SearchableF f t key a => proxy key -> (a -> a) -> f t -> f t Source

O(log n). adjust with a looser context.

updateX :: SearchableF f t key a => proxy key -> a -> f t -> f t Source

O(log n). update with a looser context.

(<$*?>) :: SearchableF f t key a => (key |> (a -> b)) -> f t -> f (Smap t key a b) infixl 4 Source

Infix operator that works almost like smapX.

(p |> f) <$*?> c = smapX p f cz

Unioncasable

class UnioncasableX t t' res => Unioncasable t t' res Source

Instances

Unioncasable (Leaf *) t' res
(Contains k t' key (a -> res), Unioncasable l t' res, Unioncasable r t' res) => Unioncasable (Node * l (Item k key a) r) t' res

unioncase :: Unioncasable t t' res => Union t -> Record t' -> res Source

O(log n + log n'). Pattern matching on Union t, where Record t' contains functions that return res for all items in t.

A special version of unioncaseX with a tighter context.

class UnioncasableX t t' res where Source

Methods

unioncaseX :: Union t -> Record t' -> res Source

O(log n + log n'). Pattern matching on Union t, where Record t' contains functions that return res for some items in t.

unioncase with a looser context.

Instances

UnioncasableX (Leaf *) t' res
(Searchable k t' key (a -> res), UnioncasableX l t' res, UnioncasableX r t' res) => UnioncasableX (Node * l (Item k key a) r) t' res

Inclusion

class Includes t t' Source

t includes t'; in other words, t contains all items in t'.

Instances

Includes t (Leaf *)
(Contains k t key a, Includes t l, Includes t r) => Includes t (Node * l ((\|>) k key a) r)

class Includes t' t => IncludedBy t t' Source

t is included by t'; in other words, t' contains all items in t.

IncludedBy t t' == Includes t' t

Instances

Includes t' t => IncludedBy t t'

shrink :: (Metamorphosable Record t t', Includes t t') => Record t -> Record t' Source

O(n log n'). A special version of metamorphose with a tighter context guaranteeing the safety of the conversion.

expand :: (Metamorphosable Union t t', IncludedBy t t') => Union t -> Union t' Source

O(log n + log n'). A special version of metamorphose with a tighter context guaranteeing the safety of the conversion.

Balancing

class (Foldable t, Fromlistable (Tolist t)) => Balanceable t where Source

Associated Types

type Balance t :: BST * Source

O(n log n) (no matter how unbalanced t is). Balance an unbalanced BST.

Doing a lot of insertions and deletions may cause an unbalanced BST.

If t and t' have the same items (just in different orders), Balance t == Balance t',

Moreover, if t and as have the same items (just in different orders), Balance t = Fromlist as.

Methods

balance :: Record t -> Record (Balance t) Source

O(n log n) (no matter how unbalanced t is). Balance an unbalanced Record.

If rc and rc' have the same items (just in different orders), balance rc == balance rc',

Moreover, if rc and l have the same items (just in different orders), balance rc = fromlist l.

Instances

(Foldable t, Fromlistable (Tolist t)) => Balanceable t

Metamorphosis

class Metamorphosable f t t' where Source

Methods

metamorphose :: f t -> f t' Source

O(n log n') when f is Record and O(log n + log n') when f is Union.

Possibly unsafe conversion from f t to f t'.

Instances

MetamorphosableU t t' => Metamorphosable Union t t'
MetamorphosableR t t' => Metamorphosable Record t t'

Merging

class Mergeable t t' where Source

Associated Types

type Merge t t' :: BST * Source

O(n log n + n' log n'). Merge two BSTs. If t and t' has an Item with the same key, only the one in t will be added to the result.

type MergeE t t' :: BST * Source

O(n log n + n' log n'). Merge two BSTs in a more equal manner. If t has Item key a and t' has Item key b, Item key (a, b) will be added to the result.

Methods

merge :: Record t -> Record t' -> Record (Merge t t') Source

O(n log n + n' log n'). Merge two Records.

mergeE :: Record t -> Record t' -> Record (MergeE t t') Source

O(n log n + n' log n'). Merge two Records in a more equal manner.

Instances

(Foldable t, Foldable t', MergeableL (Tolist t) (Tolist t'), Fromlistable (MergeL (Tolist t) (Tolist t')), Fromlistable (MergeEL (Tolist t) (Tolist t'))) => Mergeable t t'

Insertion

class Insertable t key where Source

Associated Types

type Insert t key a :: BST * Source

O(log n). Insert Item key a into the BST. If t already has an Item with key, the Item will be overwritten. The result may be unbalanced.

Methods

insert :: proxy key -> a -> Record t -> Record (Insert t key a) Source

O(log n). Insert a at key into the Record. The result may be unbalanced.

Instances

Insertable k (Leaf *) key
Insertable' k (Compare k k1 key key') (Node * l ((\|>) k1 key' b) r) key => Insertable k (Node * l ((\|>) k key' b) r) key

Deletion

class Deletable t key where Source

Associated Types

type Delete t key :: BST * Source

O(log n). Delete an Item at key from the BST. If the BST does not have any item at key, the original BST will be returned. The result may be unbalanced.

Methods

delete :: proxy key -> Record t -> Record (Delete t key) Source

O(log n). Delete an Item at key from the Record.

Instances

Deletable k (Leaf *) key
Deletable' k (Compare k k1 key key') (Node * l ((\|>) k1 key' a) r) key => Deletable k (Node * l ((\|>) k key' a) r) key

Min and Max

class Minnable t where Source

Associated Types

type Findmin t :: * Source

O(log n). Get the value type of the Item at the minimum key in the BST.

Methods

splitmin :: Record t -> (Findmin t, Record (Deletemin t)) Source

O(log n). Split the Record into (the value of) the Item at the minimum key and the rest.

Instances

Minnable (Node * l' b r') => Minnable (Node * (Node * l' b r') a r)
Minnable (Node * (Leaf *) a r)

findmin :: Minnable t => Record t -> Findmin t Source

O(log n). Get the value of the Item at the minimum key in the Record.

findmin = fst . splitmin

deletemin :: Minnable t => Record t -> Record (Deletemin t) Source

O(log n). Delete the Item at the minimum key from the Record.

deletemin = snd . splitmin

class Maxable t where Source

Associated Types

type Findmax t :: * Source

Methods

splitmax :: Record t -> (Findmax t, Record (Deletemax t)) Source

O(log n). Get the value type of the Item at the maximum key in the BST.

Instances

Maxable (Node * l' b r') => Maxable (Node * l a (Node * l' b r'))
Maxable (Node * l a (Leaf *))

findmax :: Maxable t => Record t -> Findmax t Source

O(log n). Get the value of the Item at the maximum key in the Record.

findmin = fst . splitmin

deletemax :: Maxable t => Record t -> Record (Deletemax t) Source

O(log n). Delete the Item at the maximum key from the Record.

deletemin = snd . splitmin

Item

newtype Item key a Source

Item used in BST.

Constructors

Item
Fields value :: a

Instances

(Contains k t key a, Includes t l, Includes t r) => Includes t (Node * l ((\|>) k key a) r)
Deletable' k (Compare k k1 key key') (Node * l ((\|>) k1 key' a) r) key => Deletable k (Node * l ((\|>) k key' a) r) key
Insertable' k (Compare k k1 key key') (Node * l ((\|>) k1 key' b) r) key => Insertable k (Node * l ((\|>) k key' b) r) key
Accessible' k (Compare k k1 key key') (Node * l ((\|>) k1 key' a) r) key => Accessible k (Node * l ((\|>) k key' a) r) key
Searchable' k (Compare k k1 key key') (Node * l ((\|>) k1 key' c) r) key a => Searchable k (Node * l ((\|>) k key' c) r) key a
(Showtype k key, Show a) => Show (Item k key a)
(Searchable k t' key (a -> res), UnioncasableX l t' res, UnioncasableX r t' res) => UnioncasableX (Node * l (Item k key a) r) t' res
(Contains k t' key (a -> res), Unioncasable l t' res, Unioncasable r t' res) => Unioncasable (Node * l (Item k key a) r) t' res
type Delete k (Node * l ((\|>) k1 key' a) r) key
type At k (Node * l ((\|>) k1 key' a) r) key
type Insert k (Node * l ((\|>) k1 key' b) r) key a
type Smap k (Node * l ((\|>) k1 key' c) r) key a b

type (|>) = Item infixr 6 Source

Infix synonym for Item.

type With key = forall a. a -> Item key a Source

When x has a type T, (Item :: With key) x works as Item x :: Item key T.

Using With, you can avoid writing T.

newkey :: Item key a -> proxy key' -> Item key' a Source

Give a new key to an Item.

item :: proxy key -> a -> Item key a Source

Make an Item setting a key with proxy.

(|>) :: proxy key -> a -> Item key a infixr 6 Source

Infix synonym for item.

List

data family List as Source

Dependently-typed list.

Instances

(Show a, Showlist (List as)) => Show (List ((:) * a as))
Show (List ([] *))
data List ([] *) = Nil
data List ((:) * a as) = Cons a (List as)

(.:.) :: a -> List as -> List (a : as) infixr 5 Source

Infix synonym for Cons.

Sum

data family Sum as Source

Dependently-typed sum.

Instances

(Show a, Show (Sum as)) => Show (Sum ((:) * a as))
Show (Sum ([] *))
data Sum ([] *)
data Sum ((:) * a as) = Head a \| Tail (Sum as)

Comparison

type family Compare a b :: Ordering Source

Compare two types.

Equations

Compare Largest Largest = EQ
Compare _' Largest = LT
Compare Largest _' = GT
Compare Smallest Smallest = EQ
Compare _' Smallest = GT
Compare Smallest _' = LT
Compare False False = EQ
Compare False True = LT
Compare True False = GT
Compare True True = EQ
Compare LT LT = EQ
Compare LT EQ = LT
Compare LT GT = LT
Compare EQ LT = GT
Compare EQ EQ = EQ
Compare EQ GT = LT
Compare GT LT = GT
Compare GT EQ = GT
Compare GT GT = EQ
Compare m n = CmpNat m n
Compare s t = CmpSymbol s t
Compare Nothing Nothing = EQ
Compare Nothing (Just b) = LT
Compare (Just a) Nothing = GT
Compare (Just a) (Just b) = Compare a b
Compare (Left _') (Right _'') = LT
Compare (Right _') (Left _'') = GT
Compare (Left a) (Left b) = Compare a b
Compare (Right a) (Right b) = Compare a b
Compare [] [] = EQ
Compare [] (b : bs) = LT
Compare (a : as) [] = GT
Compare (a : as) (b : bs) = Compare a b $$ Compare as bs
Compare `(a1, a2)` `(b1, b2)` = Compare a1 b1 $$ Compare a2 b2
Compare `(a1, a2, a3)` `(b1, b2, b3)` = (Compare a1 b1 $$ Compare a2 b2) $$ Compare a3 b3
Compare `(a1, a2, a3, a4)` `(b1, b2, b3, b4)` = ((Compare a1 b1 $$ Compare a2 b2) $$ Compare a3 b3) $$ Compare a4 b4
Compare `(a1, a2, a3, a4, a5)` `(b1, b2, b3, b4, b5)` = (((Compare a1 b1 $$ Compare a2 b2) $$ Compare a3 b3) $$ Compare a4 b4) $$ Compare a5 b5
Compare `(a1, a2, a3, a4, a5, a6)` `(b1, b2, b3, b4, b5, b6)` = ((((Compare a1 b1 $$ Compare a2 b2) $$ Compare a3 b3) $$ Compare a4 b4) $$ Compare a5 b5) $$ Compare a6 b6
Compare `(a1, a2, a3, a4, a5, a6, a7)` `(b1, b2, b3, b4, b5, b6, b7)` = (((((Compare a1 b1 $$ Compare a2 b2) $$ Compare a3 b3) $$ Compare a4 b4) $$ Compare a5 b5) $$ Compare a6 b6) $$ Compare a7 b7
Compare `(a1, a2, a3, a4, a5, a6, a7, a8)` `(b1, b2, b3, b4, b5, b6, b7, b8)` = ((((((Compare a1 b1 $$ Compare a2 b2) $$ Compare a3 b3) $$ Compare a4 b4) $$ Compare a5 b5) $$ Compare a6 b6) $$ Compare a7 b7) $$ Compare a8 b8
Compare `(a1, a2, a3, a4, a5, a6, a7, a8, a9)` `(b1, b2, b3, b4, b5, b6, b7, b8, b9)` = (((((((Compare a1 b1 $$ Compare a2 b2) $$ Compare a3 b3) $$ Compare a4 b4) $$ Compare a5 b5) $$ Compare a6 b6) $$ Compare a7 b7) $$ Compare a8 b8) $$ Compare a9 b9
Compare `(a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)` `(b1, b2, b3, b4, b5, b6, b7, b8, b9, b10)` = ((((((((Compare a1 b1 $$ Compare a2 b2) $$ Compare a3 b3) $$ Compare a4 b4) $$ Compare a5 b5) $$ Compare a6 b6) $$ Compare a7 b7) $$ Compare a8 b8) $$ Compare a9 b9) $$ Compare a10 b10
Compare (Item key a) (Item key' b) = Compare key key'
Compare a b = CompareUser a b

data LargestK Source

The largest type (and kind) on Compare.

Constructors

Largest

data SmallestK Source

The smallest type (and kind) on Compare.

Constructors

Smallest

type family CompareUser a b :: Ordering Source

Compare two types. Users can add instances.

Showtype

class Showtype a where Source

Conversion of types to readable Strings. Analogous to Show.

Minimal complete definition

showtype | showtypesPrec

Methods

showtype :: proxy a -> String Source

Convert a type a to a readable String. Analogous to show in Show.

showtypesPrec :: Int -> proxy a -> String -> String Source

Convert a type a to a readable String with additional arguments. Analogous to showsPrec in Show.

Instances

Showtype Bool False
Showtype Bool True
Showtype Ordering LT
Showtype Ordering EQ
Showtype Ordering GT
KnownNat n => Showtype Nat n
KnownSymbol s => Showtype Symbol s
(Showtype * a, Showtype * b) => Showtype * (a, b)
(Showtype * a, Showtype * b, Showtype * c) => Showtype * (a, b, c)
(Showtype * a, Showtype * b, Showtype * c, Showtype * d) => Showtype * (a, b, c, d)
(Showtype * a, Showtype * b, Showtype * c, Showtype * d, Showtype * e) => Showtype * (a, b, c, d, e)
(Showtype * a, Showtype * b, Showtype * c, Showtype * d, Showtype * e, Showtype * f) => Showtype * (a, b, c, d, e, f)
(Showtype * a, Showtype * b, Showtype * c, Showtype * d, Showtype * e, Showtype * f, Showtype * g) => Showtype * (a, b, c, d, e, f, g)
(Showtype * a, Showtype * b, Showtype * c, Showtype * d, Showtype * e, Showtype * f, Showtype * g, Showtype * h) => Showtype * (a, b, c, d, e, f, g, h)
(Showtype * a, Showtype * b, Showtype * c, Showtype * d, Showtype * e, Showtype * f, Showtype * g, Showtype * h, Showtype * i) => Showtype * (a, b, c, d, e, f, g, h, i)
(Showtype * a, Showtype * b, Showtype * c, Showtype * d, Showtype * e, Showtype * f, Showtype * g, Showtype * h, Showtype * i, Showtype * j) => Showtype * (a, b, c, d, e, f, g, h, i, j)
Showtype [k] ([] k)
Showtype (Maybe k) (Nothing k)
Showtype k a => Showtype (Maybe k) (Just k a)
(Showtype k a, Showlisttype k as) => Showtype [k] ((:) k a as)
Showtype k1 a => Showtype (Either k k) (Right k k a)
Showtype k a => Showtype (Either k k) (Left k k a)

(Contains k t key a, Includes t l, Includes t r) => Includes t (Node * l ((\|>) k key a) r)
Deletable' k (Compare k k1 key key') (Node * l ((\|>) k1 key' a) r) key => Deletable k (Node * l ((\|>) k key' a) r) key
Insertable' k (Compare k k1 key key') (Node * l ((\|>) k1 key' b) r) key => Insertable k (Node * l ((\|>) k key' b) r) key
Accessible' k (Compare k k1 key key') (Node * l ((\|>) k1 key' a) r) key => Accessible k (Node * l ((\|>) k key' a) r) key
Searchable' k (Compare k k1 key key') (Node * l ((\|>) k1 key' c) r) key a => Searchable k (Node * l ((\|>) k key' c) r) key a
(Showtype k key, Show a) => Show (Item k key a)
(Searchable k t' key (a -> res), UnioncasableX l t' res, UnioncasableX r t' res) => UnioncasableX (Node * l (Item k key a) r) t' res
(Contains k t' key (a -> res), Unioncasable l t' res, Unioncasable r t' res) => Unioncasable (Node * l (Item k key a) r) t' res
type Delete k (Node * l ((\|>) k1 key' a) r) key
type At k (Node * l ((\|>) k1 key' a) r) key
type Insert k (Node * l ((\|>) k1 key' b) r) key a
type Smap k (Node * l ((\|>) k1 key' c) r) key a b