Linearly usable maps and sets on identifiers
- module Data.Subtyping
- module Data.TypeInt
- module Control.Functor
- data Id k
- equalBy :: Maplike i k a -> Id k -> Id k -> Bool
- type Map i k a = Maplike (M i) k a
- type Set i k = Maplike (S Zero i) k ()
- insert :: forall i k a. MaplikeClass i a => Id k -> a -> Maplike i k a -> Maplike i k a
- delete :: forall i k a. MaplikeClass i a => Id k -> Maplike i k a -> Maplike i k a
- lookUp :: forall i k a. MaplikeClass i a => Id k -> Maplike i k a -> Maybe a
- member :: MaplikeClass i a => Id k -> Maplike i k a -> Bool
- union :: Maplike i k1 a -> Maplike i k2 a -> Maplike i (k1 :|: k2) a
- unsafeInsert :: forall i k a. MaplikeClass i a => Id k -> a -> Maplike i k a -> ()
- unsafeEquivalent :: Maplike i k a -> Maplike i k a -> Maplike i k a
- data Sets i k where
- data Maps i k where
- type ICC i k a = Maps i k -> (forall b. Map Zero k b) -> [Id k] -> a
- runICC :: I i => (forall k. ICC i k a) -> a
- type ICCS i k a = Maps i k -> Sets I32 k -> [Id k] -> a
- runICCS :: I i => (forall k. ICCS i k a) -> a
- data Maplike i k a
- class MaplikeClass i x
- inserts :: I i => Map i k a -> [(Id k, a)] -> Map i k a
- (!) :: I i => Map i k a -> Id k -> a
- setInsert :: I i => Id k -> Set i k -> Set i k
- setInserts :: I i => Set i k -> [Id k] -> Set i k
Documentation
module Data.Subtyping
module Data.TypeInt
module Control.Functor
Identifiers
Identifiers indexed by k
. (Id k)
can be seen as a set of identifiers.
The possible identifier indexes form a recursive set. An identifier index is either
equalBy :: Maplike i k a -> Id k -> Id k -> BoolSource
Equality check of identifiers. The first map parameter is the witness that the identifiers are sane.
The first parameter prevents identifiers of type
which could cause strange runtime behaviour.
For example, Id
(a :|: a)(
should be left
x == right
x)False
in theory, but during runtime (
and left
x)(
are exactly the same identifiers.
right
x)
Finite maps and sets
type Map i k a = Maplike (M i) k aSource
Family of finite maps from keys (
to values Id
k)a
.
For efficiency reasons, use only with concrete type integers:
Map I0 k a Map I1 k a Map I2 k a ...
type Set i k = Maplike (S Zero i) k ()Source
Family of finite sets of keys (
.
For efficiency reasons, use only with concrete type integers:
Id
k)
Set I0 k Set I1 k Set I2 k ...
insert :: forall i k a. MaplikeClass i a => Id k -> a -> Maplike i k a -> Maplike i k aSource
O(1). Insert a new key and value in the map. If the key is already present in the map, the associated value is replaced with the supplied value.
After insertion, the original map may not be used.
delete :: forall i k a. MaplikeClass i a => Id k -> Maplike i k a -> Maplike i k aSource
O(1). Delete a key and its value from the map. When the key is not a member of the map, the original map is returned.
After deletion, the original map may not be used.
lookUp :: forall i k a. MaplikeClass i a => Id k -> Maplike i k a -> Maybe aSource
O(1). Look up the value at a key in the map.
union :: Maplike i k1 a -> Maplike i k2 a -> Maplike i (k1 :|: k2) aSource
O(0). Union of two maps.
Linearity constraints:
- After union, the component maps may also be used.
- After insertion into either components, the union map may not be used.
- After insertion into the union map, the components may not be used.
Unsafe operations
unsafeInsert :: forall i k a. MaplikeClass i a => Id k -> a -> Maplike i k a -> ()Source
unsafeEquivalent :: Maplike i k a -> Maplike i k a -> Maplike i k aSource
Unsafe equality coercion of maps.
The two maps are equal, so every link to the first map could be safely replaced by a link to the second map.
Range of sets and maps
Helps to store a range of sets numbered from 0 to i
-1.
For example, (Sets I3 k)
is similar to (Set I2 k, Set I1 k, Set I0 k)
.
Helps to store a range of maps numbered from 1 to i
.
For example, (Maps1 I3 k)
is similar to (forall a . Map I3 k a, forall a . Map I2 k a, forall a . Map I1 k a)
.
Creation of sets, maps and identifiers
type ICC i k a = Maps i k -> (forall b. Map Zero k b) -> [Id k] -> aSource
Identifier-consuming computation. i
is a type-level integer.
A computation of type (ICC i k a)
gets i
maps numbered from 0 to i
-1, an infinite list of different identifiers,
and returns a value of type a
.
runICC :: I i => (forall k. ICC i k a) -> aSource
Return the value computed by an identifier-consuming computation.
forall k
ensures that the identifiers indexed by k
are inaccessible to the rest of the program.
type ICCS i k a = Maps i k -> Sets I32 k -> [Id k] -> aSource
Identifier-consuming computation with sets. i
is a type-level integer.
A computation of type (ICCS i k a)
gets 32 sets numbered from 0 to 31, i
maps numbered from 1 to i
, an infinite list of different identifiers,
and returns a value of type a
.
runICCS :: I i => (forall k. ICCS i k a) -> aSource
Return the value computed by an identifier-consuming computation with sets.
forall k
ensures that the identifiers indexed by k
are inaccessible to the rest of the program.
For internal use
class MaplikeClass i x Source
I i => MaplikeClass (M i) a | |
(I i, I j) => MaplikeClass (S j i) () |