Type.BST

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.

BST, Record and Union

Data Types

data BST a

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

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

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

Associated Types

type Fromlist as :: BST *

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)

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

Methods

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

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

Instances

Fromsumable' as (Fromlist as) => Fromsumable as

class Foldable t where

Minimal complete definition

tolist', tosum', virtual

Methods

virtual :: Record t

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)

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

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

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

type family Tolist t :: [*]

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

t has an Item with key.

Associated Types

type At t key :: *

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

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)

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

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

Infix synonym for at.

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

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)

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)

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

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

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

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

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

Instances

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

Searchable

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

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 *

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

Methods

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

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

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

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

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

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

Infix synonym for atX.

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

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)

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)

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

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

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

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

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

Infix operator that works almost like smapX.

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

Unioncasable

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

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

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

Methods

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

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'

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'

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'

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'

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

Associated Types

type Balance t :: BST *

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)

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

Methods

metamorphose :: f t -> f t'

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

Associated Types

type Merge t t' :: BST *

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 *

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')

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

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

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

Associated Types

type Insert t key a :: BST *

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)

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

Associated Types

type Delete t key :: BST *

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)

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

Associated Types

type Findmin t :: *

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))

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

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)

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

deletemin = snd . splitmin

class Maxable t where

Associated Types

type Findmax t :: *

Methods

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

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

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)

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

deletemin = snd . splitmin

Item

newtype Item key a

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

Infix synonym for Item.

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

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

Give a new key to an Item.

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

Make an Item setting a key with proxy.

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

Infix synonym for item.

List

data family List as

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

Infix synonym for Cons.

Sum

data family Sum as

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

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

The largest type (and kind) on Compare.

Constructors

Largest

data SmallestK

The smallest type (and kind) on Compare.

Constructors

Smallest

type family CompareUser a b :: Ordering

Compare two types. Users can add instances.

Showtype

class Showtype a where

Conversion of types to readable Strings. Analogous to Show.

Minimal complete definition

showtype | showtypesPrec

Methods

showtype :: proxy a -> String

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

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

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)