Copyright | (c) Yusuke Matsushita 2014 |
---|---|
License | BSD3 |
Maintainer | Yusuke Matsushita |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell2010 |
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.
- data BST a
- data family Record s
- data family Union s
- class Fromlistable as where
- class Fromsumable as where
- class Foldable t where
- tolist :: Foldable t => Record t -> List (Tolist t)
- tosum :: Foldable t => Union t -> Sum (Tolist t)
- type family Tolist t :: [*]
- class Searchable t key (At t key) => Accessible t key where
- type At t key :: *
- at :: Accessible t key => Record t -> proxy key -> At t key
- proj :: Accessible t key => Union t -> proxy key -> Maybe (At t key)
- inj :: Accessible t key => proxy key -> At t key -> Union t
- (!) :: Accessible t key => Record t -> proxy key -> At t key
- class (Accessible t key, SearchableF f t key (At t key)) => AccessibleF f t key
- smap :: AccessibleF f t key => proxy key -> (At t key -> b) -> f t -> f (Smap t key (At t key) b)
- supdate :: AccessibleF f t key => proxy key -> b -> f t -> f (Smap t key (At t key) b)
- adjust :: AccessibleF f t key => proxy key -> (At t key -> At t key) -> f t -> f t
- update :: AccessibleF f t key => proxy key -> At t key -> f t -> f t
- (<$*>) :: AccessibleF f t key => (key |> (At t key -> b)) -> f t -> f (Smap t key (At t key) b)
- class (Accessible t key, a ~ At t key) => Contains t key a | t key -> a
- class Contains t key a => ContainedBy key a t | t key -> a
- class (Smap t key a a ~ t) => Searchable t key a where
- (!?) :: Searchable t key a => Record t -> proxy key -> Maybe a
- class Searchable t key a => SearchableF f t key a where
- supdateX :: SearchableF f t key (At t key) => proxy key -> b -> f t -> f (Smap t key (At t key) b)
- adjustX :: SearchableF f t key a => proxy key -> (a -> a) -> f t -> f t
- updateX :: SearchableF f t key a => proxy key -> a -> f t -> f t
- (<$*?>) :: SearchableF f t key a => (key |> (a -> b)) -> f t -> f (Smap t key a b)
- class UnioncasableX t t' res => Unioncasable t t' res
- unioncase :: Unioncasable t t' res => Union t -> Record t' -> res
- class UnioncasableX t t' res where
- unioncaseX :: Union t -> Record t' -> res
- class Includes t t'
- class Includes t' t => IncludedBy t t'
- shrink :: (Metamorphosable Record t t', Includes t t') => Record t -> Record t'
- expand :: (Metamorphosable Union t t', IncludedBy t t') => Union t -> Union t'
- class (Foldable t, Fromlistable (Tolist t)) => Balanceable t where
- class Metamorphosable f t t' where
- metamorphose :: f t -> f t'
- class Mergeable t t' where
- class Insertable t key where
- class Deletable t key where
- class Minnable t where
- findmin :: Minnable t => Record t -> Findmin t
- deletemin :: Minnable t => Record t -> Record (Deletemin t)
- class Maxable t where
- findmax :: Maxable t => Record t -> Findmax t
- deletemax :: Maxable t => Record t -> Record (Deletemax t)
- newtype Item key a = Item {
- value :: a
- type (|>) = Item
- type With key = forall a. a -> Item key a
- newkey :: Item key a -> proxy key' -> Item key' a
- item :: proxy key -> a -> Item key a
- (|>) :: proxy key -> a -> Item key a
- data family List as
- (.:.) :: a -> List as -> List (a : as)
- data family Sum as
- type family Compare a b :: Ordering
- data LargestK = Largest
- data SmallestK = Smallest
- type family CompareUser a b :: Ordering
- class Showtype a where
BST, Record and Union
Data Types
Type-level binary search tree used as an "ordered map".
a
is supposed to be a proper type
of the kind Item
key val*
,
where key
is a key type of an arbitrary kind
val
is a value type of the kind *
.
All Item
s in a BST
should have different keys.
Type inference works very well with BST
s, and value types can naturally be polymorphic.
If you want to build a new BST
, use Fromlist
, whose result is guaranteed to be balanced.
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) |
Dependently-typed union, or an extensible union.
If you want to build a new Union
, use inj
or fromsum
.
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) |
Conversion
class Fromlistable as where Source
type Fromlist as :: BST * Source
O(n log n). Convert from a type-level list to a BST
.
If as
has two or more Item
s 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]]
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
(Sortable as, Fromslistable (Sort as)) => Fromlistable as |
class Fromsumable as where Source
Fromsumable' as (Fromlist as) => Fromsumable as |
tolist', tosum', virtual
type family Tolist t :: [*] Source
O(n). Convert from a BST
to a type-level sorted list.
type Tolist t |
Accessible
class Searchable t key (At t key) => Accessible t key Source
t
has an Item
with key
.
at :: Accessible t key => Record t -> proxy key -> At t key Source
inj :: Accessible t key => proxy key -> At t key -> Union t Source
class (Accessible t key, SearchableF f t key (At t key)) => AccessibleF f t key Source
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
supdate :: AccessibleF f t key => proxy key -> b -> f t -> f (Smap t key (At t key) b) Source
adjust :: AccessibleF f t key => proxy key -> (At t key -> At t key) -> f t -> f t Source
update :: AccessibleF f t key => proxy key -> At t key -> f t -> f t Source
(<$*>) :: 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
(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
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 keya
should be
,
but when not, At
t keya
can be any type.
atX :: Record t -> proxy key -> Maybe a Source
projX :: Union t -> proxy key -> Maybe a Source
O(log n). proj
with a looser context.
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 |
class Searchable t key a => SearchableF f t key a where Source
smapX :: proxy key -> (a -> b) -> f t -> f (Smap t key a b) Source
O(log n). smap
with a looser context.
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
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
,
where Union
t
contains functions that return Record
t'res
for all items in t
.
A special version of unioncaseX
with a tighter context.
class UnioncasableX t t' res where Source
unioncaseX :: Union t -> Record t' -> res Source
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
t
includes t'
; in other words, t
contains all items in t'
.
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
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
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
.
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
.
(Foldable t, Fromlistable (Tolist t)) => Balanceable t |
Metamorphosis
class Metamorphosable f t t' where Source
metamorphose :: f t -> f t' Source
MetamorphosableU t t' => Metamorphosable Union t t' | |
MetamorphosableR t t' => Metamorphosable Record t t' |
Merging
class Mergeable t t' where Source
type Merge t t' :: BST * Source
O(n log n + n' log n'). Merge two BST
s.
If t
and t'
has an Item
with the same key,
only the one in t
will be added to the result.
Insertion
class Insertable t key where Source
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.
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
Min and Max
Item
Item
used in BST
.
(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 |
List
Dependently-typed list.
Sum
Dependently-typed sum.
Comparison
type family Compare a b :: Ordering Source
Compare two types.
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 |
type family CompareUser a b :: Ordering Source
Compare two types. Users can add instances.