linear-maps-0.6.1: Finite maps for linear use

Data.IdMap

Contents

Description

Linearly usable maps and sets on identifiers

Synopsis

Documentation

module Data.Subtyping

module Data.TypeInt

module Control.Functor

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

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