linear-maps-0.6.1: Finite maps for linear use

Data.IdMap

Description

Linearly usable maps and sets on identifiers

Synopsis

# Identifiers

data Id k Source

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

• an uninstantiated type variable (inside invocations of `runICC` and `runICCS`), or
• `(a :|: b)`, where `a` and `b` are identifier indexes.

Instances

 Incl Id Eq (Id a)

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 `Id (a :|: a)` which could cause strange runtime behaviour. For example, `(left x == right x)` should be `False` in theory, but during runtime `(left x)` and `(right x)` are exactly the same identifiers.

# Finite maps and sets

type Map i k a = Maplike (M i) k aSource

Family of finite maps from keys `(Id k)` to values `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 `(Id k)`. For efficiency reasons, use only with concrete type integers:

``` 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.

member :: MaplikeClass i a => Id k -> Maplike i k a -> BoolSource

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

data Sets i k whereSource

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

Constructors

 PlusSet :: Set i k -> Sets i k -> Sets (Succ i) k

data Maps i k whereSource

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

Constructors

 PlusMap :: (forall a. Map (Succ i) k a) -> Maps i k -> Maps (Succ i) k

# 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

data Maplike i k a Source

Instances

 Functor2 (Maplike i) Functor (Maplike i k)

class MaplikeClass i x Source

Instances

 I i => MaplikeClass (M i) a (I i, I j) => MaplikeClass (S j i) ()

inserts :: I i => Map i k a -> [(Id k, a)] -> Map i k aSource

(!) :: I i => Map i k a -> Id k -> aSource

setInsert :: I i => Id k -> Set i k -> Set i kSource

O(1). Insert a new key in the set. If the key is already in the set, the original set is returned.

After insertion, the original set may not be used.

setInserts :: I i => Set i k -> [Id k] -> Set i kSource